Testing satisfiability, finding satisfying assignment

2009 ◽  
pp. 147-178
Keyword(s):  
Satisfying Assignment

scholarly journals Evolving Solutions to Community-Structured Satisfiability Formulas

2019 ◽  
Vol 33 ◽  
pp. 2346-2353
Author(s):  
Frank Neumann ◽  
Andrew M. Sutton
Keyword(s):  
Community Structure ◽  
Evolutionary Algorithms ◽  
Objective Function ◽  
Search Space ◽  
Propositional Satisfiability ◽  
Satisfying Assignment ◽  
Distance Correlation ◽  
Strong Signal ◽  
Fitness Distance Correlation ◽  
Correlation Properties

We study the ability of a simple mutation-only evolutionary algorithm to solve propositional satisfiability formulas with inherent community structure. We show that the community structure translates to good fitness-distance correlation properties, which implies that the objective function provides a strong signal in the search space for evolutionary algorithms to locate a satisfying assignment efficiently. We prove that when the formula clusters into communities of size s ∈ ω(logn) ∩O(nε/(2ε+2)) for some constant 0

NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability

2020 ◽  
Vol 30 (7) ◽  
pp. 736-751
Author(s):  
Hans Kleine Büning ◽  
P. Wojciechowski ◽  
K. Subramani
Keyword(s):  
Normal Form ◽  
Conjunctive Normal Form ◽  
Principal Result ◽  
Satisfying Assignment ◽  
Boolean Formulas ◽  
Complete Procedure ◽  
Np Complete ◽  
Resolution Refutation ◽  
Original Formula ◽  
Cnf Formulas

AbstractIn this paper, we analyze Boolean formulas in conjunctive normal form (CNF) from the perspective of read-once resolution (ROR) refutation schemes. A read-once (resolution) refutation is one in which each clause is used at most once. Derived clauses can be used as many times as they are deduced. However, clauses in the original formula can only be used as part of one derivation. It is well known that ROR is not complete; that is, there exist unsatisfiable formulas for which no ROR exists. Likewise, the problem of checking if a 3CNF formula has a read-once refutation is NP-complete. This paper is concerned with a variant of satisfiability called not-all-equal satisfiability (NAE-satisfiability). A CNF formula is NAE-satisfiable if it has a satisfying assignment in which at least one literal in each clause is set to false. It is well known that the problem of checking NAE-satisfiability is NP-complete. Clearly, the class of CNF formulas which are NAE-satisfiable is a proper subset of satisfiable CNF formulas. It follows that traditional resolution cannot always find a proof of NAE-unsatisfiability. Thus, traditional resolution is not a sound procedure for checking NAE-satisfiability. In this paper, we introduce a variant of resolution called NAE-resolution which is a sound and complete procedure for checking NAE-satisfiability in CNF formulas. The focus of this paper is on a variant of NAE-resolution called read-once NAE-resolution in which each clause (input or derived) can be part of at most one NAE-resolution step. Our principal result is that read-once NAE-resolution is a sound and complete procedure for 2CNF formulas. Furthermore, we provide an algorithm to determine the smallest such NAE-resolution in polynomial time. This is in stark contrast to the corresponding problem concerning 2CNF formulas and ROR refutations. We also show that the problem of checking whether a 3CNF formula has a read-once NAE-resolution is NP-complete.

scholarly journals On the Random Satisfiable Process

2009 ◽  
Vol 18 (5) ◽  
pp. 775-801 ◽  
Author(s):  
MICHAEL KRIVELEVICH ◽  
BENNY SUDAKOV ◽  
DAN VILENCHIK
Keyword(s):  
Degree Sequence ◽  
Natural Extension ◽  
Solution Space ◽  
Polynomial Time Algorithm ◽  
Random Processes ◽  
Time Algorithm ◽  
Satisfying Assignment ◽  
Fixed Degree ◽  
Graph Properties ◽  
Cnf Formulas

In this work we suggest a new model for generating random satisfiable k-CNF formulas. To generate such formulas. randomly permute all $2^k\binom{n}{k}$ possible clauses over the variables x1,. . .,xn, and starting from the empty formula, go over the clauses one by one, including each new clause as you go along if, after its addition, the formula remains satisfiable. We study the evolution of this process, namely the distribution over formulas obtained after scanning through the first m clauses (in the random permutation's order).Random processes with conditioning on a certain property being respected are widely studied in the context of graph properties. This study was pioneered by Ruciński and Wormald in 1992 for graphs with a fixed degree sequence, and also by Erdős, Suen and Winkler in 1995 for triangle-free and bipartite graphs. Since then many other graph properties have been studied, such as planarity and H-freeness. Thus our model is a natural extension of this approach to the satisfiability setting.Our main contribution is as follows. For m ≥ cn, c = c(k) a sufficiently large constant, we are able to characterize the structure of the solution space of a typical formula in this distribution. Specifically, we show that typically all satisfying assignments are essentially clustered in one cluster, and all but e−Ω(m/n)n of the variables take the same value in all satisfying assignments. We also describe a polynomial-time algorithm that finds w.h.p. a satisfying assignment for such formulas.

A Multilevel Memetic Algorithm for Large SAT-Encoded Problems

2012 ◽  
Vol 20 (4) ◽  
pp. 641-664 ◽  
Author(s):  
Noureddine Bouhmala
Keyword(s):  
Original Problem ◽  
Memetic Algorithm ◽  
Satisfying Assignment ◽  
Boolean Expression ◽  
Complete Problem ◽  
Starting Solution ◽  
Previous Level ◽  
Np Complete ◽  
Problem Instances ◽  
Hardware Designs

Many researchers have focused on the satisfiability problem and on many of its variants due to its applicability in many areas of artificial intelligence. This NP-complete problem refers to the task of finding a satisfying assignment that makes a Boolean expression evaluate to True. In this work, we introduce a memetic algorithm that makes use of the multilevel paradigm. The multilevel paradigm refers to the process of dividing large and difficult problems into smaller ones, which are hopefully much easier to solve, and then work backward toward the solution of the original problem, using a solution from a previous level as a starting solution at the next level. Results comparing the memetic with and without the multilevel paradigm are presented using problem instances drawn from real industrial hardware designs.

Minimum propositional proof length is NP-hard to linearly approximate

2001 ◽  
Vol 66 (1) ◽  
pp. 171-191 ◽  
Author(s):  
Michael Alekhnovich ◽  
Sam Buss ◽  
Shlomo Moran ◽  
Toniann Pitassi
Keyword(s):  
Assignment Problem ◽  
Sequent Calculus ◽  
Hardness Of Approximation ◽  
Np Hard ◽  
Satisfying Assignment ◽  
Proof Systems ◽  
Frege Systems ◽  
Propositional Proof ◽  
Almost All ◽  
Polynomial Calculus

AbstractWe prove that the problem of determining the minimum propositional proof length is NP-hard to approximate within a factor of . These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution. Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problems of approximation of the length of proofs.

scholarly journals On Super Strong ETH

2021 ◽  
Vol 70 ◽  
pp. 473-495
Author(s):  
Nikhil Vyas ◽  
Ryan Williams
Keyword(s):  
Randomized Algorithm ◽  
Time Algorithm ◽  
Critical Threshold ◽  
Polynomial Method ◽  
Variable Ratio ◽  
Satisfying Assignment ◽  
Worst Case ◽  
Unbounded Function ◽  
Sat Problem ◽  
Special Case

Multiple known algorithmic paradigms (backtracking, local search and the polynomial method) only yield a 2n(1-1/O(k)) time algorithm for k-SAT in the worst case. For this reason, it has been hypothesized that the worst-case k-SAT problem cannot be solved in 2n(1-f(k)/k) time for any unbounded function f. This hypothesis has been called the "Super-Strong ETH", modelled after the ETH and the Strong ETH. It has also been hypothesized that k-SAT is hard to solve for randomly chosen instances near the "critical threshold", where the clause-to-variable ratio is such that randomly chosen instances are satisfiable with probability 1/2. We give a randomized algorithm which refutes the Super-Strong ETH for the case of random k-SAT and planted k-SAT for any clause-to-variable ratio. For example, given any random k-SAT instance F with n variables and m clauses, our algorithm decides satisfiability for F in  2n(1-c*log(k)/k) time with high probability (over the choice of the formula and the randomness of the algorithm). It turns out that a well-known algorithm from the literature on SAT algorithms does the job: the PPZ algorithm of Paturi, Pudlak, and Zane (1999).   The Unique k-SAT problem is the special case where there is at most one satisfying assignment. Improving prior reductions, we show that the Super-Strong ETHs for Unique k-SAT and k-SAT are equivalent. More precisely, we show the time complexities of Unique k-SAT and k-SAT are very tightly correlated: if Unique k-SAT is in  2n(1-f(k)/k) time for an unbounded f, then k-SAT is in 2n(1-f(k)/(2k)) time.

scholarly journals Finding small counterexamples for abstract rewriting properties

2018 ◽  
Vol 28 (8) ◽  
pp. 1485-1505
Author(s):  
HANS ZANTEMA
Keyword(s):  
Binary Relation ◽  
Normal Forms ◽  
Satisfying Assignment ◽  
Rewrite Systems ◽  
Abstract Setting ◽  
Sat Solver ◽  
Rewrite System ◽  
A Current

Rewriting notions like termination, normal forms and confluence can be described in an abstract way referring to rewriting only as a binary relation. Several theorems on rewriting, like Newman's lemma, can be proved in this abstract setting. For investigating possible generalizations of such theorems, it is fruitful to have counterexamples showing that particular generalizations do not hold. In this paper, we develop a technique to find such counterexamples fully automatically, and we describe our tool Carpa that follows this technique. The basic idea is to fix the number of objects of the abstract rewrite system, and to express the conditions and the negation of the conclusion in a satisfiability (SAT) formula, and then call a current SAT solver. In case the formula turns out to be satisfiable, the resulting satisfying assignment yields a counterexample to the encoded property. We give several examples of finite abstract rewrite systems having remarkable properties that are found in this way fully automatically.

scholarly journals (1,0)-Super Solutions of (k,s)-CNF Formula

Entropy ◽  
2020 ◽  
Vol 22 (2) ◽  
pp. 253 ◽  
Author(s):  
Zufeng Fu ◽  
Daoyun Xu ◽  
Yongping Wang
Keyword(s):  
Combinatorial Optimization ◽  
Reduction Method ◽  
Optimization Problems ◽  
Decision Problems ◽  
Satisfying Assignment ◽  
Critical Function ◽  
Combinatorial Optimization Problems ◽  
Existence Conditions ◽  
Np Complete

A (1,0)-super solution is a satisfying assignment such that if the value of any one variable is flipped to the opposite value, the new assignment is still a satisfying assignment. Namely, every clause must contain at least two satisfied literals. Because of its robustness, super solutions are concerned in combinatorial optimization problems and decision problems. In this paper, we investigate the existence conditions of the (1,0)-super solution of ( k , s ) -CNF formula, and give a reduction method that transform from k-SAT to (1,0)- ( k + 1 , s ) -SAT if there is a ( k + 1 , s )-CNF formula without a (1,0)-super solution. Here, ( k , s ) -CNF is a subclass of CNF in which each clause has exactly k distinct literals, and each variable occurs at most s times. (1,0)- ( k , s ) -SAT is a problem to decide whether a ( k , s ) -CNF formula has a (1,0)-super solution. We prove that for k > 3 , if there exists a ( k , s ) -CNF formula without a (1,0)-super solution, (1,0)- ( k , s ) -SAT is NP-complete. We show that for k > 3 , there is a critical function φ ( k ) such that every ( k , s ) -CNF formula has a (1,0)-super solution for s ≤ φ ( k ) and (1,0)- ( k , s ) -SAT is NP-complete for s > φ ( k ) . We further show some properties of the critical function φ ( k ) .

Sign in / Sign up

Export Citation Format

Share Document