why is it so common to talk about how SAT-solvers work _inside_, but there's almost no texts about how to work *with* them?
with all respect to Knuth's volume 4b (which felt like the only congregating text even touching the subject, when I looked into it some years ago) - but even his work doesn't go into loads of nooks and crannies of SAT encodings that gave invaluable speedups in specific contexts, so are useful as "ideas" - not as recipies
(and Knuth's descriptions of counters' encodings would've been greatly improved by pictures, imo)
It's a good question. I was asking something like this myself at lunch today.
Basically I think the issue is that SAT solvers accept stuff at a conjunctive normal form level, which is pretty far from what you'd want to use for most applications. It's more like an IR. So SAT solvers are more typically backends to higher level tools which compile to them.
If your tool offers a high level interface, one may be inclined to just call it an SMT solver. I too despite being interested in SAT, basically reach for an SMT solver even if my problem is pure boolean because of convenience.
- SAT/SMT by example is an excellent text https://smt.st/
- https://pysathq.github.io/ offers a nicer interface directly to SAT solvers
- Z3 https://microsoft.github.io/z3guide/docs/logic/intro/ can put problems into CNF and pretty print dimacs. It contains a SAT solver, but one would probably expect a purely boolean problem to do better on the top of the line SAT-only solver like Kissat.
Also MiniZinc, Gecode and OR-Tools are 3 ways of using SAT solvers that include good documentation and walkthroughs.
> If your tool offers a high level interface, one may be inclined to just call it an SMT solver. I too despite being interested in SAT, basically reach for an SMT solver even if my problem is pure boolean because of convenience.
Fortunately SMT solvers pass the problem into a SAT solver if they are simple enough, so you are probably not even trading away performance
Yurichev's SAT/SMT by Example [0] is a great (free!) resource for learning how to model problems to SAT/SMT
[0] - https://smt.st/
I second this as a good starting point. When I was picking up z3, this was helpful.
> loads of nooks and crannies of SAT encodings that gave invaluable speedups in specific contexts
This is such an incredibly important observation it bears repeating. You're also not the first to make it (e.g. "If the final goal is the practical solving of hard real world problems and not only to make solvers overcome inappropriate encodings by rediscovering in the CNF formulas some deductions that are obvious in the original problem, then a careful encoding is crucial and must be considered as a third type of contribution beside solvers and benchmarks in the challenges organized for SAT." [0]), which makes it even more frustrating that we still haven't really made much progress there.
I have worked fairly extensively with SAT and SMT solvers and the "design space exploration" of how best, exactly, to transform your problem into gates or CNF is a maddening time-sink with do-or-die implications. If you get it wrong, the solver will never terminate.
How long should you let the solver run before bailing out and trying a new approach? How do you systematically explore the design space when you're not sure if your problem is "difficult" enough to demand a 24h timeout or if it "ought to be solved" within a 6h timeout? Should I use one-hot encodings everywhere? Is XOR a problem? Maybe a different solver will be able to solve it? Can some re-jiggering with "fraig","strash", etc. voodoo in ABC give me better/more consistent/more solve-able queries?
It goes on and on. The lack of established or at least well-known design patterns for encoding a problem into SAT queries makes it difficult to employ SAT solvers in practice. It's mostly trial by error with limited, very delayed, frequently non-existent feedback. Further, the heuristic nature of SAT solvers makes it a crapshoot to get consistent performance on varied problems, even using the same encoding techniques.
With that said, here's some advice I wish I'd gotten when I started working with SAT:
- The most correlated variable with solver time is problem size.
- More simpler SAT queries is way better than fewer bigger SAT queries. If at all possible, figure out a way to break one giant SAT query into a composition of multiple smaller SAT queries.
- However, simpler, but bigger (more gates) logic often works better than small but fancy complicated logic, especially if you can avoid XOR. Use ripple-carry or carry-select adders, not parallel prefix adders.
- One-hot and unary encodings are worth a try. But they're not always better.
- If you have some non-standard component in your problem, like a cardinality constraint, look for bespoke SAT encodings for that component first, before designing your own. Indeed, for cardinality constraints specifically, you should probably use the design presented by Bailleux and Boufkhad in "Efficient CNF Encoding of Boolean Cardinality Constraints"[0].
- Most (all?) solvers ship with a terrible malloc() implementation. Recompile your solver with Google's gperftools TCMalloc for a significant speedup.
- Throw hardware at the problem. Multiple fast (in a single thread, don't care about total throughput) high-cache CPUs in a cluster can help explore the design space faster, and can be used at solving time to approach the problem from different angles (i.e. different random seed) and with different techniques (i.e. varying solver parameters). You can't easily parallelize SAT, but you can easily run SAT in parallel.
- Try a different level of abstraction. Do you have a bit-blasted SAT problem? Try encoding it in SMT. Do you have an SMT problem? Try bit-blasting it to a SAT problem.
- Optimizing your problem with Alan Mishchenko's excellent ABC can make an intractable problem tractable. It can also make a tractable problem intractable. It's worth fiddling with it, if you've no other recourse. Some command sequences I've found to work well are:
1. print_stats;strash;print_stats;drwsat;print_stats;fraig;print_stats;refactor -N 10 -lz;print_stats;&get -n;&dch,-pem;&nf;&put
2. print_stats;strash;print_stats;drwsat;print_stats;dch -S 1000000 -C 100000 -p;print_stats;fraig;print_stats;refactor -N 15 -lz;print_stats;dc2 -pbl;print_stats;drwsat;print_stats;&get -n;&dch -pem;&nf;&put
3. print_stats;strash;print_stats;fraig;print_stats;dc2 -l -b;print_stats;irw -l -z;print_stats;refactor -N 15 -z;print_stats;dch -S 50000 -C 10000;print_stats;dc2 -l;print_stats;fraig -C 10000;print_stats;drwsat -b;print_stats;irw -l -z;print_stats;refactor -N 15 -z;print_stats;dch -S 50000 -C 10000;print_stats;dc2 -l;print_stats;fraig -C 10000;print_stats;drwsat -b;print_stats;irw -l -z;print_stats;refactor -N 15 -z;print_stats;dch -S 50000 -C 10000;print_stats;dc2 -l;print_stats;fraig -C 10000;print_stats;drwsat -b;print_stats;irw -l -z;print_stats;refactor -N 15 -z;print_stats;dch -S 50000 -C 10000;print_stats;dc2 -l;print_stats;fraig -C 10000;print_stats;drwsat -b;print_stats;irw -l -z;print_stats;refactor -N 15 -z;print_stats;dch -S 50000 -C 10000;print_stats;dc2 -l;print_stats;fraig -C 10000;print_stats;drwsat -b;print_stats
[0]: https://www.cs.toronto.edu/~fbacchus/csc2512/Assignments/Bai...
Thank you, this is fascinating advice
The point of good CNF solver is that simple changes in encoding shouldn't give big and predictable performance jump, so you don't need to worry about encodings a lot.