I'm looking for a collection of SAT problems that are usable for a test suite, i.e.:

  1. are small/easy to solve, that is, this is not a benchmark but a correctness test suite
  2. some satisfiable, some unsatisfiable
  3. answer and a possible assignment (for sat. ones) is known

All I find online are collections of benchmarks but heavy formulas are not what I need.

Any link?

  • 1
    $\begingroup$ Generate such a collection yourself by generating random SAT formulas of the correct density, and using a known SAT solver do determine the correct answer (or even just exhaustive search). If you use the correct density, then you will get both positive and negative instances. Alternatively, you can choose a density in which most instances are negative and generate planted instances (in which some particular truth assignment is guaranteed to be satisfying). $\endgroup$ Dec 31, 2020 at 14:15
  • $\begingroup$ Thanks! How do I generate instances of a given density? $\endgroup$ Dec 31, 2020 at 14:18
  • $\begingroup$ Density is the ratio between the number of clauses and the number of variables, fixing the width of the clauses. I imagine that you know how to generate 3CNFs on $n$ variables with $m$ clauses. $\endgroup$ Dec 31, 2020 at 14:19
  • 1
    $\begingroup$ In addition to Yuval's suggestion of randomly generating k-SAT formulae and taking density as a parameter, it might be worth pointing out that k-SAT densities exhibit a sharp phase transition. if your density is not close to the phase transition density, it is typically trivial to solve, almost all hard cases are at the the phase transition density. $\endgroup$ Dec 31, 2020 at 17:39
  • 2
    $\begingroup$ There are plenty of collections of small SAT formulae online, e.g. https://www.cs.ubc.ca/~hoos/SATLIB/benchm.html. $\endgroup$ Dec 31, 2020 at 17:43


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.