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, ...


13

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-...


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 ...


11

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^...


10

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 ...


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 ...


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

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

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

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

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

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

A paper by Magnus Björk describes two techniques that could be worth trying. For 1-out-of-$n$, one can use both one-hot and binary encoding simultaneously. Thus, we have $x_1,\dots,x_n$ as a one-hot encoding, and $y_1,\dots,y_b$ as a binary encoding, where $b = \lg n$. We can encode the "at least one" constraint easily, in a single clause: $(x_1 \lor \...


5

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 ...


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

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

there are a lot of different angles on your question. generally agreed with your premise that looking at "structural information" in a SAT formulation ought to be an excellent research area. SAT encoded in CNF has been a standard for decades. it was solidified in the early-to-mid 1990s with the DIMACS format/ competitions. what technically is "structural ...


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 ...


5

TL;DR: They differ in their basic input and output. SAT and SMT solvers don't know what programs are; they are tools that answer yes or no questions about mathematical formulas. Symbolic execution, on the other hand, is a method of analyzing programs. Symbolic execution usually relies on SAT and SMT solvers, but not the other way around. SAT and SMT solvers ...


5

There are competitions for constraint satisfaction solvers. Some problems there can be readily translated to IP solvers as well. See e.g., MiniZinc challenge which has taken place yearly since 2008 or the XCSP competition.


5

There are no competitions targeting general integer programming or mixed integer programming, but there are (or were) benchmarks, such as the MIPLIB (linear) and the MINLPLIB (nonlinear). There are competitions for subsets (PB, SAT, max-SAT) and for constraint programming, as you and other answers pointed out. You can find many competitions (DIMACS ...


4

I'm not sure about the existence of practical multicore sat-solvers, but there are a few projects and papers: A Short Overview on Modern Parallel SAT-Solvers Asynchronous Multi-Core Incremental SAT Solving cmcSAT - A Cooperative MultiCore SAT Solver Improving SAT Solver Efficiency using a Cooperative Multicore Approach ManySAT: a Parallel SAT Solver (site) ...


4

Hint: Use a circuit for computing $\sum_{i=1}^n x_i$. Don't forget you're allowed to add variables!


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