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