7 ms·
The Silent (R)evolution of SAT
- degoodm 3y ago"Is progress in SAT solving the sole result of hardware advancement? Time Leap Challenge compared 20-year-old SAT solvers on new computer hardware and modern SAT solvers on 20-year-old computer hardware. Although hardware improvements make old solvers faster, algorithmic progress dominates and drives today's SAT solving."* Pretty cool given computing progress over the last 20 years: 1. CPUs sped up 40-60x 2. GPU FLOPS/$ increased ~10,000x Sources: 1. https://www.cpubenchmark.net/year-on-year.html 2. https://en.wikipedia.org/wiki/FLOPS#Hardware_costs *Quote shortened for brevity
- sanxiyn 3y agoYou may want to read "A Time Leap Challenge for SAT Solving". It's just a really fun paper: https://arxiv.org/abs/2008.02215 https://arxiv.org/abs/2008.02215
- bmc7505 3y agoAnd yet, despite tremendous progress accelerating continuous optimization workloads, there are still no competitive GPU-based SAT solvers. I wonder why?
- GregarianChild 3y agoBecause all known SAT algorithms rely heavily on data-dependent branching based on non-local data. That makes the existing algorithms slow on GPUs. An algorithmic breakthrough is needed to change this.
- sanxiyn 3y agoIt's not just GPU. There are not even good multicore SAT solvers. State of the art SAT algorithms are serial and they don't parallelize.
- js8 3y agoYou could reduce to 2XSAT and presolve the linear portion. That would paralelize. I think people are not doing it because they are not aware of the reduction.
- adrianN 3y agoYou'd think that the handful of people who devote a significant fraction of their time to writing SAT solver would be aware of such simple tricks and there might be other reasons why your idea isn't being applied.
- js8 3y agoI would think so too, but I couldn't find this particular trick anywhere. Anyway, I believe it's similar to LP - we still use simplex method in practice, despite the fact that LP has a polynomial algorithm. What likely happens in SAT is even though there actually is (as I believe) a nice polynomial algorithm on the order of O(n^4) or so (which involves repeated solving of linear systems), the CDCL still wins in practical problems simply because in most cases, the upfront cost of solving the equations is higher than trying to find a first solution. However, not all hope is lost. You could actually presolve a more general problem, and then just rely on propagation to deal with a more specific instance. For instance, for integer factorization, you could presolve a general system for integers of certain bit size, and then if you wanted to factorize a specific integer, you would just plugin constants into the presolved instance. That would eliminate most of the upfront cost and bring it on par with CDCL. Unfortunately, DIMACS is not all that good format to represent SAT, because it is not composable like this - it doesn't allow for representation of presolved instances. But composability might be a win for a different types of algorithms, which do presolving.
- adrianN 3y agoIf you know a O(n^4) algorithm for SAT, I'm sure a couple of people would be interested in your paper.
- porcoda 3y agoSuper short answer: SAT doesn’t exhibit the nice properties other optimization problems often have where you can tell when you’re near a correct answer. So it doesn’t resemble most continuous optimization problems. Regarding parallelism, there has been research into parallel SAT, but it’s hard in part due to the problem of sharing information between threads/tasks in conflict clause learning algorithms. I don’t remember specific papers but a quick search on google scholar or looking at past SAT competitions would turn up material if you’re interested in the topic.
- bmc7505 3y ago> SAT doesn’t exhibit the nice properties other optimization problems often have where you can tell when you’re near a correct answer. You mean like a metric? Not all SAT instances have a natural metric, maybe a large fraction could be relaxed to MAXSAT, but it seems parallel solvers are not very popular in that setting either, i.e., there is no parallel track and parallel solvers are disqualified [1] from participating. I'm not sure I follow how metrics are related to parallelism though. A naive strategy would be to try every assignment in parallel on 2^n processors. There are plenty of better strategies for search space splitting [2] and stochastic local search [3] algorithms that seem amenable to parallelization. [1]: https://maxsat-evaluations.github.io/2023/rules.html https://maxsat-evaluations.github.io/2023/rules.html [2]: http://sat.inesc-id.pt/~ruben/papers/martins-ictai10-talk.pdf http://sat.inesc-id.pt/~ruben/papers/martins-ictai10-talk.pd... [3]: https://link.springer.com/article/10.1023/A:1006350622830 https://link.springer.com/article/10.1023/A:1006350622830
- calf 3y agon is like a million variables so you would need 2^n gazillion cores. I'm no expert but my thesis advisor is cited in the OP article, so I'm just guessing but it's an interesting question. It's not for the lack of trying in the part of SAT researchers; after the hardware advances with SAT solvers implementation in the early 2000s, they would've looked at parallelism and concurrency as well. But with continuous optimization (like with training machine learning), there's gradient descent which tells you where to guess next. But with Boolean logic there's nothing like that, the needle is either in the next bale of hay, or it isn't.
- cwzwarich 3y agoUnit propagation (a major component of CDCL-based SAT solvers) is P-complete, and thus has no effective parallel algorithm.
- bmc7505 3y agoInteresting. Do you have a link where I can read more about that? How does this relate to k-SAT or CNF complexity, isn't UP is complete w.r.t. these problems?
- zero_k 3y agoThere is a solver that can make effective use of GPUs (shameless self-promotion): https://github.com/nicolasprevot/GpuShareSat https://github.com/nicolasprevot/GpuShareSat It is a VERY fun work. Code entirely written by Nicolas Prevot, a magician of CUDA. Paper link here: https://comp.nus.edu.sg/~meel/Papers/sat21-psm.pdf https://comp.nus.edu.sg/~meel/Papers/sat21-psm.pdf
- bmc7505 3y agoOh you're one of the GPUShareSat guys, I forgot about that one. Would you say the main obstacle to scaling to a million processors is the synchronization overhead or are there certain instances from the SATComp benchmark that exhibited poor scaling with increased parallelism? Do you think sharing is essential or do you have any ideas how to improve communication-free strategies, i.e., parallelism without clause sharing using divide-and-conquer or randomized search? Six years ago, your co-author Mate wrote a very pessimistic remark on GPU-based SAT solvers here [1], I'm curious whether he still believes this or if his option was changed during the course of the project and what changed his mind? Thanks! [1]: https://news.ycombinator.com/item?id=13667565 https://news.ycombinator.com/item?id=13667565
- zero_k 3y agoHahha, I am Mate :) I still think that GPGPU can't help in the core of the algorithm. However, I was pleasantly surprised with Nicolas' work. He is a proper magician, and he had a great idea and made it work. Notice that he didn't make the GPU do propagation/conflict generation. Instead, he used it to better distribute clauses between the threads that do all of that. In a way, he improved clause cleaning. When I saw his work, I was very-very happy. I still hold that GPGPUs can't do CDCL. However, they may be helpful in some of its sub-parts, or may be able to run another algorithm for solving SAT that we haven't invented yet. Just my 2 cents, Mate
- thesz 3y agoGPU's are not friends with pointer chasing, which is the basis of contemporary CDCL solvers, because internal lazily-updateable structures are multi-linked lists. They are not friends with bottlenecks like clause queues used in contemporary stochastic SAT solvers. They can be good at something like survey and/or belief propagation [1]. [1] https://simons.berkeley.edu/talks/belief-survey-propagation https://simons.berkeley.edu/talks/belief-survey-propagation The problem is that survey/belief propagatin is effective in the area of random CNF problems and it is not a complete solution technique. It may compute a solution but it cannot provide you with the evidence that there is no soolution.
- bmc7505 3y agoMy hunch is that CDCL is probably the wrong approach to take for parallelization due to synchronization issues. You want an algorithm that is communication-free or makes belief propagation wall-clock competitive for large set of instances. It should be possible to modify BP to be asymptotically complete by using a special-purpose PRNG that ensures samples are drawn uniformly without replacement from the search space, but I'm not sure how to make it more sample-efficient.
- xavxav 3y agoA fun exercise is to write a series of sat solvers: brute force, DPLL and CDCL you really get an immediate feel for the strength of the algorithms and none of these implementations need to go much beyond 50-100 lines in a modern language. You can then of course spend months tuning and optimizing the hell out of your code to squeeze a further 10x performance. If you're really crazy like Sarek, you can also formally verify these implementations: https://sarsko.github.io/_pages/SarekSkot%C3%A5m_thesis.pdf https://sarsko.github.io/_pages/SarekSkot%C3%A5m_thesis.pdf
- philzook 3y agoExcellent link. I would love to see a CDCL implementation in a 100 (understandable) lines. From what I see in the repo, creusat is probably more like 1000?
- xavxav 3y agoIndeed, but CreuSAT is actually a high-performance implementation (ie: worst of the best), I should probably just write up a Rust gist of CDCL.
- GregarianChild 3y agoI found the description of CDCL as an abstract rewrite system illuminating. It's much shorter than an implementation. See e.g. [1]. There is/was a more readable version online, but I can't find it now. [1] https://easychair.org/publications/open/b7Cr https://easychair.org/publications/open/b7Cr
- aaw 3y agoThis one's 250 understandable lines: https://github.com/marijnheule/microsat https://github.com/marijnheule/microsat. You could probably get it to below 200 lines if you removed the restart logic and learned clause compaction, but it's actually a surprisingly competitive solver as is.
- ykonstant 3y agoWhat a lovely and well-written thesis; I am reading it with great interest.
- geysersam 3y agoParallelizing SAT solvers seems like a strikingly important avenue for future research.
- hgsgm 3y agoSimilar to faster-than-light travel.
- geysersam 3y agoReally? Does parallel algorithms for SAT contradict any known laws of physics?
- fooker 3y agoIt contradicts mathematics. :) Unit propagation is P complete.
- dgacmu 3y agoThat's not really a proof that we can't get a nice thing, though. SAT is NP-complete, but here we are talking about it. There may be ways to use parallelism at a higher level. And even if there isn't an alternative to unit propagation, a purely constant factor speedup with parallel processors isn't out of bounds and would still be fantastic.
- fooker 3y ago>a purely constant factor speedup with parallel processors isn't out of bounds and would still be fantastic. The state of the art with this is about 2x the speedup with an unbounded number of threads. That's not bad, but is not very useful because in most use cases of SAT you have multiple distinct problems solvable in parallel anyway.
- bmc7505 3y agoIsn’t UP complete with respect to CNF satisfiability though? How does P completeness relate to parallelizability of SAT?
- doetoe 3y agoI'm not an expert in any of these, but in the past few years, in addition to the success of LLM's for natural language processing, I have repeatedly read about the impressive advances in SAT solvers and in proof assistants. Given how impressive LLM's are in spite of their inability to reliably perform reasoning tasks or follow instructions with logical strictness, I wonder how much more impressive it could get if such systems got integrated
- sanxiyn 3y agoYou will enjoy "Maieutic Prompting: Logically Consistent Reasoning with Recursive Explanations". It prompts LLM to generate tree of explanations and run MAX-SAT solver over it: https://arxiv.org/abs/2205.11822 https://arxiv.org/abs/2205.11822
- doetoe 3y agoThanks, I'll check it out!
- deleted 3y ago[deleted]
- ComplexSystems 3y agoI don't really get why people think P≠NP anymore. I mean, isn't everyone expecting some kind of superintelligent AGI that can recursively improve itself to turn the planet into goo? Don't people think that this kind of AGI will get so good at nonlinear optimization that it will turn all humans into paperclips as a way to maximize the output of a paperclip factory? Why do we think that this insane next-level intelligence will somehow be able to do things like that, but not be able to figure out what pattern of bits gets a bunch of AND and OR gates to output a "1"? 10-15 years ago, the basic idea was "P≠NP because otherwise computers could do crazy shit." Well, looks like they can do crazy shit!
- adwn 3y ago> but not be able to figure out what pattern of bits gets a bunch of AND and OR gates to output a "1"? 10-15 years ago, the basic idea was "P≠NP because otherwise computers could do crazy shit." Well, looks like they can do crazy shit! I think you've fundamentally misunderstood the meaning of the P!=NP problem. In very simplified terms, it's not about what a computer can do, but about how long it takes to do something in the worst case.
- sirwhinesalot 3y agoThere already exist local-search based algorithms that can find solutions way faster than a SAT solver can... Or they get completely stuck unable to make any progress. All an LLM does is guess the next token based on the previous tokens and its training weights. For it to give you a solution to a large SAT problem it'll have to spit out a million character long binary string. The likelyhood most of that string will be entirely hallucinated is very high. LLMs are not magic. Deep Learning is already used internally in some SAT solvers to heuristically pick in which direction the search should go.
- ftxbro 3y ago> "10-15 years ago, the basic idea was "P≠NP because otherwise computers could do crazy shit." Everyone is downvoting you because that's not the mathematical explanation, but it's absolutely the informal explanation that the 'pop science' ones were saying.
- Hirrolot 3y agoI wonder what is the target audience of articles like this. I think the article is well-written, however 90-95% of the terminology make little or no sense to me who is not proficient in this field. Would the article be useful for someone who _is_ proficient in the field?
- bjarneh 3y ago> Would the article be useful for someone who _is_ proficient in the field? Yes, it is a very well written summary of what has been going on with SAT solvers in the last decades. I personally think most of this (r)evolution can be attributed to miniSAT. A relatively easy to read (at least compared to other theorem provers), free software implementation of a SAT solver, with instantiations if I remember correctly. Since variables only have two possible valuations (true/false) in boolean logic, they can be instantiated and the problem can be split up, and sometimes greatly simplified in doing so. I.e. we can replace each occurrence of variable 'a' with 'true' to make a new smaller problem, and then replace each occurrence variable 'a' with 'false' to make another smaller problem. I.e. split 1 problem into 2 simpler problems, and solve them in parallel etc.
- sanxiyn 3y agoAs I remember, Glucose was a larger advance than MiniSat. MiniSat was well-engineered but not exceptional. Glucose started as a hack, but the heuristic it introduced was so effective that you basically couldn't compete without copying it.
- bjarneh 3y agoYou could be correct. I haven't worked in academia for about 12 years; and I mostly worked on other types of logic. I do remember miniSAT being praised for its openness and readability, and it seems to predate the Glucose solver by some years. I.e. "in my day" miniSAT had all the praise, but perhaps Glucose was a more important contribution to the field.
- 3y ago
- vivegi 3y agoSAT is tantalizingly simple to describe and is an intense rabbit-hole if you are intellectually curious. I liked the article. The SAT Competition [1] is a good place to find state of the art. [1]: http://www.satcompetition.org/ http://www.satcompetition.org/
- xavxav 3y agoI wonder if they'll write a followup on the SMT revolution that happened after the CDCL breakthroughs for SAT. The lazy approach to SMT was a huge step forward, but itself spawned a whole lineage of refinements, alternatives and changed the state of automated reasoning entirely. A lot of work today seems to be going into theory combinations so that you can efficiently answer problems for example involve arrays and integers in a manner that has dependencies between the two. 'Solving' (it's an undecidable problem) SMT would open up a bunch of new possibilities..
- maweki 3y ago> it's an undecidable problem In what sense? People often use SMT (Satisfiability modulo theories) but don't state _which_ theories. I often SMT-solve with decidable theories, like Presburger Arithmetic.
- xavxav 3y agoI almost exclusively use it with quantifiers which makes it equivalent to FOL. But even without quantifiers, theory combinations can introduce undecidability. There’s the auxiliary problem that decidable but slow can often be equivalent to undecidable.
- zero_k 3y agoFor anyone who understands easier through code, I suggest: https://github.com/msoos/minisat-v1.14 https://github.com/msoos/minisat-v1.14 It's an early version of MiniSat by Niklas Eén and Niklas Sörensson. You can get the original ZIP from minisat.se, but it's easier to read from GitHub. Enjoy!
- andrewla 3y agoIncreasingly it seems that P=NP is not really all that interesting of a problem from a practical perspective. The progress made in various NP-Complete problems, SAT especially, shows that the vast majority of problem instances tend to be solvable, with the worst-case complexity problems being relatively rare but having much greater complexity cost.
- kqr 3y agoI keep asking this question and not getting satisfying answers so I'll try again: I'm sure I encounter problems every month that reduce to SAT (or SMT) and I could save a lot of time and energy (for both me and my computer) if I would just ask a SAT solver to find the answer instead of writing custom code each time. However, that thought never strikes me because I haven't gotten used to thinking about problems as SAT reducible. But since the thought never strikes me, I also don't get many opportunities to get used to that! How does one get started with incorporating SAT (or SMT) solving as a natural part of going about one's day?
- ufo 3y agoKeep your eyes open for problems where you have to do some form of brute-force search. Those that doesn't have a clear solution other than trying all the possibilities. Another thing is that the best kind of problem for SAT solvers are problems that ask a yes/no question. Is there a way to satisfy all the constraints, and if so what are the variable assignments that do so? It's also possible to use SAT solvers for other kinds of problems (e.g. find the solution with the best score) but it's more advanced.
- JonChesterfield 3y agoTry CSP instead. It works as as higher level abstraction over SAT that is easier to model with.