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.
I'd love an article like this enumerating and explaining all the different techniques used, instead of just dumping them there. I don't mean CDCL, that is explained everywhere. I mean more advanced stuff like all the preprocessing and inprocessing techniques (e.g. bounded clause elimination), how to apply them efficiently, how to collaborate with a local search based solver (e.g. walksat), stuff like that.
I remember putting together a bibliography about standard techniques a few years ago: https://arxiv.org/abs/1802.05159
The majority of this article is scratch notes. How is this getting upvotes?
I am also a bit surprised, but happy that people find value here. Maybe just pretend the article ends before "bits and bobbles". Then it is just a short note on a brute force solver and a Davis Putnam solver. I like keeping my notes in my posts because it's useful for me to do so and helps psychologically with editing and scope creep. People have been able to interpret what I was getting at but didn't flesh out a lot more than I expect. Sometimes they explain a point that I mention I was confused on or wondering about in the notes section.
- [deleted]
Any suggestions for a good parallel open source SMT solver? It seems to me like contests are full of documentation-less entries that are setup to just run the contests and may or may not be generally usable.
https://github.com/domschrei/mallob I've seen talks by AWS where they claim that distributed SAT solving is very effective.
Do you need it to be parallel or just fast? My impression is that at the single machine level, it's hard to beat kissat and the CPU or GPU parallelism is not that useful. https://github.com/arminbiere/kissat
SAT/SMT isn't parallelizable. If it were it would be in P and you'd have P=NP.
That's patently false. For example, you can fix some variables on different instances, and run the solve with those variables fixed.
This doesn't result in really good work distribution, but it's a toy example.
> That's patently false.
Then you should file a patent? Or at least email Clay Institute about it because I believe (I'm not sure) there's a substantial prize associated with proving P=NP.
> For example, you can fix some variables on different instances
You can also parallelize stock picking by just picking stocks at random across multiple portfolios. Do you think I should patent this approach as a winning strategy?
It may well be that for some worst case instances of SAT/SMT that there is no parallel algorithm to solve them faster than a sequential algorithm unless P==NP.
But most people who are not complexity theorists (or perhaps cryptographers) are not generally interested in worst case instances, but are instead interested in solving practical problems which are often not (or even-- are practically never) worst case instances.
My own experience w/ real SMT problems is that I can usually home-brew a fair amount of parallelism by fixing some variables and then solving the derived problems w/ Z3 on each core. But the result often has fairly poor load distribution (e.g. some threads finish long before others), so it could obviously be done better by software the changes the variable its parallel on and how it distributes those variables adaptively as it goes.
> But the result often has fairly poor load distribution (e.g. some threads finish long before others), so it could obviously be done better by software the changes the variable its parallel on and how it distributes those variables adaptively as it goes.
It's astonishing to me that you're staring my point straight in the face and still not getting it. Let me restate in terms of portfolios: If I distribute my stock picks across many portfolios, without an oracle to tell me how to distribute them, some of the portfolios will perform poorly and some will perform well, but on average they will perform as if I just had a single portfolio.
I do wonder how we're talking past each other. Usually when I use an SMT solver I'm interested in finding a satisfying solution. Breaking up the problem on some variable the solver would search across multiple processors can improve the wall-time until finding one.
I doubt I'm following your metaphors/allusions, but the parallel may be that you're only hoping for any portfolio to have excess performance, and not the sum total.
- [deleted]
> I doubt I'm following your metaphors/allusions, but the parallel may be that you're only hoping for any portfolio to have excess performance, and not the sum total.
I'm sorry but I don't know how else to explain it to you when you're ignoring such an obvious fact: if you're hoping for any portfolio to hit big, but they're all picked without any intelligence (i.e., without an oracle) then you will always be only as good as the worst portfolio. It's just such a patently obvious logical argument I don't know how else to state it so that it becomes clearer. I mean I could easily write out the formula for expected value of the max of N uniform iid random variables but you've literally been witness to it by watching the wall-clock time on your threads!
Let me put it without any metaphors/allusions: you simply don't understand search and/or SAT if you think that dividing a 2^N search space into N pieces will give you a speedup. It will not. It's basically the "geometric" definition of NP.
Of course, dividing search space into K pieces is not guaranteed to give you a speed-up _in the worst case_: you might pick an unlucky division where K-1 pieces are easily UNSAT but the last remaining piece is as hard as the original (so the wall clock time is unchanged). However, in practice variable-fixing can and often does give an _expected time_ speed-up, especially if the SAT instance has some inherent parallel search structure (e.g., key or midstate bits for ciphers) and such heuristic tactics are still useful.
> However, in practice variable-fixing can and often does give an _expected time_ speed-up
Proof? Because as far as I know literally none of RP, BPP, ZPP relationships to NP are known.
Indeed no proof. By "in practice" I meant "on instances encountered in real-world applications."
then instead of _expected time_ you should say _hope-for time_ because _expected time_, in this context, is already firmly defined.
- [deleted]
I'm afraid I'm still mystified and suspect we must be talking past each other, ... But, in any case, I'm grateful you took your time to try teaching me something.
first of all, it's not P=NP - it would be NC=NP. If you nitpick, then at least do it right
and secondly, when "normal bloody people" talk about parallelizing, we don't mean exponential speedup - we mean using 4 cores in hopes of getting 3x time shrinking
and cube'n'conquer does exactly that - and have been the standard tool in SAT solving for forever
NC is a subset is P.
> mean using 4 cores in hopes of getting 3x time shrinking
I've already been over this: reducing 2^N by a factor of 3 is useless.
> I've already been over this: reducing 2^N by a factor of 3 is useless.
and here you're again showing your absence of practice and you being too much into theory
it's not useless if it transforms day computation into work-shift one
because actual people aren't working on theoretical infinite problems - people need solving specific examples they are stuck at
you sound like you'll enjoy working with galactic algorithms - too bad inter-universal beings aren't hiring right now