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?

  • 1
    $\begingroup$ Maybe migrate to computer science? $\endgroup$ – probably_someone Jan 5 '17 at 23:02

Satisfiability (of systems of propositional formulae) is a decidable problem. The relevant SAT solving algorithms like DPLL are complete: they always terminate with a correct yes/no answer about satisfiability. SAT solver implementations should always either return a correct answer or run out of time or memory or some other resource (like the user's patience). An implementation might be non-deterministic about its failure or termination modes, but if it runs to completion with an answer, the implementor would consider it to be a bug if the answer was unSAT for a satisfiable system or SAT for an unsatisfiable system. If you want more details, I suggest you ask for more information on computer science stack exchange or on forums for particular SAT solvers of interest to you.


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.