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?

Improve this question
$\endgroup$
5
  • 3
    $\begingroup$ I think this might be more appropriate at the theoretical computer science stackexchange. $\endgroup$
    – Noah Schweber
    Commented Jul 12, 2019 at 22:30
  • 1
    $\begingroup$ See: cs.stackexchange.com/questions/30790/… $\endgroup$
    – LeechLattice
    Commented Jul 13, 2019 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
    Commented Jul 13, 2019 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
    Commented Jul 13, 2019 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$
    – Karl Fabian
    Commented Jul 14, 2019 at 19:43

2 Answers 2

Reset to default
6
$\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.

Improve this answer
$\endgroup$
1
$\begingroup$

In addition to Knuth's book, another useful resource is the Handbook of Satisfiability, especially its 2nd chapter, which discusses some simple best practices for SAT encodings.

A lot of the success solving the Pythagorean Triples Problem has to do not as much with the encoding itself (which in this case is quite straightforward) as with skilled use of efficient parallelization, which is very hard for SAT. The method used is called Cube-and-Conquer, and has its own chapter in the Handbook of Parallel Constraint Reasoning.

I'm afraid that even with all this, making a SAT encoding work well is still a bit of an art, and requires a lot of trial and error (I say this as a person who after writing this answer will go back to fiddling with SAT encodings for work).

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .