[HN Gopher] Modern SAT solvers: fast, neat and underused (2018)
___________________________________________________________________
Modern SAT solvers: fast, neat and underused (2018)
Author : weird_user
Score : 108 points
Date : 2023-05-26 17:50 UTC (5 hours ago)
(HTM) web link (codingnest.com)
(TXT) w3m dump (codingnest.com)
| api wrote:
| Does't Rust use a SAT solver for aspects of its type system?
| tgamblin wrote:
| Love 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
|
| [1] https://github.com/Z3Prover/z3
|
| [2] https://arxiv.org/abs/2210.08404,
| https://dl.acm.org/doi/abs/10.5555/3571885.3571931
|
| [3] https://github.com/spack/spack
| BorisTheBrave wrote:
| Do you have a recommendation for how to get into ASP? I've read
| the clingo docs, but it has never clicked.
| comfypotato wrote:
| But 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 wrote:
| Z3 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 wrote:
| Compiling 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/sca...
| wenc wrote:
| Conda 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-co...
| jjoonathan wrote:
| I 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 | / - | \
| notatallshaw wrote:
| Also there had been a growing trend for most popular packages
| to offer precompiled wheels on PyPI instead of just sdist
| releases.
|
| This meant that people who had moved to Conda because they
| couldn't get Pip to install important packages into their
| environment took another look and found that actually they
| could get things installed using Pip now.
|
| At the same time Pip also got a resolver allowing you to have
| install time confidence you're not installing conflicting
| package, and recently (Pip 23.1+) the resolver's backtracking
| got pretty good.
|
| That said Conda mostly solved this (and once mamba is the
| default resolver engine things will be really fast), Pip is not
| ever going to be a package manager, and Poetry still isn't an
| environment manager, and most other Python package/installer
| alternatives to Conda won't do things like install your
| Jupyterlab's nodejs dependency.
|
| After many years I now almost exclusively use Pip to install
| into an environment, but still nothing beats Conda for
| bootstraping the non-Python-package requirement's (such as
| Python itself) nor for getting things working when you are in a
| weird environment that you can't install OS dev libraries into.
| rowanG077 wrote:
| Great! Conda honestly can't die fast enough.
| Macuyiko wrote:
| Curious to hear about your preferred alternative. Poetry?
| fock wrote:
| spack
| rowanG077 wrote:
| Poetry, pip, nix or sending out butterflies to bend cosmic
| rays to write bits into memory. It really doesn't matter as
| long as it's not the hellscape that is conda.
| teruakohatu wrote:
| Conda is still unbearably slow. Mamba is a vastly better mostly
| drop-in replacement.
| ubj wrote:
| Second this. Not only is it faster, but the error messages in
| Mamba are much more helpful and sane.
| taeric wrote:
| That 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.
| theLiminator wrote:
| Do you know of any python dependency managers that do this?
| taeric wrote:
| I don't. That said, I think the problems are typically
| small enough that you don't gain much by hunting for a good
| SAT formulation? Python doesn't do anything that any other
| dependency manager does. (Does it?)
| nemetroid wrote:
| DNF uses a SAT solver. It's even listed first among the
| motivations for creating DNF:
|
| > DNF is a fork of Yum 3.4 that uses libsolv via hawkey
| for a backend. The main goals of the project are:
|
| > * using a SAT solver for dependency resolving
|
| > ...
|
| https://fedoraproject.org/wiki/Features/DNF
| beecafe wrote:
| https://github.com/mamba-org/mamba
| klodolph wrote:
| From this and Dart, I think one of the lessons here is that SAT
| solvers are the wrong technique for solving dependencies. SAT
| solvers find "better" solutions by some metric, but humans
| using package managers want something which is both simpler and
| faster.
| nyrikki wrote:
| As an example:
|
| Schaefer's dichotomy theorem shows that, when possible, just
| make sure to use Horn clauses when possible.
|
| Takes a bit of thinking but is superior to huristics or SAT
| solvers if you can refactor to allow for it.
| xavxav wrote:
| Wait, this is very relevant to some work I've been doing
| recently, how do you conclude that Horn clauses should be
| preferred from Schaefer's theorem?
| Karrot_Kream wrote:
| Take a look at https://en.wikipedia.org/wiki/Boolean_sati
| sfiability_problem... (based on Schaefer's "The
| complexity of satisfiability problems"). Horn clause
| satisfiability problems (HORN SAT) fall in P-c.
| thomasahle wrote:
| Isn't it just that Horn clauses are easy to understand,
| and they are guaranteed to be fast.
| weavermarquez wrote:
| Not sure if related, to Schaefer's theorem, but I dove into
| Answer Set Programming [1] recently, which follows this
| approach, enabling the use of fast-ish SMT solvers, which
| are a _generalization_ of SAT solvers! Boolean
| /Propositional Logic is to Predicate Logic as SAT is to
| SMT. There's a very nice course about it from the
| developers of Potassco, one of the best open source Answer
| Set Programming framework [2].
|
| The syntax looks like Prolog, but predicate negations are a
| first class citizen, avoids infinite loops.
|
| Prolog's approach is like a depth first search through a
| search tree -- ASP is like a nondeterministic turing
| machine, exploring all branches simultaneously from the
| bottom up.
|
| [1] https://en.wikipedia.org/wiki/Answer_set_programming
|
| [2] https://www.youtube.com/playlist?list=PL7DBaibuDD9O4I05
| DiQfi...
| c0balt wrote:
| Just wanted to shoutout Armin Biere, one of the top contributors
| in this field: 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.
| joko42 wrote:
| There 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?
| jasonwatkinspdx wrote:
| The "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
|
| 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.
| yarg wrote:
| It 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.
| [deleted]
| justicz wrote:
| I really love the clarity + practicality of this article. Super
| well-written.
| CalChris wrote:
| > ... 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/
|
| [2] https://www2.eecs.berkeley.edu/Courses/CS170/
| tanx16 wrote:
| This 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.
| dataflow wrote:
| To clarify, you're specifically talking about reductions _to_
| SAT, not _from_ SAT, right?
|
| Note the former is used as a solution technique for feeding
| into SAT solvers, where the latter's goal is basically the
| exact opposite (to show NP-hardness and hence algorithmic
| intractability). Formal methods courses do the former, but
| algorithms courses usually use SAT for the latter.
| [deleted]
| tgamblin wrote:
| I definitely recall doing reductions to 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 other problems to 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 wrote:
| > 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?
| [deleted]
| PartiallyTyped wrote:
| Both my Alma Maters had courses that used these extensively,
| and also planners like (Pl|Tr|L)ingeling. We also covered
| reducability and SAT in multiple courses in both.
|
| These should also be taught in an advanced PL course, e.g
| liquid, dependent etc types.
| [deleted]
| lower wrote:
| I used to teach formal methods at university, including a
| course with a lot of SAT examples. We tried to make it as
| practical as possible, with many examples and exercises in Java
| (where you just generate your formulas and call a solve
| method). Thing is, most students seemed to hate it
| passionately, just like with reductions to SAT in complexity
| theory.
| _0ffh wrote:
| I wrote a bespoke backtracking solver for a specific class of
| problems. Would love to use Z3 or something, but frankly, I
| wouldn't know how to systematically translate problem
| instances to solver constraints. It's essentially a kind of
| very complex job-shop scheduling problem with lots of dynamic
| inter-dependencies. Many of the problems are hard to even
| solve without dead-locking, while we also naturally strive to
| minimize overall processing time. Where would I find
| ressources to help me get a grip on my specific problem [1]?
| Could I reasonably hope that Z3 or another general solver
| might be faster than a moderately well designed bespoke
| solver in a compiled language?
|
| [1] Some of the constraints: Input goods must be transformed
| through a complex series of assembly/machining/processing
| lines to output goods; each line transforms one or two inputs
| into an (intermediary or end-) product; an assembly line
| produces it's product in a fixed number of time units and
| cannot be stopped or delayed; finished intermediary products
| arrive at the end of an assembly line, which must be cleared
| by then; there are a limited number of temporary storage
| spaces where intermediary products can be moved to/from in a
| fixed number of time units; some assembly lines must wait for
| two intermediary products to be completed to start a job
| combining them into another intermediary or end product; end
| products must then be moved to their destinations.
| travisjungroth wrote:
| The pdf linked on this site is the biggest collection of
| SMT examples I know of: https://sat-smt.codes/
|
| I'm no SMT expert, but the way I've done it is to make some
| representation in Python Z3, and then write some function
| or class that generates those. I was solving MLB
| eliminations (more complex than it sounds) and I think I
| used arrays of ints for number of wins. So I'd pull MLB
| data, turn that into schedule objects which turned
| themselves into z3 constraints.
| layer8 wrote:
| What example use-cases did you use? Just curious.
| fsckboy wrote:
| SAT? I had to look it up, so...
|
| 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 wrote:
| Ah I thought initially that these were solving SAT questions.
| Easy to make mistake, or perhaps just me.
| balls187 wrote:
| No, I also had no idea about this type of problem and
| immediately thought this article was about the placement
| tests administered in the US.
| yarg wrote:
| Has 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?
| abecedarius wrote:
| FWIW, 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 (Python 2)
___________________________________________________________________
(page generated 2023-05-26 23:00 UTC)