NooneAtAll3 2 days 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)

  • philzook a day 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://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.

    • emmanueloga_ a day ago

      Also MiniZinc, Gecode and OR-Tools are 3 ways of using SAT solvers that include good documentation and walkthroughs.

    • nextaccountic a day 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

  • rrampage 2 days 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/

    • abhgh a day ago

      I second this as a good starting point. When I was picking up z3, this was helpful.

  • kyboren a day 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/Bai...

    • philzook a day ago

      Thank you, this is fascinating advice

  • YetAnotherNick a day 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.

sirwhinesalot a day 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.

j2kun 2 days ago

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

  • philzook 2 days 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.

nullc 2 days 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.

  • almostgotcaught a day ago

    SAT/SMT isn't parallelizable. If it were it would be in P and you'd have P=NP.

    • nullc a day 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 a day 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 17 hours 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

        • nullc a day ago

          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.

          • almostgotcaught a day ago

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

            • nullc 21 hours ago

              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.

              • almostgotcaught 21 hours ago

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

                • madars 19 hours ago

                  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.

                  • almostgotcaught 17 hours ago

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

                    • madars 16 hours ago

                      Indeed no proof. By "in practice" I meant "on instances encountered in real-world applications."

                • nullc 20 hours ago

                  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.