3
$\begingroup$

I came across Marijn Heule and Oliver Kullmann's paper on recent techniques in highly efficient SAT solvers. In particular they describe the Pythagorian Triple Problem, which they solved using that method one year earlier (a problem that was open for several decades, and had a monetary reward by Ronald Graham). Another famous example is the computer-aided special case solution for Erdős's discrepancy problem (before it was generally solved by Terence Tao).

I would like to know whether there is some comprehensive literature on techniques how to map some problems to SAT problems. Otherwise, I would also like to know other special solutions that have been achieved with SAT solvers, using a mapping from a problem in some field to boolean formulars. Are there special methods that are commonly used, or does one has to think about the mapping very specifically from problem to problem?

$\endgroup$
  • 2
    $\begingroup$ I think this might be more appropriate at the theoretical computer science stackexchange. $\endgroup$ – Noah Schweber Jul 12 at 22:30
  • 1
    $\begingroup$ See: cs.stackexchange.com/questions/30790/… $\endgroup$ – Bullet51 Jul 13 at 7:19
  • $\begingroup$ @NoahSchweber - given that SAT solvers are used to solve maths problems, TCS appears only tangentially relevant here (in particular due to "T" in "TCS" :-)). $\endgroup$ – Dima Pasechnik Jul 13 at 11:13
  • $\begingroup$ our limited experience is that often a straightforward reformulation might allow a SAT solver to do its magic. $\endgroup$ – Dima Pasechnik Jul 13 at 11:15
  • $\begingroup$ The Art of Computer Programming, Volume 4, Fascicle 6: Satisfiability (by Donald E. Knuth) is the obvious first place to look ... $\endgroup$ – KFabian Jul 14 at 19:43
5
$\begingroup$

I think it's very much specific to particular problems. The problem statement might be directly translatable into logic clauses, but for nontrivial problems it definitely helps if you formulate the problem in such a way that the SAT solver may handle it efficiently.

I might mention this paper in which Satisfiability Modulo Theory (SMT) solvers play a role in mapping logical constraints to Ising model Hamiltonians for a quantum annealer.

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