9 ms·

SAT Solver Etudes I

45 points by mathgenius 2y ago

j2kun 2y ago
The majority of this article is scratch notes. How is this getting upvotes?
- deleted 2y ago
  [deleted]
- philzook 2y ago
  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.
NooneAtAll3 2y ago
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)
- rrampage 2y ago
  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/ https://smt.st/
  - abhgh 2y ago
    I second this as a good starting point. When I was picking up z3, this was helpful.
- philzook 2y ago
  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://smt.st/ - https://pysathq.github.io/ https://pysathq.github.io/ offers a nicer interface directly to SAT solvers - Z3 https://microsoft.github.io/z3guide/docs/logic/intro/ 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.
  - emmanueloga_ 2y ago
    Also MiniZinc, Gecode and OR-Tools are 3 ways of using SAT solvers that include good documentation and walkthroughs.
  - nextaccountic 2y ago
    > 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
- YetAnotherNick 2y ago
  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.
- kyboren 2y ago
  > 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/Bailleux-Boufkhad2003_Chapter_EfficientCNFEncodingOfBooleanC.pdf https://www.cs.toronto.edu/~fbacchus/csc2512/Assignments/Bai...
nullc 2y ago
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.
- philzook 2y ago
  https://github.com/domschrei/mallob 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 https://github.com/arminbiere/kissat
- almostgotcaught 2y ago
  SAT/SMT isn't parallelizable. If it were it would be in P and you'd have P=NP.
  - nullc 2y ago
    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.
    - almostgotcaught 2y ago
      > 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?
      - NooneAtAll3 2y ago
        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
Labo333 2y ago
I remember putting together a bibliography about standard techniques a few years ago: https://arxiv.org/abs/1802.05159 https://arxiv.org/abs/1802.05159
sirwhinesalot 2y ago
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.

SAT Solver Etudes I

45 points by mathgenius 2y ago

j2kun 2y ago

The majority of this article is scratch notes. How is this getting upvotes?

deleted 2y ago
[deleted]
philzook 2y ago
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.

NooneAtAll3 2y ago

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)

rrampage 2y ago
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/ https://smt.st/
- abhgh 2y ago
  I second this as a good starting point. When I was picking up z3, this was helpful.
philzook 2y ago
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://smt.st/ - https://pysathq.github.io/ https://pysathq.github.io/ offers a nicer interface directly to SAT solvers - Z3 https://microsoft.github.io/z3guide/docs/logic/intro/ 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.
- emmanueloga_ 2y ago
  Also MiniZinc, Gecode and OR-Tools are 3 ways of using SAT solvers that include good documentation and walkthroughs.
- nextaccountic 2y ago
  > 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
YetAnotherNick 2y ago
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.
kyboren 2y ago
> 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/Bailleux-Boufkhad2003_Chapter_EfficientCNFEncodingOfBooleanC.pdf https://www.cs.toronto.edu/~fbacchus/csc2512/Assignments/Bai...

nullc 2y ago

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.

philzook 2y ago
https://github.com/domschrei/mallob 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 https://github.com/arminbiere/kissat
almostgotcaught 2y ago
SAT/SMT isn't parallelizable. If it were it would be in P and you'd have P=NP.
- nullc 2y ago
  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.
  - almostgotcaught 2y ago
    > 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?
    - NooneAtAll3 2y ago
      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

Labo333 2y ago

I remember putting together a bibliography about standard techniques a few years ago: https://arxiv.org/abs/1802.05159 https://arxiv.org/abs/1802.05159

sirwhinesalot 2y ago

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.