Journal articles: 'Max-SAT Problem'

1

Chieu, H. L., and W. S. Lee. "Relaxed Survey Propagation for The Weighted Maximum Satisfiability Problem." Journal of Artificial Intelligence Research 36 (October 30, 2009): 229–66. http://dx.doi.org/10.1613/jair.2808.

Full text

Abstract:

The survey propagation (SP) algorithm has been shown to work well on large instances of the random 3-SAT problem near its phase transition. It was shown that SP estimates marginals over covers that represent clusters of solutions. The SP-y algorithm generalizes SP to work on the maximum satisfiability (Max-SAT) problem, but the cover interpretation of SP does not generalize to SP-y. In this paper, we formulate the relaxed survey propagation (RSP) algorithm, which extends the SP algorithm to apply to the weighted Max-SAT problem. We show that RSP has an interpretation of estimating marginals over covers violating a set of clauses with minimal weight. This naturally generalizes the cover interpretation of SP. Empirically, we show that RSP outperforms SP-y and other state-of-the-art Max-SAT solvers on random Max-SAT instances. RSP also outperforms state-of-the-art weighted Max-SAT solvers on random weighted Max-SAT instances.

APA, Harvard, Vancouver, ISO, and other styles

2

Abu Doush, Iyad, Amal Lutfi Quran, Mohammed Azmi Al-Betar, and Mohammed A. Awadallah. "MAX-SAT Problem using Hybrid Harmony Search Algorithm." Journal of Intelligent Systems 27, no. 4 (October 25, 2018): 643–58. http://dx.doi.org/10.1515/jisys-2016-0129.

Full text

Abstract:

Abstract Maximum Satisfiability problem is an optimization variant of the Satisfiability problem (SAT) denoted as MAX-SAT. The aim of this problem is to find Boolean variable assignment that maximizes the number of satisfied clauses in the Boolean formula. In case the number of variables per clause is equal or greater than three, then this problem is considered NP-complete. Hence, many researchers have developed techniques to deal with MAX-SAT. In this paper, we investigate the impact of different hybrid versions of binary harmony search (HS) algorithm on solving MAX 3-SAT problem. Therefore, we propose two novel hybrid binary HS algorithms. The first hybridizes Flip heuristic with HS, and the second uses Tabu search combined with Flip heuristic. Furthermore, a distinguished feature of our proposed approaches is using an objective function that is updated dynamically based on the stepwise adaptation of weights (SAW) mechanism to evaluate the MAX-SAT solution using the proposed hybrid versions. The performance of the proposed approaches is evaluated over standard MAX-SAT benchmarks, and the results are compared with six evolutionary algorithms and three stochastic local search algorithms. The obtained results are competitive and show that the proposed novel approaches are effective.

APA, Harvard, Vancouver, ISO, and other styles

3

Py, Matthieu, Mohamed Sami Cherif, and Djamal Habet. "Proofs and Certificates for Max-SAT." Journal of Artificial Intelligence Research 75 (December 8, 2022): 1373–400. http://dx.doi.org/10.1613/jair.1.13811.

Full text

Abstract:

Current Max-SAT solvers are able to efficiently compute the optimal value of an input instance but they do not provide any certificate of its validity. In this paper, we present a tool, called MS-Builder, which generates certificates for the Max-SAT problem in the particular form of a sequence of equivalence-preserving transformations. To generate a certificate, MS-Builder iteratively calls a SAT oracle to get a SAT resolution refutation which is handled and adapted into a sound refutation for Max-SAT. In particular, we prove that the size of the computed Max-SAT refutation is linear with respect to the size of the initial refutation if it is semi-read-once, tree-like regular, tree-like or semi-tree-like. Additionally, we propose an extendable tool, called MS-Checker, able to verify the validity of any Max-SAT certificate using Max-SAT inference rules. Both tools are evaluated on the unweighted and weighted benchmark instances of the 2020 Max-SAT Evaluation.

APA, Harvard, Vancouver, ISO, and other styles

4

Li, C. M., F. Manya, and J. Planes. "New Inference Rules for Max-SAT." Journal of Artificial Intelligence Research 30 (October 23, 2007): 321–59. http://dx.doi.org/10.1613/jair.2215.

Full text

Abstract:

Exact Max-SAT solvers, compared with SAT solvers, apply little inference at each node of the proof tree. Commonly used SAT inference rules like unit propagation produce a simplified formula that preserves satisfiability but, unfortunately, solving the Max-SAT problem for the simplified formula is not equivalent to solving it for the original formula. In this paper, we define a number of original inference rules that, besides being applied efficiently, transform Max-SAT instances into equivalent Max-SAT instances which are easier to solve. The soundness of the rules, that can be seen as refinements of unit resolution adapted to Max-SAT, are proved in a novel and simple way via an integer programming transformation. With the aim of finding out how powerful the inference rules are in practice, we have developed a new Max-SAT solver, called MaxSatz, which incorporates those rules, and performed an experimental investigation. The results provide empirical evidence that MaxSatz is very competitive, at least, on random Max-2SAT, random Max-3SAT, Max-Cut, and Graph 3-coloring instances, as well as on the benchmarks from the Max-SAT Evaluation 2006.

APA, Harvard, Vancouver, ISO, and other styles

5

Bouhmala, Noureddine. "A Variable Neighborhood Walksat-Based Algorithm for MAX-SAT Problems." Scientific World Journal 2014 (2014): 1–11. http://dx.doi.org/10.1155/2014/798323.

Full text

Abstract:

The simplicity of the maximum satisfiability problem (MAX-SAT) combined with its applicability in many areas of artificial intelligence and computing science made it one of the fundamental optimization problems. This NP-complete problem refers to the task of finding a variable assignment that satisfies the maximum number of clauses (or the sum of weights of satisfied clauses) in a Boolean formula. The Walksat algorithm is considered to be the main skeleton underlying almost all local search algorithms for MAX-SAT. Most local search algorithms including Walksat rely on the 1-flip neighborhood structure. This paper introduces a variable neighborhood walksat-based algorithm. The neighborhood structure can be combined easily using any local search algorithm. Its effectiveness is compared with existing algorithms using 1-flip neighborhood structure and solvers such as CCLS and Optimax from the eighth MAX-SAT evaluation.

APA, Harvard, Vancouver, ISO, and other styles

6

Wang, Xiaofeng, and Jiulei Jiang. "Warning Propagation Algorithm for the MAX-3-SAT Problem." IEEE Transactions on Emerging Topics in Computing 7, no. 4 (October 1, 2019): 578–84. http://dx.doi.org/10.1109/tetc.2017.2736504.

Full text

APA, Harvard, Vancouver, ISO, and other styles

7

Bertoni, Alberto, Marco Carpentieri, Paola Campadelli, and Giuliano Grossi. "A Genetic Model: Analysis and Application to MAXSAT." Evolutionary Computation 8, no. 3 (September 2000): 291–309. http://dx.doi.org/10.1162/106365600750078790.

Full text

Abstract:

In this paper, a genetic model based on the operations of recombination and mutation is studied and applied to combinatorial optimization problems. Results are: The equations of the deterministic dynamics in the thermodynamic limit (infinite populations) are derived and, for a sufficiently small mutation rate, the attractors are characterized; A general approximation algorithm for combinatorial optimization problems is designed. The algorithm is applied to the Max Ek-Sat problem, and the quality of the solution is analyzed. It is proved to be optimal for k≥3 with respect to the worst case analysis; for Max E3-Sat the average case performances are experimentally compared with other optimization techniques.

APA, Harvard, Vancouver, ISO, and other styles

8

Alasow, Abdirahman, Peter Jin, and Marek Perkowski. "Quantum Algorithm for Variant Maximum Satisfiability." Entropy 24, no. 11 (November 5, 2022): 1615. http://dx.doi.org/10.3390/e24111615.

Full text

Abstract:

In this paper, we proposed a novel quantum algorithm for the maximum satisfiability problem. Satisfiability (SAT) is to find the set of assignment values of input variables for the given Boolean function that evaluates this function as TRUE or prove that such satisfying values do not exist. For a POS SAT problem, we proposed a novel quantum algorithm for the maximum satisfiability (MAX-SAT), which returns the maximum number of OR terms that are satisfied for the SAT-unsatisfiable function, providing us with information on how far the given Boolean function is from the SAT satisfaction. We used Grover’s algorithm with a new block called quantum counter in the oracle circuit. The proposed circuit can be adapted for various forms of satisfiability expressions and several satisfiability-like problems. Using the quantum counter and mirrors for SAT terms reduces the need for ancilla qubits and realizes a large Toffoli gate that is then not needed. Our circuit reduces the number of ancilla qubits for the terms T of the Boolean function from T of ancilla qubits to ≈⌈log2⁡T⌉+1. We analyzed and compared the quantum cost of the traditional oracle design with our design which gives a low quantum cost.

APA, Harvard, Vancouver, ISO, and other styles

9

Gallo, G., C. Gentile, D. Pretolani, and G. Rago. "Max Horn SAT and the minimum cut problem in directed hypergraphs." Mathematical Programming 80, no. 2 (January 1998): 213–37. http://dx.doi.org/10.1007/bf01581727.

Full text

APA, Harvard, Vancouver, ISO, and other styles

10

Zhu, Wenxing, and Yuanhui Yan. "Solving the weighted MAX-SAT problem using the dynamic convexized method." Optimization Letters 8, no. 1 (November 8, 2012): 359–74. http://dx.doi.org/10.1007/s11590-012-0583-4.

Full text

APA, Harvard, Vancouver, ISO, and other styles

11

Adelshin, A. V., and A. K. Kuchin. "ANALYSIS OF L-STRUCTURE OF POLYHEDRON IN THE PARTIAL MAX SAT PROBLEM." Prikladnaya diskretnaya matematika, no. 38 (December 1, 2017): 110–18. http://dx.doi.org/10.17223/20710410/38/9.

Full text

APA, Harvard, Vancouver, ISO, and other styles

12

WOCJAN, PAWEL, and THOMAS BETH. "THE 2-LOCAL HAMILTONIAN PROBLEM ENCOMPASSES NP." International Journal of Quantum Information 01, no. 03 (September 2003): 349–57. http://dx.doi.org/10.1142/s021974990300022x.

Full text

Abstract:

We show that the NP-complete problems max cut and independent set can be formulated as the 2-local Hamiltonian problem as defined by Kitaev. The 5-local Hamiltonian problem was the first problem to be shown to be complete for the quantum complexity class QMA — the quantum analog of NP. Subsequently, it was shown that 3-locality is already sufficient for QMA-completeness. It is still not known whether the 2-local Hamiltonian problem is QMA-complete. Therefore it is interesting to determine what problems can be reduced to the 2-local Hamiltonian problem. Kitaev showed that 3-SAT can be formulated as a 3-local Hamiltonian problem. We extend his result by showing that 2-locality is sufficient in order to encompass NP.

APA, Harvard, Vancouver, ISO, and other styles

13

Omelchenko, Oleksii, and Andrei A. Bulatov. "Analysis of Pure Literal Elimination Rule for Non-uniform Random (MAX) k-SAT Problem with an Arbitrary Degree Distribution." Proceedings of the AAAI Conference on Artificial Intelligence 36, no. 4 (June 28, 2022): 3804–12. http://dx.doi.org/10.1609/aaai.v36i4.20295.

Full text

Abstract:

MAX k-SAT is one of the archetypal NP-hard problems. Its variation called random MAX k-SAT problem was introduced in order to understand how hard it is to solve instances of the problem on average. The most common model to sample random instances is the uniform model, which has received a large amount of attention. However, the uniform model often fails to capture important structural properties we observe in the real-world instances. To address these limitations, a more general (in a certain sense) model has been proposed, the configuration model, which is able to produce instances with an arbitrary distribution of variables' degrees, and so can simulate biases in instances appearing in various applications. Our overall goal is to expand the theory built around the uniform model to the more general configuration model for a wide range of degree distributions. This includes locating satisfiability thresholds and analysing the performance of the standard heuristics applied to instances sampled from the configuration model. In this paper we analyse the performance of the pure literal elimination rule. We provide an equation that given an underlying degree distribution gives the number of clauses the pure literal elimination rule satisfies w.h.p. We also show how the distribution of variable degrees changes over time as the algorithm is being executed.

APA, Harvard, Vancouver, ISO, and other styles

14

Ma, Shaohan, and Dongmin Liang. "A polynomial-time algorithm for reducing the number of variables in MAX SAT problem." Science in China Series E: Technological Sciences 40, no. 3 (June 1997): 301–11. http://dx.doi.org/10.1007/bf02916605.

Full text

APA, Harvard, Vancouver, ISO, and other styles

15

Xu, Zhenxing, Kun He, and Chu-Min Li. "An iterative Path-Breaking approach with mutation and restart strategies for the MAX-SAT problem." Computers & Operations Research 104 (April 2019): 49–58. http://dx.doi.org/10.1016/j.cor.2018.12.005.

Full text

APA, Harvard, Vancouver, ISO, and other styles

16

Palubeckis, Gintaras. "A new bounding procedure and an improved exact algorithm for the Max-2-SAT problem." Applied Mathematics and Computation 215, no. 3 (October 2009): 1106–17. http://dx.doi.org/10.1016/j.amc.2009.06.043.

Full text

APA, Harvard, Vancouver, ISO, and other styles

17

Hastings, M. B. "A Short Path Quantum Algorithm for Exact Optimization." Quantum 2 (July 26, 2018): 78. http://dx.doi.org/10.22331/q-2018-07-26-78.

Full text

Abstract:

We give a quantum algorithm to exactly solve certain problems in combinatorial optimization, including weighted MAX-2-SAT as well as problems where the objective function is a weighted sum of products of Ising variables, all terms of the same degree D; this problem is called weighted MAX-ED-LIN2. We require that the optimal solution be unique for odd D and doubly degenerate for even D; however, we expect that the algorithm still works without this condition and we show how to reduce to the case without this assumption at the cost of an additional overhead. While the time required is still exponential, the algorithm provably outperforms Grover's algorithm assuming a mild condition on the number of low energy states of the target Hamiltonian. The detailed analysis of the runtime dependence on a tradeoff between the number of such states and algorithm speed: fewer such states allows a greater speedup. This leads to a natural hybrid algorithm that finds either an exact or approximate solution.

APA, Harvard, Vancouver, ISO, and other styles

18

Chicano, Francisco, Andrew M. Sutton, L. Darrell Whitley, and Enrique Alba. "Fitness Probability Distribution of Bit-Flip Mutation." Evolutionary Computation 23, no. 2 (June 2015): 217–48. http://dx.doi.org/10.1162/evco_a_00130.

Full text

Abstract:

Bit-flip mutation is a common mutation operator for evolutionary algorithms applied to optimize functions over binary strings. In this paper, we develop results from the theory of landscapes and Krawtchouk polynomials to exactly compute the probability distribution of fitness values of a binary string undergoing uniform bit-flip mutation. We prove that this probability distribution can be expressed as a polynomial in p, the probability of flipping each bit. We analyze these polynomials and provide closed-form expressions for an easy linear problem (Onemax), and an NP-hard problem, MAX-SAT. We also discuss a connection of the results with runtime analysis.

APA, Harvard, Vancouver, ISO, and other styles

19

Munawar, Asim, Mohamed Wahib, Masaharu Munetomo, and Kiyoshi Akama. "Hybrid of genetic algorithm and local search to solve MAX-SAT problem using nVidia CUDA framework." Genetic Programming and Evolvable Machines 10, no. 4 (October 20, 2009): 391–415. http://dx.doi.org/10.1007/s10710-009-9091-4.

Full text

APA, Harvard, Vancouver, ISO, and other styles

20

Grégoire, Éric, and Jean-Marie Lagniez. "RCL: An A. I. Tool for Computing Maximal Consensuses." International Journal on Artificial Intelligence Tools 25, no. 04 (August 2016): 1650026. http://dx.doi.org/10.1142/s0218213016500263.

Full text

Abstract:

RCL is an original Artificial Intelligence tool for computing maximal consensuses among conflicting agents in the Boolean logic framework. It extracts one maximal set of information that does not conflict with any of the agents, taking all possible deductions into account. This form of consensus can go far beyond what is actually shared by all agents. It might be endorsed by every agent since it does not conflict with any of them. Several types of preference criteria can be selected and iterated in order to orient the computation towards some preferred consensuses. From a computational point of view RCL relies on an internal transformation of the maximal consensus-finding problem into one single instance of the Weighted Partial Max-SAT problem.

APA, Harvard, Vancouver, ISO, and other styles

21

Fielder, Catherine E., Yao-Yuan Mao, Jeffrey A. Newman, Andrew R. Zentner, and Timothy C. Licquia. "Predictably missing satellites: subhalo abundances in Milky Way-like haloes." Monthly Notices of the Royal Astronomical Society 486, no. 4 (April 17, 2019): 4545–68. http://dx.doi.org/10.1093/mnras/stz1098.

Full text

Abstract:

ABSTRACT On small scales there have been a number of claims of discrepancies between the standard cold dark matter (CDM) model and observations. The ‘missing satellites problem’ infamously describes the overabundance of subhaloes from CDM simulations compared to the number of satellites observed in the Milky Way. A variety of solutions to this discrepancy have been proposed; however, the impact of the specific properties of the Milky Way halo relative to the typical halo of its mass has yet to be explored. Motivated by recent studies that identified ways in which the Milky Way is atypical, we investigate how the properties of dark matter haloes with mass comparable to our Galaxy’s – including concentration, spin, shape, and scale factor of the last major merger – correlate with the subhalo abundance. Using zoom-in simulations of Milky Way-like haloes, we build two models of subhalo abundance as functions of host halo properties. From these models we conclude that the Milky Way most likely has fewer subhaloes than the average halo of the same mass. We expect up to 30 per cent fewer subhaloes with low maximum rotation velocities ($V_{\rm max}^{\rm sat} \sim 10$ km s−1) at the 68 per cent confidence level and up to 52 per cent fewer than average subhaloes with high rotation velocities ($V_{\rm max}^{\rm sat} \gtrsim 30$ km s−1, comparable to the Magellanic Clouds) than would be expected for a typical halo of the Milky Way’s mass. Concentration is the most informative single parameter for predicting subhalo abundance. Our results imply that models tuned to explain the missing satellites problem assuming typical subhalo abundances for our Galaxy may be overcorrecting.

APA, Harvard, Vancouver, ISO, and other styles

22

DOVIER, AGOSTINO. "Preface." Theory and Practice of Logic Programming 17, no. 4 (July 2017): 359–64. http://dx.doi.org/10.1017/s1471068417000199.

Full text

Abstract:

Magic squares, chess-like problems, cryptarithmetic puzzles, and similar classes of problems have been extensively used to challenge human reasoning capabilities. Lo Shu magic square can be traced back to 650 B.C., the eight-queens problem was proposed in 1848 by the chess player Max Bazzel TWO × TWO = THREE puzzle appeared in Strand Magazine in 1924. These puzzles are nowadays widely used in constraint programming courses. The first programming language provided with constraint modelling primitives (Sketchpad) has been proposed by the Turing award winner Ivan Sutherland in his PhD thesis (1963). Logemann and Loveland, when implementing the Davis–Putnam procedure (Davis and Putnam 1960) for testing the satisfiability of a propositional formula (SAT), devised an algorithm (Davis–Putnam–Logemann–Loveland (DPLL)) that has become the core of all SAT/and Answer Set Programming solvers (50 years later). It consists in choosing an un-assigned variable, assigning it a value 0 or 1, propagating the chosen value (unit propagation), and proceeding with the alternative value, if the original assignment leads to a contradiction (backtracking). Some years later Waltz (1975) introduced the notion of domain filtering (arc-consistency-based constraint propagation). With this idea the same DPLL scheme can be used for verifying the satisfiability of a constraint satisfaction problem, where the assignment is no longer 0/1 and the unit propagation is replaced by constraint propagation. For a detailed history of these early years achievements, we refer the reader to the works by Loveland et al. (2017), Jaffar and Maher (1994), and Freuder and Mackworth (2006).

APA, Harvard, Vancouver, ISO, and other styles

23

Sahai, Tuhin, Anurag Mishra, Jose Miguel Pasini, and Susmit Jha. "Estimating the Density of States of Boolean Satisfiability Problems on Classical and Quantum Computing Platforms." Proceedings of the AAAI Conference on Artificial Intelligence 34, no. 02 (April 3, 2020): 1627–35. http://dx.doi.org/10.1609/aaai.v34i02.5524.

Full text

Abstract:

Given a Boolean formula ϕ(x) in conjunctive normal form (CNF), the density of states counts the number of variable assignments that violate exactly e clauses, for all values of e. Thus, the density of states is a histogram of the number of unsatisfied clauses over all possible assignments. This computation generalizes both maximum-satisfiability (MAX-SAT) and model counting problems and not only provides insight into the entire solution space, but also yields a measure for the hardness of the problem instance. Consequently, in real-world scenarios, this problem is typically infeasible even when using state-of-the-art algorithms. While finding an exact answer to this problem is a computationally intensive task, we propose a novel approach for estimating density of states based on the concentration of measure inequalities. The methodology results in a quadratic unconstrained binary optimization (QUBO), which is particularly amenable to quantum annealing-based solutions. We present the overall approach and compare results from the D-Wave quantum annealer against the best-known classical algorithms such as the Hamze-de Freitas-Selby (HFS) algorithm and satisfiability modulo theory (SMT) solvers.

APA, Harvard, Vancouver, ISO, and other styles

24

Alkasem, Haifa Hamad, and Mohamed El Bachir Menai. "A Stochastic Local Search Algorithm for the Partial Max-SAT Problem Based on Adaptive Tuning and Variable Depth Neighborhood Search." IEEE Access 9 (2021): 49806–43. http://dx.doi.org/10.1109/access.2021.3068824.

Full text

APA, Harvard, Vancouver, ISO, and other styles

25

Francès, Guillem, Blai Bonet, and Hector Geffner. "Learning General Planning Policies from Small Examples Without Supervision." Proceedings of the AAAI Conference on Artificial Intelligence 35, no. 13 (May 18, 2021): 11801–8. http://dx.doi.org/10.1609/aaai.v35i13.17402.

Full text

Abstract:

Generalized planning is concerned with the computation of general policies that solve multiple instances of a planning domain all at once. It has been recently shown that these policies can be computed in two steps: first, a suitable abstraction in the form of a qualitative numerical planning problem (QNP) is learned from sample plans, then the general policies are obtained from the learned QNP using a planner. In this work, we introduce an alternative approach for computing more expressive general policies which does not require sample plans or a QNP planner. The new formulation is very simple and can be cast in terms that are more standard in machine learning: a large but finite pool of features is defined from the predicates in the planning examples using a general grammar, and a small subset of features is sought for separating “good” from “bad” state transitions, and goals from non-goals. The problems of finding such a “separating surface” while labeling the transitions as “good” or “bad” are jointly addressed as a single combinatorial optimization problem expressed as a Weighted Max-SAT problem. The advantage of looking for the simplest policy in the given feature space that solves the given examples, possibly non-optimally, is that many domains have no general, compact policies that are optimal. The approach yields general policies for a number of benchmark domains.

APA, Harvard, Vancouver, ISO, and other styles

26

Traversa, Fabio L., Pietro Cicotti, Forrest Sheldon, and Massimiliano Di Ventra. "Evidence of Exponential Speed-Up in the Solution of Hard Optimization Problems." Complexity 2018 (July 3, 2018): 1–13. http://dx.doi.org/10.1155/2018/7982851.

Full text

Abstract:

Optimization problems pervade essentially every scientific discipline and industry. A common form requires identifying a solution satisfying the maximum number among a set of many conflicting constraints. Often, these problems are particularly difficult to solve, requiring resources that grow exponentially with the size of the problem. Over the past decades, research has focused on developing heuristic approaches that attempt to find an approximation to the solution. However, despite numerous research efforts, in many cases even approximations to the optimal solution are hard to find, as the computational time for further refining a candidate solution also grows exponentially with input size. In this paper, we show a noncombinatorial approach to hard optimization problems that achieves an exponential speed-up and finds better approximations than the current state of the art. First, we map the optimization problem into a Boolean circuit made of specially designed, self-organizing logic gates, which can be built with (nonquantum) electronic elements with memory. The equilibrium points of the circuit represent the approximation to the problem at hand. Then, we solve its associated nonlinear ordinary differential equations numerically, towards the equilibrium points. We demonstrate this exponential gain by comparing a sequential MATLAB implementation of our solver with the winners of the 2016 Max-SAT competition on a variety of hard optimization instances. We show empirical evidence that our solver scales linearly with the size of the problem, both in time and memory, and argue that this property derives from the collective behavior of the simulated physical circuit. Our approach can be applied to other types of optimization problems, and the results presented here have far-reaching consequences in many fields.

APA, Harvard, Vancouver, ISO, and other styles

27

Zhuo, Hankz Hankui, Qiang Yang, Rong Pan, and Lei Li. "Cross-Domain Action-Model Acquisition for Planning via Web Search." Proceedings of the International Conference on Automated Planning and Scheduling 21 (March 22, 2011): 298–305. http://dx.doi.org/10.1609/icaps.v21i1.13449.

Full text

Abstract:

Applying learning techniques to acquire action models is an area of intense research interest. Most previous works in this area have assumed that there is a significant amount of training data available in a planning domain of interest, which we call target domain, where action models are to be learned. However, it is often difficult to acquire sufficient training data to ensure that the learned action models are of high quality. In this paper, we develop a novel approach to learning action models with limited training data in the target domain by transferring knowledge from related auxiliary or source domains. We assume that the action models in the source domains have already been created before, and seek to transfer as much of the the available information from the source domains as possible to help our learning task. We first exploit a Web searching method to bridge the target and source domains, such that transferrable knowledge from source domains is identified. We then encode the transferred knowledge together with the available data from the target domain as constraints in a maximum satisfiability problem, and solve these constraints using a weighted MAX-SAT solver. We finally transform the solutions thus obtained into high-quality target-domain action models. We empirically show that our transfer-learning based framework is effective in several domains, including the International Planning Competition (IPC) domains and some synthetic domains.

APA, Harvard, Vancouver, ISO, and other styles

28

Escoffier, Bruno, and Vangelis Th Paschos. "Differential approximation of min sat, max sat and related problems." European Journal of Operational Research 181, no. 2 (September 2007): 620–33. http://dx.doi.org/10.1016/j.ejor.2005.04.057.

Full text

APA, Harvard, Vancouver, ISO, and other styles

29

Argelich, Josep, and Felip Manyà. "Exact Max-SAT solvers for over-constrained problems." Journal of Heuristics 12, no. 4-5 (September 2006): 375–92. http://dx.doi.org/10.1007/s10732-006-7234-9.

Full text

APA, Harvard, Vancouver, ISO, and other styles

30

Maciejewski, Filip B., Flavio Baccari, Zoltán Zimborás, and Michał Oszmaniec. "Modeling and mitigation of cross-talk effects in readout noise with applications to the Quantum Approximate Optimization Algorithm." Quantum 5 (June 1, 2021): 464. http://dx.doi.org/10.22331/q-2021-06-01-464.

Full text

Abstract:

Measurement noise is one of the main sources of errors in currently available quantum devices based on superconducting qubits. At the same time, the complexity of its characterization and mitigation often exhibits exponential scaling with the system size. In this work, we introduce a correlated measurement noise model that can be efficiently described and characterized, and which admits effective noise-mitigation on the level of marginal probability distributions. Noise mitigation can be performed up to some error for which we derive upper bounds. Characterization of the model is done efficiently using Diagonal Detector Overlapping Tomography – a generalization of the recently introduced Quantum Overlapping Tomography to the problem of reconstruction of readout noise with restricted locality. The procedure allows to characterize k-local measurement cross-talk on N-qubit device using O(k2klog(N)) circuits containing random combinations of X and identity gates. We perform experiments on 15 (23) qubits using IBM's (Rigetti's) devices to test both the noise model and the error-mitigation scheme, and obtain an average reduction of errors by a factor >22 (>5.5) compared to no mitigation. Interestingly, we find that correlations in the measurement noise do not correspond to the physical layout of the device. Furthermore, we study numerically the effects of readout noise on the performance of the Quantum Approximate Optimization Algorithm (QAOA). We observe in simulations that for numerous objective Hamiltonians, including random MAX-2-SAT instances and the Sherrington-Kirkpatrick model, the noise-mitigation improves the quality of the optimization. Finally, we provide arguments why in the course of QAOA optimization the estimates of the local energy (or cost) terms often behave like uncorrelated variables, which greatly reduces sampling complexity of the energy estimation compared to the pessimistic error analysis. We also show that similar effects are expected for Haar-random quantum states and states generated by shallow-depth random circuits.

APA, Harvard, Vancouver, ISO, and other styles

31

Cade, Chris, Marten Folkertsma, Ido Niesen, and Jordi Weggemans. "Quantifying Grover speed-ups beyond asymptotic analysis." Quantum 7 (October 10, 2023): 1133. http://dx.doi.org/10.22331/q-2023-10-10-1133.

Full text

Abstract:

Run-times of quantum algorithms are often studied via an asymptotic, worst-case analysis. Whilst useful, such a comparison can often fall short: it is not uncommon for algorithms with a large worst-case run-time to end up performing well on instances of practical interest. To remedy this it is necessary to resort to run-time analyses of a more empirical nature, which for sufficiently small input sizes can be performed on a quantum device or a simulation thereof. For larger input sizes, alternative approaches are required.In this paper we consider an approach that combines classical emulation with detailed complexity bounds that include all constants. We simulate quantum algorithms by running classical versions of the sub-routines, whilst simultaneously collecting information about what the run-time of the quantum routine would have been if it were run instead. To do this accurately and efficiently for very large input sizes, we describe an estimation procedure and prove that it obtains upper bounds on the true expected complexity of the quantum algorithms.We apply our method to some simple quantum speedups of classical heuristic algorithms for solving the well-studied MAX-k-SAT optimization problem. This requires rigorous bounds (including all constants) on the expected- and worst-case complexities of two important quantum sub-routines: Grover search with an unknown number of marked items, and quantum maximum-finding. These improve upon existing results and might be of broader interest.Amongst other results, we found that the classical heuristic algorithms we studied did not offer significant quantum speedups despite the existence of a theoretical per-step speedup. This suggests that an empirical analysis such as the one we implement in this paper already yields insights beyond those that can be seen by an asymptotic analysis alone.

APA, Harvard, Vancouver, ISO, and other styles

32

Boughaci, Dalila, Belaïd Benhamou, and Habiba Drias. "Scatter Search and Genetic Algorithms for MAX-SAT Problems." Journal of Mathematical Modelling and Algorithms 7, no. 2 (February 27, 2008): 101–24. http://dx.doi.org/10.1007/s10852-008-9077-x.

Full text

APA, Harvard, Vancouver, ISO, and other styles

33

Kumar, Mohit, Samuel Kolb, Stefano Teso, and Luc De Raedt. "Learning MAX-SAT from Contextual Examples for Combinatorial Optimisation." Proceedings of the AAAI Conference on Artificial Intelligence 34, no. 04 (April 3, 2020): 4493–500. http://dx.doi.org/10.1609/aaai.v34i04.5877.

Full text

Abstract:

Combinatorial optimization problems are ubiquitous in artificial intelligence. Designing the underlying models, however, requires substantial expertise, which is a limiting factor in practice. The models typically consist of hard and soft constraints, or combine hard constraints with a preference function. We introduce a novel setting for learning combinatorial optimisation problems from contextual examples. These positive and negative examples show – in a particular context – whether the solutions are good enough or not. We develop our framework using the MAX-SAT formalism. We provide learnability results within the realizable and agnostic settings, as well as hassle, an implementation based on syntax-guided synthesis and showcase its promise on recovering synthetic and benchmark instances from examples.

APA, Harvard, Vancouver, ISO, and other styles

34

Pipatsrisawat, Knot, Akop Palyan, Mark Chavira, Arthur Choi, and Adnan Darwiche. "Solving Weighted Max-SAT Problems in a Reduced Search Space: A Performance Analysis1." Journal on Satisfiability, Boolean Modeling and Computation 4, no. 2-4 (June 1, 2008): 191–217. http://dx.doi.org/10.3233/sat190044.

Full text

APA, Harvard, Vancouver, ISO, and other styles

35

Kochenberger, Gary, Fred Glover, Bahram Alidaee, and Karen Lewis. "Using the unconstrained quadratic program to model and solve Max 2-SAT problems." International Journal of Operational Research 1, no. 1/2 (2005): 89. http://dx.doi.org/10.1504/ijor.2005.007435.

Full text

APA, Harvard, Vancouver, ISO, and other styles

36

Resende, Mauricio G. C., Leonidas S. Pitsoulis, and Panos M. Pardalos. "Fortran subroutines for computing approximate solutions of weighted MAX-SAT problems using GRASP." Discrete Applied Mathematics 100, no. 1-2 (March 2000): 95–113. http://dx.doi.org/10.1016/s0166-218x(99)00171-7.

Full text

APA, Harvard, Vancouver, ISO, and other styles

37

BONGIOVANNI, GIANCARLO, PIERLUIGI CRESCENZI, and SERGIO DE AGOSTINO. "MAX SAT AND MIN SET COVER APPROXIMATION ALGORITHMS ARE $\mathcal P$-COMPLETE." Parallel Processing Letters 05, no. 02 (June 1995): 293–98. http://dx.doi.org/10.1142/s0129626495000278.

Full text

Abstract:

We prove that the sequential approximation algorithms for the problems [Formula: see text] and [Formula: see text] proposed in [9] are [Formula: see text]-hard with respect to the logarithmic space reducibility. As a corollary, these two algorithms cannot be implemented efficiently in parallel unless [Formula: see text].

APA, Harvard, Vancouver, ISO, and other styles

38

Layeb, Abdesslem, and Djamel-Eddine Saidouni. "A Hybrid Quantum Genetic Algorithm and Local Search based DPLL for Max 3-SAT Problems." Applied Mathematics & Information Sciences 8, no. 1 (January 1, 2014): 77–87. http://dx.doi.org/10.12785/amis/080109.

Full text

APA, Harvard, Vancouver, ISO, and other styles

39

Gregory, Peter, Derek Long, Maria Fox, and J. Christopher Beck. "Planning Modulo Theories: Extending the Planning Paradigm." Proceedings of the International Conference on Automated Planning and Scheduling 22 (May 14, 2012): 65–73. http://dx.doi.org/10.1609/icaps.v22i1.13505.

Full text

Abstract:

Considerable effort has been spent extending the scope of planning beyond propositional domains to include, for example, time and numbers. Each extension has been designed as a separate specific semantic enrichment of the underlying planning model, with its own syntax and customised integration into a planning algorithm. Inspired by work on SAT Modulo Theories (SMT) in the SAT community, we develop a modelling language and planner that treat arbitrary first order theories as parameters. We call the approach Planning Modulo Theories (PMT). We introduce a modular language to represent PMT problems and demonstrate its benefits over PDDL in expressivity and compactness. We present a generalisation of the $h_{max}$ heuristic that allows our planner, PMTPlan, to automatically reason about arbitrary theories added as modules. Over several new and existing benchmarks, exploiting different theories, we show that PMTPlan can significantly out-perform an existing planner using PDDL models.

APA, Harvard, Vancouver, ISO, and other styles

40

Russell, Richard, and Sean Holden. "Handling Goal Utility Dependencies in a Satisfiability Framework." Proceedings of the International Conference on Automated Planning and Scheduling 20 (May 25, 2021): 145–52. http://dx.doi.org/10.1609/icaps.v20i1.13401.

Full text

Abstract:

Goal utility dependencies arise when the utility of achieving a goal depends on the other goals that are achieved with it. This complicates the planning procedure because achieving a new goal can potentially alter the utilities of all the other goals currently achieved. In this paper, we present an encoding procedure that enables general-purpose Max-SAT solvers to be used to solve planning problems with goal utility dependencies. We compare this approach to one using integer programming via an empirical evaluation using benchmark problems from past international planning competitions. Our results indicate that this approach is competitive and sometimes more successful than an integer programming one -- solving two to three times more subproblems in some domains, while being outperformed by only a significantly smaller margin in others.

APA, Harvard, Vancouver, ISO, and other styles

41

Alidaee, Bahram, Gary Kochenberger, and Haibo Wang. "Theorems Supporting r-flip Search for Pseudo-Boolean Optimization." International Journal of Applied Metaheuristic Computing 1, no. 1 (January 2010): 93–109. http://dx.doi.org/10.4018/jamc.2010102605.

Full text

Abstract:

Modern metaheuristic methodologies rely on well defined neighborhood structures and efficient means for evaluating potential moves within these structures. Move mechanisms range in complexity from simple 1-flip procedures where binary variables are “flipped” one at a time, to more expensive, but more powerful, r-flip approaches where “r” variables are simultaneously flipped. These multi-exchange neighborhood search strategies have proven to be effective approaches for solving a variety of combinatorial optimization problems. In this paper, we present a series of theorems based on partial derivatives that can be readily adopted to form the essential part of r-flip heuristic search methods for Pseudo-Boolean optimization. To illustrate the use of these results, we present preliminary results obtained from four simple heuristics designed to solve a set of Max 3-SAT problems.

APA, Harvard, Vancouver, ISO, and other styles

42

Sinjorgo, Lennart, and Renata Sotirov. "On Solving MAX-SAT Using Sum of Squares." INFORMS Journal on Computing, November 7, 2023. http://dx.doi.org/10.1287/ijoc.2023.0036.

Full text

Abstract:

We consider semidefinite programming (SDP) approaches for solving the maximum satisfiability (MAX-SAT) problem and weighted partial MAX-SAT. It is widely known that SDP is well-suited to approximate (MAX-)2-SAT. Our work shows the potential of SDP also for other satisfiability problems by being competitive with some of the best solvers in the yearly MAX-SAT competition. Our solver combines sum of squares (SOS)–based SDP bounds and an efficient parser within a branch-and-bound scheme. On the theoretical side, we propose a family of semidefinite feasibility problems and show that a member of this family provides the rank-two guarantee. We also provide a parametric family of semidefinite relaxations for MAX-SAT and derive several properties of monomial bases used in the SOS approach. We connect two well-known SDP approaches for (MAX)-SAT in an elegant way. Moreover, we relate our SOS-SDP relaxations for partial MAX-SAT to the known SAT relaxations. History: Accepted by Andrea Lodi, Area Editor for Design & Analysis of Algorithms – Discrete. Supplemental Material: The online appendix is available at https://doi.org/10.1287/ijoc.2023.0036 .

APA, Harvard, Vancouver, ISO, and other styles

43

Fremont, Daniel, Markus Rabe, and Sanjit Seshia. "Maximum Model Counting." Proceedings of the AAAI Conference on Artificial Intelligence 31, no. 1 (February 12, 2017). http://dx.doi.org/10.1609/aaai.v31i1.11138.

Full text

Abstract:

We introduce the problem Max#SAT, an extension of model counting (#SAT). Given a formula over sets of variables X, Y, and Z, the Max#SAT problem is to maximize over the variables X the number of assignments to Y that can be extended to a solution with some assignment to Z. We demonstrate that Max#SAT has applications in many areas, showing how it can be used to solve problems in probabilistic inference (marginal MAP), planning, program synthesis, and quantitative information flow analysis. We also give an algorithm which by making only polynomially many calls to an NP oracle can approximate the maximum count to within any desired multiplicative error. The NP queries needed are relatively simple, arising from recent practical approximate model counting and sampling algorithms, which allows our technique to be effectively implemented with a SAT solver. Through several experiments we show that our approach can be successfully applied to interesting problems.

APA, Harvard, Vancouver, ISO, and other styles

44

Bannach, Max, Malte Skambath, and Till Tantau. "On the Parallel Parameterized Complexity of MaxSAT Variants." Journal of Artificial Intelligence Research 78 (November 19, 2023). http://dx.doi.org/10.1613/jair.1.14748.

Full text

Abstract:

In the maximum satisfiability problem (max-sat) we are given a propositional formula in conjunctive normal form and have to find an assignment that satisfies as many clauses as possible. We study the parallel parameterized complexity of various versions of max-sat and provide the first constant-time algorithms parameterized either by the solution size or by the allowed excess relative to some guarantee. For the dual parameterized version where the parameter is the number of clauses we are allowed to leave unsatisfied, we present the first parallel algorithm for max-2sat (known as almost-2sat). The difficulty in solving almost-2sat in parallel comes from the fact that the iterative compression method, originally developed to prove that the problem is fixed-parameter tractable at all, is inherently sequential. We observe that a graph flow whose value is a parameter can be computed in parallel and develop a parallel algorithm for the vertex cover problem parameterized above the size of a given matching. Finally, we study the parallel complexity of max-sat parameterized by the vertex cover number, the treedepth, the feedback vertex set number, and the treewidth of the input’s incidence graph. While max-sat is fixedparameter tractable for all of these parameters, we show that they allow different degrees of possible parallelization. For all four we develop dedicated parallel algorithms that are constructive, meaning that they output an optimal assignment – in contrast to results that can be obtained by parallel meta-theorems, which often only solve the decision version.

APA, Harvard, Vancouver, ISO, and other styles

45

Austrin, Per, Jonah Brown-Cohen, and Johan Håstad. "Optimal Inapproximability with Universal Factor Graphs." ACM Transactions on Algorithms, December 15, 2023. http://dx.doi.org/10.1145/3631119.

Full text

Abstract:

The factor graph of an instance of a constraint satisfaction problem (CSP) is the bipartite graph indicating which variables appear in each constraint. An instance of the CSP is given by the factor graph together with a list of which predicate is applied for each constraint. We establish that many Max-CSPs remain as hard to approximate as in the general case even when the factor graph is fixed (depending only on the size of the instance) and known in advance. Examples of results obtained for this restricted setting are: (1) Optimal inapproximability for Max-3-Lin and Max-3-Sat (Håstad, J. ACM 2001). (2) Approximation resistance for predicates supporting pairwise independent subgroups (Chan, J. ACM 2016). (3) Hardness of the “(2 + ϵ)-Sat” problem and other Promise CSPs (Austrin et al., SIAM J. Comput. 2017). The main technical tool used to establish these results is a new way of folding the long code which we call “functional folding”.

APA, Harvard, Vancouver, ISO, and other styles

46

Mirkarimi, Puya, Adam Callison, Lewis Light, Nicholas Chancellor, and Viv Kendon. "Comparing the hardness of MAX 2-SAT problem instances for quantum and classical algorithms." Physical Review Research 5, no. 2 (June 5, 2023). http://dx.doi.org/10.1103/physrevresearch.5.023151.

Full text

APA, Harvard, Vancouver, ISO, and other styles

47

Abbasi-Zadeh, Sepehr, Nikhil Bansal, Guru Guruganesh, Aleksandar Nikolov, Roy Schwartz, and Mohit Singh. "Sticky Brownian Rounding and its Applications to Constraint Satisfaction Problems." ACM Transactions on Algorithms, February 11, 2022. http://dx.doi.org/10.1145/3459096.

Full text

Abstract:

Semidefinite programming is a powerful tool in the design and analysis of approximation algorithms for combinatorial optimization problems. In particular, the random hyperplane rounding method of has been extensively studied for more than two decades, resulting in various extensions to the original technique and beautiful algorithms for a wide range of applications. Despite the fact that this approach yields tight approximation guarantees for some problems, e.g. , Max-Cut , for many others, e.g. , Max-SAT and Max-DiCut , the tight approximation ratio is still unknown. One of the main reasons for this is the fact that very few techniques for rounding semi-definite relaxations are known. In this work, we present a new general and simple method for rounding semi-definite programs, based on Brownian motion. Our approach is inspired by recent results in algorithmic discrepancy theory. We develop and present tools for analyzing our new rounding algorithms, utilizing mathematical machinery from the theory of Brownian motion, complex analysis, and partial differential equations. Focusing on constraint satisfaction problems, we apply our method to several classical problems, including Max-Cut , Max-2SAT , and Max-DiCut , and derive new algorithms that are competitive with the best known results. To illustrate the versatility and general applicability of our approach, we give new approximation algorithms for the Max-Cut problem with side constraints that crucially utilizes measure concentration results for the Sticky Brownian Motion, a feature missing from hyperplane rounding and its generalizations.

APA, Harvard, Vancouver, ISO, and other styles

48

Jansen, Bart M. P., and Michał Włodarczyk. "Optimal Polynomial-time Compression for Boolean Max CSP." ACM Transactions on Computation Theory, September 26, 2023. http://dx.doi.org/10.1145/3624704.

Full text

Abstract:

In the Boolean maximum constraint satisfaction problem – Max CSP ( Γ ) – one is given a collection of weighted applications of constraints from a finite constraint language Γ , over a common set of variables, and the goal is to assign Boolean values to the variables so that the total weight of satisfied constraints is maximized. There exists a concise dichotomy theorem providing a criterion on Γ for the problem to be polynomial-time solvable and stating that otherwise it becomes NP-hard. We study the NP-hard cases through the lens of kernelization and provide a complete characterization of Max CSP ( Γ ) with respect to the optimal compression size. Namely, we prove that Max CSP ( Γ ) parameterized by the number of variables n is either polynomial-time solvable, or there exists an integer d ≥ 2 depending on Γ , such that: (1) An instance of Max CSP ( Γ ) can be compressed into an equivalent instance with $\mathcal {O}(n^d\log n) $ bits in polynomial time, (2) Max CSP( Γ ) does not admit such a compression to $\mathcal {O}(n^{d-\varepsilon }) $ bits unless NP⊆co-NP/poly. Our reductions are based on interpreting constraints as multilinear polynomials combined with the framework of ‘constraint implementations’, formerly used in the context of APX-hardness. As another application of our reductions, we reveal tight connections between optimal running times for solving Max CSP( Γ ) . More precisely, we show that obtaining a running time of the form $\mathcal {O}(2^{(1-\varepsilon)n}) $ for particular classes of Max CSP s is as hard as breaching this barrier for Max d - SAT for some d .

APA, Harvard, Vancouver, ISO, and other styles

49

Chandriah, Kiran Kumar, and Raghavendra V. Naraganahalli. "Maximizing a deep submodular function optimization with a weighted MAX-SAT problem for trajectory clustering and motion segmentation." Applied Intelligence, March 28, 2021. http://dx.doi.org/10.1007/s10489-021-02276-8.

Full text

APA, Harvard, Vancouver, ISO, and other styles

50

Bashar, Mohammad Khairul, and Nikhil Shukla. "Designing Ising machines with higher order spin interactions and their application in solving combinatorial optimization." Scientific Reports 13, no. 1 (June 12, 2023). http://dx.doi.org/10.1038/s41598-023-36531-4.

Full text

Abstract:

AbstractThe Ising model provides a natural mapping for many computationally hard combinatorial optimization problems (COPs). Consequently, dynamical system-inspired computing models and hardware platforms that minimize the Ising Hamiltonian, have recently been proposed as a potential candidate for solving COPs, with the promise of significant performance benefit. However, prior work on designing dynamical systems as Ising machines has primarily considered quadratic interactions among the nodes. Dynamical systems and models considering higher order interactions among the Ising spins remain largely unexplored, particularly for applications in computing. Therefore, in this work, we propose Ising spin-based dynamical systems that consider higher order (> 2) interactions among the Ising spins, which subsequently, enables us to develop computational models to directly solve many COPs that entail such higher order interactions (i.e., COPs on hypergraphs). Specifically, we demonstrate our approach by developing dynamical systems to compute the solution for the Boolean NAE-K-SAT (K ≥ 4) problem as well as solve the Max-K-Cut of a hypergraph. Our work advances the potential of the physics-inspired ‘toolbox’ for solving COPs.

APA, Harvard, Vancouver, ISO, and other styles

Journal articles on the topic 'Max-SAT Problem'

Create a spot-on reference in APA, MLA, Chicago, Harvard, and other styles