6
$\begingroup$

For a graph theory problem I need to solve hundreds of millions of CNF problems that typically have around 200 variables and 15,000 clauses no larger than 10.

By default I use glucose, which usually takes a fraction of one second. However, in about one case out of a million, glucose doesn't want to finish and I don't see what is different about those cases.

I put one example here . There are 214 variables and 16466 clauses, which is small by the standards of the SAT competitions. I also ran it for more than 3 days in kissat without result.

An example of an easy CNF, slightly smaller but not by much is here . Both glucose and kissat take 4-5 seconds.

Incidentally both the hard and easy examples are unsatisfiable.

Any advice would be appreciated.

$\endgroup$
2
  • $\begingroup$ Could you also make one of the easy instances available? $\endgroup$
    – Kyle Jones
    Dec 18, 2021 at 18:26
  • $\begingroup$ @KyleJones Added. $\endgroup$ Dec 19, 2021 at 2:55

1 Answer 1

6
$\begingroup$

Why is this SAT problem hard?

A change in perspective may be helpful. It is expected that some SAT problems are extraordinarily hard: if the strong exponential time hypothesis is true, then for any SAT solver $A$, there are some specific formulas $\varphi$ that $A$ takes exponential time on. Plug in $A = \mathsf{glucose}$ or $\mathsf{kissat}$ to this statement, and you have chanced upon one such example $\varphi$. The fact this only occurs in 1 in a million cases is just a testament to how strong SAT solvers have become on average cases.

In fact, it is typically not hard to come up with formulas to stump even the best SAT solvers, and all SAT solver users encounter such formulas sooner or later. In my experience, this often happens when taking a sufficiently "mathematically complex" statement and encoding it as a SAT problem. For example, for a long time, the pigeonhole principle, when encoded directly into SAT, was very difficult for SAT solvers to figure out. (I know there was active research on the pigeonhole case, so it's possible that modern SAT solvers no longer suffer from that particular barrier.)

Regarding the number of variables and clauses: for "hard" instances $\varphi$, the time required to solve will be exponential in the number of variables and clauses. So you can't necessarily expect that just because there are a small number of variables or clauses, the problem will be tractable.

What can I do about it?

This one I have a much more positive answer for! Researchers working on SAT solvers typically love examples like this as they are very interesting case studies for improving their tools. So what you can and should do is:

  • Post the example publicly (you have already done this, but consider also posting it on, e.g. GitHub or Pastebin)

  • Share the example with the solvers you have tried as a hard instance, for example by posting an issue or by sending an email to active maintainers. Be sure to explain your use case/application to make the example interesting. You've already formed a more "minimal" instance, which is great as it will help them to isolate the difficulty.

Finally, the other thing you can do is try to leverage your own domain expertise to simplify the problem at formula generation time. As one example of an optimization to try, symmetry breaking can be very useful. That is, find an encoding of your graph theory problem which hardcodes constraints on the solution and avoids sources of exponential blowup in the number of cases to check.

$\endgroup$
1
  • 1
    $\begingroup$ One example of symmetry breaking in a graph theoretic problem is k-colorability. It's a good idea to find a large clique and precolor that, and let the solver work from there. $\endgroup$
    – Juho
    Dec 19, 2021 at 7:36

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.