8
$\begingroup$

I have the following question. Is the SAT solvers are deterministic?

I mean, for example, about miniSAT and DPLL algorithm. Are they completely deterministic?

If these algorithms will return unSAT it means that certainly the solution does not exist?

$\endgroup$
14
$\begingroup$

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, which are are randomised algorithms whose output is always correct, but the algorithms 'gamble' with the resources used in the computation, e.g. running time on identical inputs may vary.

At the other extreme are probabilistic algorithms for solving $k$-SAT such as Schöning's [ 1 ] which is Monte-Carlo, and remarkably effective in practise given its utter simplicity. Interestingly Schöning's algorithm can be completely derandomised without losing (much of) its effectiveness [ 2 ].

In practise, industrial SAT-solvers always employ some degree of randomness, so as to 'escape' from the bad (= exponential) worst-case behaviour of DPLL-based algorithms. MiniSat is a highly configurable and evolving piece of software. That said, MiniSat is not completely deterministic: the choice of branching variable is sometimes randomised, depending on command line options. (The default is that 2% of branching variables are chosen randomly IIRC.) Likewise, MiniSAT has the option of initialising the VSIDS scores randomly. (VSIDS is a heuristic for 'measuring' the influence a variable has.)


  1. U. Schöning, A Probabilistic Algorithm for $k$-SAT Based on Limited Local Search and Restart.

  2. R. A. Moser, D. Scheder, A Full Derandomization of Schöning's $k$-SAT Algorithm.

$\endgroup$
  • $\begingroup$ Very nice references. $\endgroup$ – adrianN Jan 6 '17 at 9:55
  • $\begingroup$ does monte-carlo algorithm can say that a problem is SAT when it isn't, without solution of satisfability or it is just on the unSAT case, that the problem might be SAT ? $\endgroup$ – Xavier Combelle Jan 10 '17 at 17:40
  • $\begingroup$ @XavierCombelle That would depend on the specific algorithm, although I have a hard time thinking of an algorithm that could get SAT wrong. Schöning's gets only unSAT wrong. $\endgroup$ – Martin Berger Jan 10 '17 at 22:17
  • $\begingroup$ One minor extension -- while MiniSat using randomness, it is not "true" randomness. Every run of MiniSat will produce the same answer, in the same amount of time (if you do not reconfigure any options), as the same "random" choices are chosen each time the solver is run. $\endgroup$ – Chris Jefferson Apr 17 '17 at 17:41
  • $\begingroup$ @ChrisJefferson Doesn't MiniSAT have a way to specify a random seed? $\endgroup$ – Martin Berger Apr 18 '17 at 15:25
6
$\begingroup$

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 others to verify that the formula is unsatisfiable without them having to re-run the SAT algorithm again. This can be useful in some contexts.

MiniSAT is an implementation, rather than an algorithm. Its behavior depends on its code. I can't speak to what the code does.

$\endgroup$
  • $\begingroup$ All DPLL/CDCL solvers can be "augmented" to produce a proof of unsatisfiability. $\endgroup$ – Yuval Filmus Jan 6 '17 at 19:02
5
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

SAT solvers can be deterministic or not depending on how they are implemented. Note that the nondeterminism here can only affect the generated model not the answer (SAT or UNSAT) of the solver! For diversification purposes and others, SAT solver generally introduce randomness at certain point: for example to initialize variable activities or to make random decisions. In minisat for example, random decisions are made by calling a fonction that always return the same random number when using the same random seed. So at this point when you don't change any configuration of the solver, you will always have the same answer and the same model. Changing the random seed for example will not affect the answer (SAT or UNSAT) but can change the model and the execution time.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.