12 ms·
Modern SAT solvers: fast, neat and underused
- ar_xiv 7y agookay, I'll bite.. what's a SAT, and why does it need to be solved? Am I a buffoon for thinking it's the standardized test?
- sourceless 7y agohttps://en.wikipedia.org/wiki/Boolean_satisfiability_problem https://en.wikipedia.org/wiki/Boolean_satisfiability_problem
- petters 7y agoIt means satisfiability problem. You can think of it as one "assembly language" of optimization, in the sense that many higher-order problem formulations can be "compiled" to SAT.
- ar_xiv 7y agothanks
- mlevental 7y agohmm I wonder if the article about SAT solvers defines them? https://codingnest.com/modern-sat-solvers-fast-neat-underused-part-1-of-n/ https://codingnest.com/modern-sat-solvers-fast-neat-underuse...
- city41 7y agoTo be fair it took me a bit realize this was part 3 of a series. It would have made more sense to post part 1 to HN.
- OskarS 7y agoWhat would be a concrete problem you could solve with SAT solvers, besides the obvious "satisfy this boolean expression" (which doesn't exactly come up every day)? Is it a useful tool for other NP-complete problems? I mean, certainly you COULD reduce the Traveling Salesman Problem to SAT (it's NP-complete, after all), but I would assume that it would be a totally impractical way of doing it compared to more specialized algorithms. I'm asking since the title contains the word "underused", but doesn't elaborate on practical use-cases. What would you use it for?
- maxmunzel 7y agoAs its applicable to all discrete Problems (think of Sudoku), its a really neat skill to have. Reductions are pretty easy to write and modern SAT solvers are crazy fast.
- thanatropism 7y agoIt's not difficult to reduce scheduling problems that are usually done with dynamic programming etc. to SAT. Then there's SATPLAN. If I had VC money I would be seeking young'uns trying to change the world with SATPLAN, of course in a way that's married to machine learning. (Machine learning doesn't "think", it "learns"; logic-based AI "thinks" but can't "learn"). E: part 1 says at the outset: > 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. The problem our group worked on, generating key and lock cuttings based on user-provided lock-chart and manufacturer-specified geometry, is also NP-complete.< Part 3 is already deep in the rabbit hole of comparing heuristics. People like me just write something that "compiles" to DIMACS and fires Minisat.
- 6gvONxR4sf7o 7y agoA primary problem in marrying logic to ML is doing so in a differentiable way. i.e. when your SAT part of the system is suboptimal, how do you know which parameters of the learned part to change, and in which direction?
- nl 7y agoWe propose Differentiable Satisfiability and Differentiable Answer Set Programming (Differentiable SAT/ASP) for multi-model optimization. Models (answer sets or satisfying truth assignments) are sampled using a novel SAT/ASP solving approach which uses a gradient descent-based branching mechanism. https://arxiv.org/abs/1812.11948 https://arxiv.org/abs/1812.11948
- smallnamespace 7y agoFrom the article, a lot of the heuristics seems to revolve around and 1) which variables to try first 2) which learned clauses to keep in your set. Assign scores and differentiate on those scores. This is (very loosely) how AlphaGo also works - you take a tree-based algorithm (MCTS) and then use neural nets to score the next node to expand.
- anjc 7y agoIs meta-learning still useful for SAT solving (e.g SATzilla)?
- projectramo 7y agoAlthough modern SAT solvers has a ring to it, I wish we would go back to calling them high schoolers.
- Wistar 7y agoYes. Isn't this what has Felicity Huffman is facing a prison sentence?
- flatfilefan 7y agoCan anyone help with what looks like SAT scalability problem? Is there a modern SAT solver that can do it? I was trying out Google SAT and it seems not to be able to scale to a simple school scheduling problem. Here’s the post with the code and test data https://groups.google.com/forum/m/#!topic/or-tools-discuss/O8LZ9n__LVA https://groups.google.com/forum/m/#!topic/or-tools-discuss/O...
- maweki 7y agoIn the worst case we can't get around exponential runtime in the problem size. This is problematic since encoding often is not even linear but quadratic or worse. But there are often tricks to get to encoding to nlogn size. Problems that are "hard" are usually specially crafted (SAT competition). Getting back to your question: In practice most problems do not show exponential runtime behaviour. Using a good SAT solver is key here since the more naive an implementation is, the more probable it is to run into exponential runtime with practical problems.
- flatfilefan 7y agoThanks. Is there such a good SAT solver you would recommend to try out?
- thijsvandien 7y agoAt this year's PyCon, Raymond Hettinger gave a talk about the very subject: https://www.youtube.com/watch?v=_GP9OpZPUYc https://www.youtube.com/watch?v=_GP9OpZPUYc. I haven't watched it yet, but knowing him, it will definitely be worth doing so.
- gloflo 7y agoIt is! He ran out of time a bit I think, at least it felt quite rushed at times, but I was left very curious and motivated to try some SAT.
- dtornabene 7y agowow, thanks for this, Raymond is a serious python programmer, and old hand, and he gives excellent talks. Had no idea he gave a talk on SAT
- anjc 7y agoWhy are people ITT talking about reducing problems to SAT? As I understand it, the point of reducing a problem to SAT is because there's a proof that SAT is NP-Complete which in turn would prove that your problem is NP-Complete. But if you have some sort of industrial constraint satisfaction/ASP/scheduling/search/etc problem, you can solve it with whatever methods are available. You don't have to reduce a problem in such and such domain down to a big Boolean formula and solve it via SAT techniques. Am I wrong?
- ausbah 7y agoReading through a couple of other responses in this thread, it seems that converting a problem to be compatible with a SAT solver can sometimes result in unexpected gains in speed? That SAT solvers can sometimes be a better solution to a problem than the general "go to" solutions for a domain, despite it seeming to be inapplicable to such a domain? Maybe?
- taejo 7y agoIt's not that they seem inapplicable to some domain: they're applicable to a huge number of domains (basically any kind of constraint satisfaction problem). A lot of people thinks that this generality means that solving SAT problems is difficult, but in reality it means that a huge amount of effort has been invested into SAT solvers, which may outweigh the benefits you can get from a specialized solver.
- Drup 7y agoSAT (and SMT) solvers are extremely optimized and very expressive. Writing an encoding from problem P to SAT is usually much simpler and easier to do correctly than writing a dedicated solver for P. SAT solvers are so efficient than very often they will be competitive with dedicated ones. At the end of the day, you want to solve your high-level problem, not writing a solver, especially when such good solvers are already available.
- pfdietz 7y agoWhat happened was that SAT solvers (and the related SMT solvers) got very fast, so fast that often the fastest way to solve a constraint satisfaction problem is to express it in a form one of these general solvers takes as input and then just using the general tool. Of course the problems being solved are NP hard in general, but in practice, on the kind of problems they're actually given, the solvers can be sufficiently fast.
- gajomi 7y agoStupid question... Are there equivalent (in the sense of being fast and having nice interfaces) solvers for #SAT problems? A whole pile of inference in machine learning can be framed in this way which makes me curious.
- nickpsecurity 7y agoIm on my phone so will have to just dump links. Just found these in DuckDuckGo: https://sites.google.com/site/marcthurley/sharpsat https://sites.google.com/site/marcthurley/sharpsat http://www.ii.uib.no/~telle/bib/STV15.pdf http://www.ii.uib.no/~telle/bib/STV15.pdf http://www.cs.toronto.edu/~fbacchus/Papers/DBaaai07.pdf http://www.cs.toronto.edu/~fbacchus/Papers/DBaaai07.pdf https://github.com/dfremont/maxcount https://github.com/dfremont/maxcount
- hugomg 7y agoIn case others aren't familiar with the termiology: #SAT is the counting version of the SAT problem, which tries to find how many different solutions exist to a set of constraints)
- rcfox 7y agoHow similar is that to answer set programming?
- IloveHN84 7y agoI thought it was an article on satellite signal for tv
- deleted 7y ago[deleted]
- deleted 7y ago[deleted]
- pdobsan 7y agoThe article does not mention it but "symmetry breaking", a technique of exploiting symmetry to prune the search tree, can also be an important component of modern SAT solvers. In some sense one cannot do better than avoiding all symmetries in the given problem however that might come at significant computational price in practice. Static symmetry breaking is performed as a kind of preprocessing, while dynamic symmetry breaking is interleaved with the search process. The static method has been used more but there are promising attempts to use dynamic symmetry breaking with CDCL solvers. See, for example, cosy (https://github.com/lip6/cosy https://github.com/lip6/cosy) a symmetry breaking library which can be used with CDCL solvers.
- rienko 7y agoI’ve researched many moon ago, breaking symmetries dynamically by adding clause conflicts. You take the search space build a graph with it and pass it to a Graph homomorphism detector. Then you create adicional clauses that break the symmetry by stopping possible assignments that limit the search space. The overhead of searching for symmetries and the exposition of dynamic clauses, make it a difficult trade off against the ruthless efficiency of traditional CDCL. Also many competitions used to occur every year to find out the fastest solver, these things have been optimized far beyond you would do for “normal” software.
- pdobsan 7y ago> The overhead of searching for symmetries and the exposition of dynamic clauses, make it a difficult trade off against the ruthless efficiency of traditional CDCL That is certainly true. However, once all the other components have been optimized the hell out of them (of course that is a never ending story itself but probably with diminishing returns) the optimization of the symmetry breaking parts will follow. As I mentioned before, efficiently dealing with isomorphism in the search space is the ultimate (theoretical) optimization. This development can already been observed looking at the history of graph automorphism packages. For a very long time "naughty" was the only significant player than suddenly came "saucy" and "bliss". As far as I know, one of the motivations for the newcomers was to use them for symmetry breaking.
- 7y ago
- tantalor 7y ago"and underused" Where does the article talk about this?
- trombonechamp 7y agoWhat is the benefit of using a SAT solver directly instead of an SMT solver, other than tweaking for a bit better performance in the SAT solver?
- calf 7y agoIs there a standard book or lecture that explains the stuff like conflict clauses and literal watch? I see informal tutorials but something more fully explained, but not overly technical would be useful for people interested in applications. Just something in between blog posts and having to read the original technical papers.
- bayesian_horse 7y agoThe barrier to entry seems extremely high. Most "example" problems already require arcane domain knowledge.
- bayesian_horse 7y agoI think the number one reason SAT Solvers are underutilized is because even relatively advanced programmers like me don't have a particular clue how to frame their problems for a SAT solver.
- lou1306 7y agoSince I cannot find it mentioned in the OP nor in the comments: if you want to experiment with SAT, the pysat package might be a pretty good start. https://github.com/pysathq/pysat https://github.com/pysathq/pysat The API is not exactly Pythonic (numpy/scipy/opencv style) but it's loaded with features.