27
$\begingroup$

I found some fascinating paper by Marijn Heule and Oliver Kullmann on advances in SAT solvers and automated reasoning. In particular, the authors where able to show (a year earlier) a breakthrough result on a decade old problem through automated reasoning, showing that state of the art tools on solving boolean satifyability problem are very powerful these days.

I am curious how Mathematica's SAT solver compares to these developments. Does Mathematica's function SatisfiableQ or SatisfiabilityInstances use clever techniques such as Conflict-Driven Clause Learning, look-ahead or Cube-And-Conquere?

The background of my question is the following: I am able to map certain hard problems to boolean formulars, and wonder whether it is immediatly worth learning these other techniques, or is Mathematica sufficently clever solving these systems (or is it basically trying with pure brute-force to find solutions?)

One useful previous answer by a Wolfram developer can be found here, which sets the stage for my question (which methods have been used 3 years ago, but not what explicit techniques and how they compare to state-of-the-art)

Improve this question
$\endgroup$
6
  • 5
    $\begingroup$ I am not very familiar with SAT solvers, but I did experiment with other solvers (such as glucose) when developing the graph colouring functionality of IGraph/M. Using them did not give a consistent or significant speedup compared to using Mathematica's. $\endgroup$
    – Szabolcs
    Commented Jul 14, 2019 at 12:56
  • $\begingroup$ But it should be easy to put problems into a conjunctive normal form, export them, and ty other SAT solvers. $\endgroup$
    – Szabolcs
    Commented Jul 14, 2019 at 12:59
  • $\begingroup$ Mathematica claims "industrial strength" Boolean computation so its SATSolver should be doing better than "brute force". On the other hand, SATSolvers tend to specialise on formulae type (satisfiable, unsatisfiable, random, etc) or available resources (time, space, parallelization) or especially, exploiting a domain's structure, so it might be optimistic to hope for leading-edge performance across the board (curiously, in Heule, Kullman and Marek’s breakthrough paper mentioned in the OP’s introduction, after colouring the natural numbers red and blue ... $\endgroup$
    – Ronald Monson
    Commented Jul 20, 2019 at 10:26
  • $\begingroup$ ... the SAT (CNF) instances that encode the unavoidablity of monochromatic pythagorean triples are reminiscent of random CNF formulae). To compare Mathematica’s SATSolver you could use the benchmarks provided in the 2018 SAT Competition where, given this competition’s history Maple’s SATSolver(s) seems to be laying down the gauntlet which might pique WRI’s interest … (Another indicator of state-of-the-art solvers is the ability to generate so-called DRAT proof files ... $\endgroup$
    – Ronald Monson
    Commented Jul 20, 2019 at 10:27
  • $\begingroup$ ... for use in verifying unsatisfiability claims but which seems absent as an option in SatisfiabilityInstances?). Alternatively, providing some benchmarks in the question would allow comparative answers - a natural starting point might be the paper’s SAT encodings generated by a WL-version of the (19-line C) encodings provided by the authors in the file Ptn-encode. $\endgroup$
    – Ronald Monson
    Commented Jul 20, 2019 at 10:28

0

Reset to default

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.