Modern SAT solvers: fast, neat and underused (2018)

CODINGNEST.COM
198
76
weird_user
4d

Comments

@jjoonathan 4d
I seem to recall that a poorly scaling sat solver in conda-forge broke so badly in 2020 that it shifted the tectonic plates underneath the entire academic python ecosystem away from conda and towards pip.

    Solving Environment | / - | \
@hackandthink 4d
Compiling Scala without a SAT solver is probably too difficult.

The CNF Converter is a gem.

https://github.com/scala/scala/blob/v2.13.5/src/compiler/sca...

@wenc 4d
* * *
@comfypotato 4d
But what do you mean “fast”? If your problem ends up on the steep side of the exponential curve, it’s going to take a while to solve.

I had a lot of fun making my own CDCL solver in Rust, and I’ve really enjoyed messing with Z3 for some theoretical computer science. On all of my explorations, there was a very tangible problem size beyond which the solve time was unusable.

In the case of Z3 with most real world problems, the typical problem size is beyond this limit.

@CalChris 4d
> ... modern SAT solvers are fast, neat and criminally underused by the industry.

Modern SAT solvers are fast, neat and criminally undertaught by the universities. Seriously, why isn't this taught at the undergraduate level in CS70 [1] discrete math type courses or CS170 [2] analysis of algorithms type courses?

[1] https://www2.eecs.berkeley.edu/Courses/CS70/

[2] https://www2.eecs.berkeley.edu/Courses/CS170/

@fsckboy 4d
SAT? I had to look it up, so...

Boolean satisfiability problem

https://en.wikipedia.org/wiki/Boolean_satisfiability_problem

"In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE."

@c0balt 4d
Just wanted to shoutout Armin Biere, one of the top contributors in this field: https://github.com/arminbiere

He has a few open source SAT solvers and tooling that provide good and proven examples on modern SAT solver techniques.

@justicz 4d
I really love the clarity + practicality of this article. Super well-written.
@joko42 3d
There was a time when people thought SAT and formal logic is the way to building AI. Now you don't hear anything about it. I wonder what happened?
@tgamblin 3d
Love this article and the push to build awareness of what modern SAT solvers can do.

It's worth mentioning that there are higher level abstractions that are far more accessible than SAT. If I were teaching a course on this, I would start with either Answer Set Programming (ASP) or Satisfiability Modulo Theories (SMT). The most widely used solvers for those are clingo [0] and Z3 [1]:

With ASP, you write in a much clearer Prolog-like syntax that does not require nearly as much encoding effort as your typical SAT problem. Z3 is similar -- you can code up problems in a simple Python API, or write them in the smtlib language.

Both of these make it easy to add various types of optimization, constraints, etc. to your problem, and they're much better as modeling languages than straight SAT. Underneath, they have solvers that leverage all the modern CDCL tricks.

We wrote up a paper [2] on how to formulate a modern dependency solver in ASP; it's helped tremendously for adding new types of features like options, variants, and complex compiler/arch dependencies to Spack [3]. You could not get good solutions to some of these problems without a capable and expressive solver.

[0] https://github.com/potassco/clingo

[1] https://github.com/Z3Prover/z3

[2] https://arxiv.org/abs/2210.08404, https://dl.acm.org/doi/abs/10.5555/3571885.3571931

[3] https://github.com/spack/spack

@yarg 3d
Has there been any effort to formalise the subset of NP that lends itself to SAT resolution (is there something between x^n and n^x)?

For example, what are the defining characteristics of a graphs for which the travelling salesman problem is resolvable without resorting to brute force?

@abecedarius 3d
FWIW, here's a little console-mode puzzle game of SAT problems, if you want to solve some manually. The "board" is not exactly like the example table in the post, since that one was for Sudoku in particular. This grid represents variables as rows and clauses as columns.

https://github.com/darius/sturm/blob/master/satgame.py (Python 2)

@AdieuToLogic 3d
> As an example, the often-talked-about dependency management problem, is also NP-Complete and thus translates into SAT[2][3], and SAT could be translated into dependency manager.

This reminds me of make[0] and of being made aware that make[0] is a SAT solver. I think it was when I attended a conference. Unfortunately I cannot find an authoritative source to quote, so will rely on, and be grateful to, the HN community to correct me should this be wrong.

0 - https://www.gnu.org/software/make/

@rojeee 3d
This brings back memories. In early 2000s, I wrote my undergrad thesis on a survey of SAT solving techniques. I believe the most capable general solver at the time was called DPLL and used a backtracking approach. My key insight at the time was that if you knew the "shape" of the SAT problem (you had domain specific insight) then you could take some shortcuts by using a custom algorithm. Eg this clause is always false and reduce the search space.
@bertman 3d
Related post (and highly recommended!) from yesterday:

The Silent (R)evolution of SAT https://news.ycombinator.com/item?id=36079115