20 ms·
Modern SAT solvers: fast, neat and underused (2018)
- comfypotato 3y agoBut what do you mean “fast”? If your problem ends up on the steep side of the exponential curve, it’s going to take a while to solve. I had a lot of fun making my own CDCL solver in Rust, and I’ve really enjoyed messing with Z3 for some theoretical computer science. On all of my explorations, there was a very tangible problem size beyond which the solve time was unusable. In the case of Z3 with most real world problems, the typical problem size is beyond this limit.
- xavxav 3y agoZ3 is actually not a particularly good SAT solver, you really want to use a dedicated tool for pure SAT problems. On the other hand if your problem is in a richer class like QBF or SMT then z3 shines and often you can use encoding tricks to scale problems significantly
- hackandthink 3y agoCompiling Scala without a SAT solver is probably too difficult. The CNF Converter is a gem. https://github.com/scala/scala/blob/v2.13.5/src/compiler/scala/tools/nsc/transform/patmat/Solving.scala#L50 https://github.com/scala/scala/blob/v2.13.5/src/compiler/sca...
- rwmj 3y agoCan you expand a bit on why / which bits of Scala compilation this is used for?
- hackandthink 3y agoIt is used for pattern matching. I don't know anything about the Scala compiler. A few years ago I needed a CNF Converter and I ripped their Logic Module. (performant CNF Converter are harder to find than SAT Solver)
- rwmj 3y agoNice idea! The pattern matching compiler/optimizer in OCaml doesn't do this. It's implemented using this algorithm which I've attempted to understand a few times but is a bit beyond me: Fabrice Le Fessant, Luc Maranget, Optimizing Pattern-Matching ICFP'2001 http://pauillac.inria.fr/~maranget/papers/opat/ http://pauillac.inria.fr/~maranget/papers/opat/
- wenc 3y agoConda uses a SAT solver. It is still very slow on degenerate cases and I’m not sure if work to replace it with Microsoft’s SAT solver has started. https://www.anaconda.com/blog/understanding-and-improving-condas-performance https://www.anaconda.com/blog/understanding-and-improving-co...
- jjoonathan 3y agoI seem to recall that a poorly scaling sat solver in conda-forge broke so badly in 2020 that it shifted the tectonic plates underneath the entire academic python ecosystem away from conda and towards pip. Solving Environment | / - | \
- teruakohatu 3y agoConda is still unbearably slow. Mamba is a vastly better mostly drop-in replacement.
- ubj 3y agoSecond this. Not only is it faster, but the error messages in Mamba are much more helpful and sane.
- rowanG077 3y agoGreat! Conda honestly can't die fast enough.
- taeric 3y agoThat was always a bit of a red herring, from my understanding. Yes, if you poorly model something into an ad hoc SAT solver, expect slowness. Which is a bit of the general idea of these being underused. If you can get your problem into a SAT form or three, than feed it to a state of the art solver, it can work amazingly well. But, you will be spending a lot of time moving to and from the SAT formulation.
- CalChris 3y ago> ... modern SAT solvers are fast, neat and criminally underused by the industry. Modern SAT solvers are fast, neat and criminally undertaught by the universities. Seriously, why isn't this taught at the undergraduate level in CS70 [1] discrete math type courses or CS170 [2] analysis of algorithms type courses? [1] https://www2.eecs.berkeley.edu/Courses/CS70/ https://www2.eecs.berkeley.edu/Courses/CS70/ [2] https://www2.eecs.berkeley.edu/Courses/CS170/ https://www2.eecs.berkeley.edu/Courses/CS170/
- deleted 3y ago[deleted]
- tanx16 3y agoThis is… not true. CS170 specifically teaches about reducing NP problems to SAT (you can find this in the Algorithms textbook linked in the class syllabus). I recall solving one of the projects by using MiniSat after converting a problem to 3-SAT. FWIW, the textbook is excellent and the course was very useful.
- deleted 3y ago[deleted]
- deleted 3y ago[deleted]
- tgamblin 3y agoI definitely recall doing reductions from SAT in Algorithms courses. I think that is a common part of most curricula. I don't recall being taught any practical uses of SAT. It was introduced only in the context of Cook's theorem, as the problem you needed to reduce to other problems in order to show NP-completeness. I think most people now learn SAT in that theoretical context, not as a tool to solve problems.
- dataflow 3y ago> I definitely recall doing reductions to SAT in Algorithms courses. > It was introduced only in the context of Cook's theorem, as the problem you needed to reduce other problems to in order to show NP-completeness. Are you referring to reductions from SAT, or to SAT? You seem to be mentioning both?
- c0balt 3y agoJust wanted to shoutout Armin Biere, one of the top contributors in this field: https://github.com/arminbiere https://github.com/arminbiere He has a few open source SAT solvers and tooling that provide good and proven examples on modern SAT solver techniques.
- justicz 3y agoI really love the clarity + practicality of this article. Super well-written.
- fsckboy 3y agoSAT? I had to look it up, so... Boolean satisfiability problem https://en.wikipedia.org/wiki/Boolean_satisfiability_problem https://en.wikipedia.org/wiki/Boolean_satisfiability_problem "In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE."
- hackernewds 3y agoAh I thought initially that these were solving SAT questions. Easy to make mistake, or perhaps just me.
- balls187 3y agoNo, I also had no idea about this type of problem and immediately thought this article was about the placement tests administered in the US.
- joko42 3y agoThere was a time when people thought SAT and formal logic is the way to building AI. Now you don't hear anything about it. I wonder what happened?
- deleted 3y ago[deleted]
- jasonwatkinspdx 3y agoThe "AI Winter" was largely caused by people realizing building better logic, chess, or similar analytical engines proves to be a poor model for human like intelligence. The current renaissance is due to Machine Learning / Deep Learning based essentially on statistical models. In the specific context of language there was a famous debate between Chompsky and Norvig that touches on these themes: http://norvig.com/chomsky.html http://norvig.com/chomsky.html I believe events of recent years have not been kind to Chompsky's side of this debate. I'm less bullish on large language models turning into AGI than many people here, but I think if we do develop AGI it's a certainty it will be a based on probabilistic models, not logically consistent formalisms alone.
- andrepd 3y agoBut also not probabilistic models alone, that's the point.
- yarg 3y agoIt requires large amounts of formalised and human defined domain specific knowledge, for every domain that you work with. The overheads are huge, and it's very bad at dealing with fuzzy situations.
- abecedarius 3y agoFWIW, here's a little console-mode puzzle game of SAT problems, if you want to solve some manually. The "board" is not exactly like the example table in the post, since that one was for Sudoku in particular. This grid represents variables as rows and clauses as columns. https://github.com/darius/sturm/blob/master/satgame.py https://github.com/darius/sturm/blob/master/satgame.py (Python 2)
- tgamblin 3y agoLove this article and the push to build awareness of what modern SAT solvers can do. It's worth mentioning that there are higher level abstractions that are far more accessible than SAT. If I were teaching a course on this, I would start with either Answer Set Programming (ASP) or Satisfiability Modulo Theories (SMT). The most widely used solvers for those are clingo [0] and Z3 [1]: With ASP, you write in a much clearer Prolog-like syntax that does not require nearly as much encoding effort as your typical SAT problem. Z3 is similar -- you can code up problems in a simple Python API, or write them in the smtlib language. Both of these make it easy to add various types of optimization, constraints, etc. to your problem, and they're much better as modeling languages than straight SAT. Underneath, they have solvers that leverage all the modern CDCL tricks. We wrote up a paper [2] on how to formulate a modern dependency solver in ASP; it's helped tremendously for adding new types of features like options, variants, and complex compiler/arch dependencies to Spack [3]. You could not get good solutions to some of these problems without a capable and expressive solver. [0] https://github.com/potassco/clingo https://github.com/potassco/clingo [1] https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3 [2] https://arxiv.org/abs/2210.08404 https://arxiv.org/abs/2210.08404, https://dl.acm.org/doi/abs/10.5555/3571885.3571931 https://dl.acm.org/doi/abs/10.5555/3571885.3571931 [3] https://github.com/spack/spack https://github.com/spack/spack
- BorisTheBrave 3y agoDo you have a recommendation for how to get into ASP? I've read the clingo docs, but it has never clicked.
- tgamblin 3y agoI read Potassco's Answer Set Solving in Practice book [0] but it's pretty dense. I suspect it would be easier to digest if you read it while also following their course materials, which are all online [1]. These days I recommend people start with the Lifschitz book [2] and read through the Potassco book [0]. Lifschitz's book is a much gentler introduction to ASP and logic programming in general and its examples are in ASP code (not math). It's also more geared towards the programming side than the solving side, which is probably better for most people until they really want to understand what clingo/gringo/clasp are doing and what their limitations are. There are other more applied courses, like Adam Smith's Applied ASP course at UCSC [3]. The problems in that course look like a lot of fun. [0] https://potassco.org/book/ https://potassco.org/book/ [1] https://teaching.potassco.org https://teaching.potassco.org [2] https://www.cs.utexas.edu/users/vl/teaching/378/ASP.pdf https://www.cs.utexas.edu/users/vl/teaching/378/ASP.pdf, https://www.amazon.com/Answer-Set-Programming-Vladimir-Lifschitz/dp/3030246574 https://www.amazon.com/Answer-Set-Programming-Vladimir-Lifsc... [3] https://canvas.ucsc.edu/courses/1338 https://canvas.ucsc.edu/courses/1338
- yarg 3y agoHas there been any effort to formalise the subset of NP that lends itself to SAT resolution (is there something between x^n and n^x)? For example, what are the defining characteristics of a graphs for which the travelling salesman problem is resolvable without resorting to brute force?
- api 3y agoDoes't Rust use a SAT solver for aspects of its type system?
- AdieuToLogic 3y ago> As an example, the often-talked-about dependency management problem, is also NP-Complete and thus translates into SAT[2][3], and SAT could be translated into dependency manager. This reminds me of make[0] and of being made aware that make[0] is a SAT solver. I think it was when I attended a conference. Unfortunately I cannot find an authoritative source to quote, so will rely on, and be grateful to, the HN community to correct me should this be wrong. 0 - https://www.gnu.org/software/make/ https://www.gnu.org/software/make/
- rojeee 3y agoThis brings back memories. In early 2000s, I wrote my undergrad thesis on a survey of SAT solving techniques. I believe the most capable general solver at the time was called DPLL and used a backtracking approach. My key insight at the time was that if you knew the "shape" of the SAT problem (you had domain specific insight) then you could take some shortcuts by using a custom algorithm. Eg this clause is always false and reduce the search space.
- scg 3y agoMirror: https://web.archive.org/web/20230108202435/https://codingnest.com/modern-sat-solvers-fast-neat-underused-part-1-of-n/ https://web.archive.org/web/20230108202435/https://codingnes...
- ur-whale 3y agohttps://archive.is/zE6eQ https://archive.is/zE6eQ
- bertman 3y agoRelated post (and highly recommended!) from yesterday: The Silent (R)evolution of SAT https://news.ycombinator.com/item?id=36079115 https://news.ycombinator.com/item?id=36079115
- andrepd 3y agoAnd they've only evolved since then! Take a look at SAT COMP, to see the year-on-year evolution of the field.