I 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?
"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
1. https://www.cpubenchmark.net/year-on-year.html
2. https://en.wikipedia.org/wiki/FLOPS#Hardware_costs
A 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
Excellent 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?
This one's 250 understandable lines: 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.
I 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.
Indeed, but CreuSAT is actually a high-performance implementation (ie: worst of the best), I should probably just write up a Rust gist of CDCL.
It's worth mentioning Mathias Fleury work who first verified a CDCL implementation [1]. He has written follow-up stuff.
What a lovely and well-written thesis; I am reading it with great interest.
You may want to read "A Time Leap Challenge for SAT Solving". It's just a really fun paper: https://arxiv.org/abs/2008.02215
And yet, despite tremendous progress accelerating continuous optimization workloads, there are still no competitive GPU-based SAT solvers. I wonder why?
GPU'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
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.
My 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.
Super 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.
> 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
[2]: http://sat.inesc-id.pt/~ruben/papers/martins-ictai10-talk.pd...
[3]: https://link.springer.com/article/10.1023/A:1006350622830
The 2^n idea is just a thought experiment, but you should be able to realize linear or close-to-linear speedup using a communication-free algorithm that shards the search space evenly across available cores, no? I don't see why this strategy isn't more widely used.
I can see how continuity accelerates the search for solutions, but I see that more as an orthogonal property, not a limitation of parallelism. Even if your domain is continuous, accelerating gradient descent is nontrivial, and many discrete optimizations problems benefit from parallelism.
No, parallel SAT solvers are NOT disqualified, in fact there is a parallel track. Seriously? Every year there is a winner for the parallel track. Here's last year's:
The difficulty is which variables to pick so that all subspaces are of comparable difficulty. Cube and conquer is a nice paper on that problem.
Using a naive splitting strategy is trivial, but ensuring the distribution is well-balanced across the subspaces is not. You need to preprocess the formula by setting the variables, then doing some propagation, then restarting, otherwise one core will get stuck doing a bunch of useless work.
There is a solver that can make effective use of GPUs (shameless self-promotion): 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
Oh 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!
It'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.
ManySAT: http://www.cril.univ-artois.fr/~jabbour/manysat.htm
It shares short conflict clauses between parallel solvers and achieves superlinear speedup in some cases, e.g., 4 parallel solvers solve faster than one forth of the single solver soolution time.
Short conflict clauses are rare so there is little communication between solvers required.
CryptoMiniSAT: https://github.com/msoos/cryptominisat
Author's goal to have solver that is good in computing range from single CPU up to cluster. Judging from CryptoMiniSAT successes, he has mostly reached the goal.
I was thinking there might be some theoretical barrier to parallelization, e.g., maybe naturally-arising SAT instances have poor empirical scaling constants [1], so sequential solvers with good branch heuristics are pretty close to optimal. There are some portfolio solvers (e.g., [2]) that have shown modest, but not dramatic speedups. Or maybe we just haven't tried hard enough.
You 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.
Because 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.
Unit propagation (a major component of CDCL-based SAT solvers) is P-complete, and thus has no effective parallel algorithm.
Interesting. 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?
Parallelizing SAT solvers seems like a strikingly important avenue for future research.
Similar to faster-than-light travel.
Really? Does parallel algorithms for SAT contradict any known laws of physics?
That'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.
Isn’t UP complete with respect to CNF satisfiability though? How does P completeness relate to parallelizability of SAT?
I 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..
> 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.
I 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.
For anyone who understands easier through code, I suggest:
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!
SAT 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.
I'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
You 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
Thanks, I'll check it out!
Increasingly 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.
I 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?
> 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.
As 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.
Glucose was a patch on minisat I think. So it couldn't have existed without minisat and its exceptional popularity. For a while there was even a category at the competition where entrants had to be small modifications of minisat.
That is true, but there are many interesting heuristics in modern SAT solvers, such as kissat: https://github.com/arminbiere/kissat (winner for a few years now). LBD ("glues" in glucose) is one of them. Kissat is actually quite readable. More readable is CaDiCaL, also extremely fast and effective: https://github.com/arminbiere/cadical
I personally also develop a SAT solver called CryptoMiniSat, but the above two are easier to read :)
You 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.
FWIW, Knuth's chapter on satisfiability mentions MiniSat once for historical interest and discusses Glucose heuristic for five pages. This matches my impression of their technical contributions.
It's not just you. I found the technical sections of the article impenetrable. And yet my background is on resolution theorem-proving (I did my PhD research on Inductive Logic Programming) and I read the article wishing to understand how CDCL is related to Resolution, but I couldn't figure that out.
I don't have a background in SAT solving but the "clause learning" in CDCL looks a lot like what we call a Resolution-derivation in Resolution theorem-proving. In short, given a conjunction of two (propositional or first order) clauses (¬φ ∨ ψ) ∧ (φ ∨ χ) Resolution eliminates the contradiction in the "complementary pair" (¬φ, φ) and derives the new clause ψ ∨ χ. If that's what CDCL folk call learning then that's really interesting to me because most of Inductive Logic Programming is an effort to use Resolution for inductive inference i.e. machine learning, but in logic. I guess I should check the article's bibliography. They reference s a textbook that might be useful ("Handbook of Satisfiability". Though one of the authors is an author of the article so that may not bode well for the textbook).
Conflict explanation in CDCL is entirely based around resolution, the idea being to take a conflicting set of clauses and apply resolution a bunch of times to “simplify” the conflict into its most general form.
If I understand correctly what "conflicting" means, that process can't possibly result in an empty clause, as in Resolution refutation proofs, correct?
What would be the gold standard reference for CDCL? Something that would be taught at an undergraduate class, say?
Edit: after reading a bit on the net it seems like clause learning in CDCL is basically Resolution-derivation by input Resolution. Cool beans.
The resolution is actually also what 2SAT algorithm is doing.
I like how the Wikipedia page on 2SAT explains the use of Resolution:
>> Resolution, a method for combining pairs of constraints to make additional valid constraints, also leads to a polynomial time solution.
"Constraints" being a slightly odd-sounding way to put it, to me anyway, but I guess that's because I don't have the relevant background to think of clauses that way.
The target audience is members of the acm. So that mostly includes computer science researchers, I guess.
I 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!
P != NP is more likely akin to a fundamental mathematical law, like Noethers theorem [0]. No amount of self improving AI will alter the fundamental laws of physics. More provincially, in our solar system, there's a cap on energy so that any system that uses it will eventually hit a ceiling (like a self improving AI that eats up energy resources at an exponential pace).
As motivation for why P != NP, one can think of it as a finite restatement of the Halting Problem [1] in the form of asking whether a (polynomially sized) Turing machine has an input that will halt in K steps.
> As motivation for why P != NP, one can think of it as a finite restatement of the Halting Problem
That's a really poor motivation. Analogically, you can think of the NP question as solving a polynomial equation over Z_2. What you're arguing is that because for Z the problem is unsolvable (due to DPRM theorem), then for Z_2, we have to try all the solutions.
That argument fundamentally ignores that the source of unsolvability is the infinite nature of Z.
For the record, I believe that P=NP (see https://news.ycombinator.com/item?id=35729626). I wish people spend more time looking for polynomial algorithm using logic approach, as I am doing (trying to extend the 2SAT and XORSAT proof to 2XSAT). This approach could give new algorithms that actually compose and can be paralelized (DIMACS is a really awkward representation).
Godels incompleteness theorem and the Halting problem are very nearly equivalent. I believe Turing, very soon after hearing about Godels' incompleteness theorem, used it to show the non-existence of the Halting problem. The consequences of Godel's incompleteness theorem and the Halting problem wove into many outstanding problems, including Hilbert's 10th problem.
I would argue that computation is a much more natural setting for thinking about these ideas. Whether is recursively enumerable sets, Diophantine equations or set theory doesn't fundamentally matter so much, as they're all equivalent in some way. I wouldn't argue that you, or anyone else, shouldn't think of it in that way, but in my opinion, for many people, myself included, casting it through a computational lens makes more sense.
Not to harp on a small point but I would argue the diagonalization proof of the Halting problem relies on there being different orders of infinity, not that Z itself is infinite. Since Godel's incompleteness, we know that the continuum hypothesis can be true or false depending on which (consistent) axioms you choose, so I would argue that it's not so much which axioms we choose for how we think about infinities that's fundamental but the fact that consistent systems of sufficient complexity must be incomplete.
I'm firmly in the P!=NP camp but I commend you for putting your beliefs out there and actually doing the work. I do believe people throw up their hands when they hear "NP-Complete" when they absolutely shouldn't. The path from problems being "easy" (polynomial) to "hard" (exponential) is not very well understood and even if a problem is, in general, NP-Complete doesn't mean that a particular ensemble of problems being drawn from couldn't be solved by some clever polynomial time algorithm.
And of course, P ?= NP still remains an open problem so we still don't understand something pretty fundamental.
The catch here is that P vs NP talks about worst-case behavior. Many SAT solver inputs can be solved quickly with good heuristics, but there are some that are still difficult no matter what you do. One way to see this is via the phase transition behavior of SAT.
https://www.researchgate.net/profile/Lavallee-Ivan/publicati...
If you have too few constraints it's easy to find a solution to the problem. If there are too many constraints it's also easy to show there are no solutions. But in the middle there's a sweet spot in the ratio of constraints to variables that's when the problem becomes fiendishly difficult.
There 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.
> "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.
I don't think it was the informal explanation ever. People think that P≠NP, because they tried it hard, and did not find any NP-hard problem in P.
> "People think that P≠NP, because they tried it hard, and did not find any NP-hard problem in P."
That was the informal explanation given to the computer scientists. But that's not so convincing to non computer scientists and it's not the informal 'pop science' explanation.
An example (not the only one) of the kind of 'pop science' explanation I mean, is Impagliazzo's Five Worlds (https://gwern.net/doc/cs/cryptography/1995-impagliazzo.pdf). One of those hypothetical worlds he called 'Algorithmica' and it's where P = NP. One of the amazing and outlandish things that could be accomplished in such an exotic world would be the following feat: "Thus, a computer could be taught to recognize and parse grammatically correct English just by having sufficiently many examples of correct and incorrect English statements, without needing any specialized knowledge of grammar or English."
It's not so wild to me, to think that if someone's understanding of P vs. NP was from that kind of pop science article, then they would think we should start considering more seriously that we are in the Algorithmica (P = NP) world where such feats are possible!
Thank you. I stand corrected, people indeed argued "10-15 years ago, the basic idea was "P≠NP because otherwise computers could do crazy shit." (1 person at least).
If P = NP because there's a O(N^{Graham's Number}) polynomial algorithm - a 'galactic algorithm' indeed - then the lay description is theoretically correct, but meaningless in practice.
In particular, the hand-waving is the phrase 'sufficiently many examples.' This may be impossible to provide even if only a googol (10^100) examples are needed, because of mass and energy limitations of the universe - there's only so much you can do with 10^80 atoms, and the speed of light is too slow.
"Only a googol" because Graham's Number is mind-boggingly huge - https://en.wikipedia.org/wiki/Graham%27s_number
The Wikipedia entry for "galactic algorithm" at https://en.wikipedia.org/wiki/Galactic_algorithm even mentions SAT: "a hypothetical large but polynomial O(n^2^100) algorithm for the Boolean satisfiability problem, although unusable in practice, would settle the P versus NP problem".
Algorithmica may therefore be very little different than our world, other than that people no longer debate if P = NP.
Informal, as in, poorly-researched clickbait pop-science. Most of the serious pop-science sources (Scientific American, Quanta Magazine, Computerphile, etc.) have explained it correctly, without restoring to woo.
> 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.
> isn't everyone expecting some kind of superintelligent AGI that can recursively improve itself to turn the planet into goo?
I most certainly am not.
Keep 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.
Try CSP instead. It works as as higher level abstraction over SAT that is easier to model with.
Right, SAT can sometimes be thought of as the assembly language of discrete optimisation.