18

Informally: In DNF, you can pick any clause to be true, to make the formula true. This means that a DNF that is equivalent to a certain CNF, is basically an enumeration of all the solutions to boolean sat on the CNF. Note, there can be an exponential number of solutions. Since solving boolean sat for CNF for a single solution is NP-complete, converting to ...


14

Core algorithms like DPLL and its refinements like CDCL are completely deterministic. Note that non-determinism doesn't necessarily mean that an algorithm may lead to a wrong result. For example we can distinguish between Monte Carlo algorithms, which are randomised algorithms whose output may be incorrect with some probability. Las Vegas algorithms, ...


12

For the special case of k out of n variables true where k = 1, there is commander variable encoding as described in Efficient CNF Encoding for Selecting 1 to N Objects by Klieber and Kwon. Simplified: Divide the variables into small groups and add clauses that cause a commander variable's state to imply that a group of variables is either all false or all-...


12

SAT solvers solve the Boolean Satisfiability Problem. This is "the problem of determining if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to TRUE." An example is find an assignment of truth values to variables $a,b,c$ such that $(a \lor b \lor c)\land (\lnot a \lor \lnot b \lor c)\land (a \lor \lnot ...


11

A typical SAT solver notices that a satisfying assignment has been found when there are no more variables to assign. So the only time that a SAT solver would save by early notification is the time it would take to assign values to any remaining unassigned variables. This is a one-time cost linear in the number of variables in the formula. It's linear ...


10

There are other much simpler instances which we provably know that the current algorithms cannot solve in sub-exponential time. These algorithms are incapable of counting (almost all of them are improvements of DPLL which correspond to Resolution propositional proof system). Unfortunately such examples are unsatisfiable instances. The question about ...


10

After reading your question the only way I could see and had enough knowledge to tie the topics together was to give a hi-level set of articles that drill down from software verification ending up with trying to unite model checking and theorem proving. Hopefully my comment did that: Take a look at Software verification then Formal verification then Model ...


10

There are many related ways you can mechanise your logic. Deep embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is (almost) always possible, but makes using the embedded logic awkward. Shallow embedding into one of the well-developed provers such as Isabelle/HOL, Coq or Agda. This is only possible when the embedded ...


10

TL;DR: polynomial reduction increases the size of a problem; using a specific solver allows you to exploit the structure of a problem. When you reduce one NP-complete problem to another one, the size of the problem usually grows polynomially. For example, when you reduce a HAMPATH on a graph with $n$ nodes to SAT, the resulting formula has size of $\Theta(n^...


9

I read a survey paper a few years ago that seems relevant, "Successful SAT Encoding Techniques" by Magnus Björk. Abstract: This article identifies good practices for SAT encodings by analysing interviews with a number of well known SAT experts. The purpose is both to determine the confidence in different encoding strategies by analysing whether there is ...


9

First order logic is undecidable, so SAT solving does not really help. That said, techniques exist for bounded model checking of first order formulas. This means that only a fixed number of objects can be considered when trying to determine whether the formula is true or false. Clearly, this is not complete, but if a counter-example is found, then it truly ...


9

There is some research in this area. In The Effect of Restarts on the Efficiency of Clause Learning Jinbo Huang shows empirically that restarts improve a solver's performance over suites of both satisfiable and unsatisfiable SAT instances. The theoretical justification for the speedup is that in CDCL solvers a restart allows the search to benefit from ...


8

I think this is a very good question. You could also ask: when to use a SMT solver? I have a feeling it might be hard to determine before modeling the problem and actually running the CSP/SAT/SMT solvers and finding out. It is well known that even different solvers perform very differently on the same instances! My intuition also comes from the fact that ...


8

Have a look at the results from this years SAT 2013 competition. Based on these results, definitely give Lingeling a try. Plingeling is the parallel variant of it. If you don't need to prove unsatisfiability (perhaps you know the instance is satisfiable, and you just need to know an assignment making it SAT), you could try local search methods, too.


7

Schaefer's dichotomy theorem is proved by dividing CSPs into two types: those that can be reduced to one of a few specific problems in P, and the other to which SAT can be reduced (and so are NP-complete). Specifically, every CSP of the former type is either trivial (always satisfied by the constant 0 or the constant 1 assignment), can be reduced to 2SAT, ...


7

Local (stochastic) search is all about clever navigation of the search space. DPLL's advantage is pruning the search space of large swaths of assignments that provably cannot satisfy the formula. DPLL does this by incrementally building partial assignments (some variables assigned values, some left unassigned), applying the unit propagation and pure ...


7

It can be, but the solution process is equivalent to converting a CNF formula to DNF, which is NP-hard. You will at worst end up exploring an exponential number of disjunction branches.


7

Many better techniques for enforcing cardinality constraints are described in this answer. For the special case $y=1$, see also Encoding 1-out-of-n constraint for SAT solvers. Read those links; they suggest more efficient conversions, though I'm not aware of any reason to expect that they are necessarily optimal, so they don't answer your question about ...


7

Here's the relevant paragraph from the MiniSAT paper: The decision phase will continue until either all variables have been assigned, in which case we have a model, or a conflict has occurred. On conflicts, the learning procedure will be invoked and a conflict clause producted. The trail will be used to undo decision, one level at a time, until ...


7

Solvers that use the two-watched-literals algorithm to implement unit propagation don't keep track of which clauses have been deleted (by implication) to produce the subformula implied by the current partial assignment. By not tracking this information, solvers can avoid touching most of the clauses during assignments and avoid touching any of the clauses ...


7

Actually, probably you can't use a SAT solver to find another SAT solver, unless something surprising happens. If P = NP, then you can. If P = NP, then the polynomial hierarchy collapses (i.e., P = PH), so there is a polynomial-time algorithm for every problem in PH. The problem of asking whether there is a faster SAT solving algorithm is essentially a $\...


6

Both forward checking (FC) and arc consistency (AC) are methods of inference. Regardless of the problem you are solving, choosing a specific method of inference is always a tradeoff. Basically, the more you are willing to pay in terms of time, the more you gain in terms of strength of inference. So yes, it is faster to perform forward checking than arc ...


6

Your problem is the canonical $\Sigma_2^P$-complete problem: $$ \exists \vec{S} \forall \vec{A} \lnot F(\vec{A},\vec{S}). $$ As such, it is thought to be more difficult than SAT (which is $\Sigma_1^P$). Solving it with a few SAT-oracle calls is akin to solving SAT itself efficiently (the P vs. NP question), though it could be that $\Sigma_2^P = \Sigma_1^P$ ...


6

That's correct. DPLL exhaustively explores the space. If it returns 'unsat' then certainly no satisfying assignment exists. More recently, researchers have developed certifying SAT solvers that additionally return a (hopefully short) proof of unsatisfiability, when they return 'unsat'. This proof can be checked by anyone else, which provides a way for ...


5

I think your problem is not the algorithm itself but a few surrounding notions. A literal is a variable or its negation: $a$ or $\neg a$ for example. A clause is a disjunction of literals: $a \lor b$ A unit clause contains only one literal: $\neg a$ is an example The empty clause contains no literals and is written $\{\}$ or $()$ or $\Box$. The empty clause ...


5

It works because the three cases you mention will remove every non-pure variable after some number of steps, but it is crucial that you also consider the recursive step, namely $\mbox{dpll}(\phi \land l) \lor \mbox{dpll}(\phi \land \neg l)$. After a recursive step, you are guaranteed to have at least one unit clause, so the unit clause will be set to its ...


5

While the deductions made by $M$ can have equivalent (possibly exponentially bigger) resolution proofs, I'm not sure what you mean by translating the rule system of $M$ into resolution form. If $M$ has a rule saying that if the problem is a PHP (pigeonhole principle) problem then output unsat if number of pigeons > number of holes, how would you translate ...


5

A keyword you might be missing is completeness. In general, a search algorithm is said to be complete if it finds a solution given it exists (given enough time). In particular, DPLL is an example of a deterministic, complete search method.


5

You're asking two questions. I'll answer your first question. There's no simple answer. It depends on the structure of the problem. There are problems with millions of clauses that can be handled by a SAT solver. There are also problems with only tens of thousands of clauses (perhaps fewer) that can't be handled by SAT solvers. The number of clauses ...


4

It is always a good idea to first check out the Handbook of Satisfiability [1] (I guess it's not freely available, sorry). Here, Chapter 2 is titled "CNF Encodings". At the very least, the book provides literature references on the state of the art on the time of the writing, and you can expand your search through them. In addition, here and here are two ...


Only top voted, non community-wiki answers of a minimum length are eligible