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...