Modern SAT solvers: fast, neat and underused

What would be a concrete problem you could solve with SAT solvers, besides the obvious &quot;satisfy this boolean expression&quot; (which doesn&#x27;t exactly come up every day)? Is it a useful tool for other NP-complete problems?<p>I mean, certainly you COULD reduce the Traveling Salesman Problem to SAT (it&#x27;s NP-complete, after all), but I would assume that it would be a totally impractical way of doing it compared to more specialized algorithms.<p>I&#x27;m asking since the title contains the word &quot;underused&quot;, but doesn&#x27;t elaborate on practical use-cases. What would you use it for?

The article does not mention it but &quot;symmetry breaking&quot;, a technique of exploiting symmetry to prune the search tree, can also be an important component of modern SAT solvers. In some sense one cannot do better than avoiding all symmetries in the given problem however that might come at significant computational price in practice.<p>Static symmetry breaking is performed as a kind of preprocessing, while dynamic symmetry breaking is interleaved with the search process. The static method has been used more but there are promising attempts to use dynamic symmetry breaking with CDCL solvers. See, for example, cosy (<a href="https:&#x2F;&#x2F;github.com&#x2F;lip6&#x2F;cosy" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;lip6&#x2F;cosy</a>) a symmetry breaking library which can be used with CDCL solvers.

At this year&#x27;s PyCon, Raymond Hettinger gave a talk about the very subject: <a href="https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=_GP9OpZPUYc" rel="nofollow">https:&#x2F;&#x2F;www.youtube.com&#x2F;watch?v=_GP9OpZPUYc</a>. I haven&#x27;t watched it yet, but knowing him, it will definitely be worth doing so.

I think the number one reason SAT Solvers are underutilized is because even relatively advanced programmers like me don&#x27;t have a particular clue how to frame their problems for a SAT solver.

Although modern SAT solvers has a ring to it, I wish we would go back to calling them high schoolers.

Can anyone help with what looks like SAT scalability problem? Is there a modern SAT solver that can do it? I was trying out Google SAT and it seems not to be able to scale to a simple school scheduling problem. Here’s the post with the code and test data <a href="https:&#x2F;&#x2F;groups.google.com&#x2F;forum&#x2F;m&#x2F;#!topic&#x2F;or-tools-discuss&#x2F;O8LZ9n__LVA" rel="nofollow">https:&#x2F;&#x2F;groups.google.com&#x2F;forum&#x2F;m&#x2F;#!topic&#x2F;or-tools-discuss&#x2F;O...</a>

Is there a standard book or lecture that explains the stuff like conflict clauses and literal watch? I see informal tutorials but something more fully explained, but not overly technical would be useful for people interested in applications. Just something in between blog posts and having to read the original technical papers.

okay, I&#x27;ll bite.. what&#x27;s a SAT, and why does it need to be solved? Am I a buffoon for thinking it&#x27;s the standardized test?

Why are people ITT talking about reducing problems to SAT? As I understand it, the point of reducing a problem to SAT is because there&#x27;s a proof that SAT is NP-Complete which in turn would prove that your problem is NP-Complete. But if you have some sort of industrial constraint satisfaction&#x2F;ASP&#x2F;scheduling&#x2F;search&#x2F;etc problem, you can solve it with whatever methods are available. You don&#x27;t have to reduce a problem in such and such domain down to a big Boolean formula and solve it via SAT techniques. Am I wrong?

What is the benefit of using a SAT solver directly instead of an SMT solver, other than tweaking for a bit better performance in the SAT solver?

Since I cannot find it mentioned in the OP nor in the comments: if you want to experiment with SAT, the pysat package might be a pretty good start.<p><a href="https:&#x2F;&#x2F;github.com&#x2F;pysathq&#x2F;pysat" rel="nofollow">https:&#x2F;&#x2F;github.com&#x2F;pysathq&#x2F;pysat</a><p>The API is not exactly Pythonic (numpy&#x2F;scipy&#x2F;opencv style) but it&#x27;s loaded with features.

&quot;and underused&quot;<p>Where does the article talk about this?

Stupid question... Are there equivalent (in the sense of being fast and having nice interfaces) solvers for #SAT problems? A whole pile of inference in machine learning can be framed in this way which makes me curious.

Is meta-learning still useful for SAT solving (e.g SATzilla)?

I thought it was an article on satellite signal for tv