6 ms·

Modern SAT solvers: fast, neat and underused

237 points by dmit 7y ago

ladberg 7y ago
SAT solvers are something I would like to use more, but I feel like I simply never come across real world problems that they work well with. I've tried to use them for program/circuit synthesis, but the problem was intractable at any scale larger than a tiny proof-of-concept example. Does anyone have good suggestions for what to use SAT solvers for?
- nightcracker 7y ago
  At a local group we have weekly meetings where we cook dinner. Two people cook, and two people do the dishes. I used a SAT solver (z3) to find optimal schedules given that people want the tasks to be distributed fairly, but also given other secondary criteria such as mixing up which pairs cook together, prevent being assigned a task two weeks in a row or getting the same task twice in a row, etc.
  - nurettin 7y ago
    It is pretty easy to come up with an integer space in order to simulate week days, the concept of consecutiveness and homogeneous distribution. However, as soon as we get custom rules and exceptions things start to become impossible and we have to start inventing a best effort solution which turns into minimization or maximization of each human variable. At this point some humans with higher status want to be favoured and you get a tug of war instead of an sat solver problem where nothing you suggest pleases anyone because they have a life and can't afford to tell you every little detail that interests them and they go back to manually picking their dates.
    - roenxi 7y ago
      In corporate deployment of a SAT or even a linear solver one of the bigger challenges is convincing people to solve the SAT/linear problem and then stop. I'd guess that most corporate deployments of a solver are (1) solve the easy part (2) add one extension to try and deal with a difficult part (3) deployment finishes because cost of a 2nd extension is too high, either computationally or in development time. I think there is a big untapped corporate demand for evolutionary optimisers. They scale a bit closer to problem difficulty as measured by humans and people get dazzled by the idea of finding an optimal solution to a bad model rather than an OK solution to an OK model of reality which is more flexible.
    - wenc 7y ago
      > they go back to manually picking their dates. I'm not sure if it's all or nothing. SAT are concerned with satisfying constraints, so you get feasible solutions. A feasible solution merely satisfies constraints, and does not take objectives into account. The optimization-equivalent is an Integer Program (IP), which gives you optimal solutions for a given objective function while satisfying all constraints. Most complex scheduling problems are solved as IPs or MIPS (Mixed Integer Programs). Priorities can be modeled as weights. Even if everybody's preferences cannot be met, you can arrive at some sort of weighted compromise (either in a least-squares sense, or some user-defined distance metric) The best MIP solvers today (e.g. CPLEX, Gurobi, Xpress) solve problems with 100k variables without breaking a sweat (caveat: they do not handle nonconvexities, but good modelers know how to develop linear/convex formulations). They are used in applications ranging from hospital scheduling to airline scheduling to oil refinery scheduling. In my experience computer scientists typically know about SAT solvers but only a small subset know about MIP solvers. Knowing about the latter expands one's horizons on what's possible.
      - nurettin 7y ago
        What I meant was, human capriciousness is hard to model and they change their initial premises on a whim. Especially in academic environments. On the other hand, military and hospital applications won't show that weakness.
        wenc 7y ago
        Human capriciousness is indeed hard to model, so one solution is not do it. In timetabling applications, the algorithm provides a level of impartiality so even if some constituents don't get what they want, you can always blame the algorithm -- "it tried, but it had to satisfy other constraints". This removes some (but not all) of the politics behind timetabling. Influential persons may still try to wield their political power to bend the algorithm toward favoring them (e.g. in algorithmic terms, this could mean boosting their weight from 0.5 to 0.8 to beat out competition) but even in this compromised state, optimal timetabling is still better than doing it manually -- the optimization algorithm will at least try to maximize remaining preferences within the remainder degrees-of-freedom. Timetabling is an inherently political process anywhere (if one has ever done timetable for high school teachers....), but optimization algorithms do bring a level of impartiality to the process. Also, if folks aren't explicit about their preferences, or change their minds, it's no fault of the algorithm.
  - mabbo 7y ago
    That's fascinating! I've always wanted to build a similar system for assigning chores around the house based on everyone "bidding" on how much they see the effort of each chore being. In theory, one should be able to come up with an assignment where everyone believes they're doing less than everyone else, by their own metric of work effort. Applying computer science to everyday life is so rare but lovely.
    - Pamar 7y ago
      I studied Simplex and related techniques at University, and took https://courses.edx.org/courses/course-v1:MITx+15.053x+3T2016/course/ https://courses.edx.org/courses/course-v1:MITx+15.053x+3T201... as a refresher. The course is now closed, but you can probably find something similar as a MOOC.
- saagarjha 7y ago
  SMT solvers (which are a generalization of SAT solvers) are quite useful for program verification and symbolic execution.
- nextos 7y ago
  I have applied SATs with some success to generative models where sampling methods would not work well, e.g. if you have many soft and hard constraints. Another alternative is to use neural guides.
  - 2400 7y ago
    do you have any pointers on modeling with soft/hard constraints and SAT solvers?
- KboPAacDA3 7y ago
  These can be deployed against the Eternity II puzzle. I doubt any SAT solver will find a complete solution in our lifetimes, but a near solution would be satisfying. https://en.wikipedia.org/wiki/Eternity_II_puzzle https://en.wikipedia.org/wiki/Eternity_II_puzzle
  - OscarCunningham 7y ago
    > satisfying Heh.
- silly_giraffe 7y ago
  I have used the Z3 solver(https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3) to optimize a job scheduling problem. Roughly, I have ~20k jobs, defined by N tasks (~1-50). A job is complete only if M tasks (typically 2-3) per job are done. Every task takes some variable amount of time to complete and can only be run during specific windows. Given the equipment can only perform P tasks in parallel, what is the optimal configuration of tasks (~500k) that will allow us to complete the most jobs? The search space for this problem is enormous, but Z3 will produce an impressive result within a few minutes.
  - 2400 7y ago
    amazing, I tried doing this recently but I guess my modeling was not good enough and it would take hours to find the solution with a couple of dozen variables. Do you have any pointers on how to much these types of problems with a SMT/SAT solver efficiently?
    - silly_giraffe 7y ago
      The documentation and API quirks of z3 also led me down some performance sinks before I was able to tackle the larger models. Not a Z3/SMT expert, but what worked for me was to model every time tick as the sum of all tasks that could be performed at that instant. Set a constraint on each tick that sets the sum of these tasks to be <= P. Add the book-keeping on the task-job relationships and that was it. Using the Python bindings, the biggest performance impact I discovered was ensuring that my jobs and tasks were represented as z3.Bool and not z3.Int (requiring a roundabout way to do a summation on z3.Bools). Something like: tasks_this_tick = [(z3.Bool(task_id), 1) for task_id in current_tasks] model.add(z3.PbLe(tasks_this_tick, max_tasks_per_tick + 1)
- kabes 7y ago
  The meteor framework uses it for dependency resolution in their package system.
- noneeeed 7y ago
  I'm the same with Prolog. I love the language, but I have only once worked somewhere that used it for an actual problem.
- debatem1 7y ago
  I've done some program synthesis and equivalence proving with them. It was for sure trivial to express and nontrivial to express in a way that would actually get to a solution. I know of no general shortcuts for avoiding the part where it performs terribly for nonobvious reasons, but then I am not a SAT solver expert. I've also done a bit of work on concolic execution, which has yielded interesting insights but not useful results. I'll probably write something up for hn if/when it does yield results. As others have said, my first real use of it was for scheduling problems. It works but isn't really better than a hand rolled naive solver for the scale of problem I was looking at. They seem to be good for proving obvious things about cryptosystems. It's very interesting to see how quickly block length becomes a security parameter for things like Speck. Overall I like them and they clearly have potent uses, but... often I find myself shrugging, accepting some constraint, and using the more obvious approach. It may be that I just seldom have to solve a hard enough problem with full generality.
- zeroonetwothree 7y ago
  I used one to do the seating arrangement at my wedding. Doing it well manually is nearly impossible if you have a lot of constraints.
- froh 7y ago
  libsolv, a free package dependency solver using a satisfiability algorithm. https://github.com/openSUSE/libsolv https://github.com/openSUSE/libsolv https://en.opensuse.org/openSUSE:Libzypp_satsolver https://en.opensuse.org/openSUSE:Libzypp_satsolver
abbadadda 7y ago
SAT solvers Wikipedia: https://en.m.wikipedia.org/wiki/Boolean_satisfiability_problem https://en.m.wikipedia.org/wiki/Boolean_satisfiability_probl...
bcherny 7y ago
Previously posted 4 months ago and 1 year ago: https://hn.algolia.com/?dateRange=all&page=0&prefix=false&query=modern%20sat%20solvers%3A%20fast&sort=byPopularity&type=story https://hn.algolia.com/?dateRange=all&page=0&prefix=false&qu...
vasili111 7y ago
Can you please share your personal experience of using SAT solver with real world problem?
- mochomocha 7y ago
  Not SAT but this a recent example of using Mixed Integer Programming in real life: https://medium.com/netflix-techblog/predictive-cpu-isolation-of-containers-at-netflix-91f014d856c7 https://medium.com/netflix-techblog/predictive-cpu-isolation... (I'm one of the author of the article)
- ackbar03 7y ago
  Cracking product keys for... Uh... Research. You reverse engineer the binary, enter the conditions into an sat solver and boom. But I don't think most keys are implemented this way these days. Also if you want cool, check out uc Santa Barbara's team for the darpa cyber challenge a few years ago for an autonomous hacking system. Their framework, angr, makes use a lot of sat solvers although I didn't quite understand everything when I read their technical docs
  - xfer 7y ago
    Based on my experience, most key requiring programs use public key crypto and pin their public key in the binary to verify the signature, which is the key.
    - nullc 7y ago
      That hasn't been my experience. I've seen some that use public key crypto, but mostly they do not because even the smallest secure cryptosystems have signatures on the order of at least 20 bytes (and more conventional choices more like 256-bit ECDSA... 64 bytes)-- which, after conversion to typeable characters, are a bit unwieldy.
foxes 7y ago
The programming language Mercury which is a functional, predicate based, moded language uses something like a precursor to a sat solver to "run" the program. As in you can ask for the input of a function to make your program true. I imagine all sorts of things can be done like this, and the sat solver is useful for verifying correctness.
atilimcetin 7y ago
You can also watch the talk from same author about the same subject here - https://www.youtube.com/watch?v=x2XtpCn0-bM https://www.youtube.com/watch?v=x2XtpCn0-bM
T-R 7y ago
SAT solvers are starting to be used as tooling for functional languages - Liquid Haskell uses one for refinement types[1], and Djinn uses one for suggesting functions given a type[2]. Similarly to Djinn, Edwin Brady gave a presentation on using an SMT solver to do live code suggestions/implementation inference in the successor to Idris[3]. [1] https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/ [2] http://lambda-the-ultimate.org/node/1178 http://lambda-the-ultimate.org/node/1178 [3] https://www.youtube.com/watch?v=mOtKD7ml0NU https://www.youtube.com/watch?v=mOtKD7ml0NU
pthariensflame 7y ago
If you’re looking for a higher-level interface to SAT, SMT, and general constraint solvers, I can recommend MiniZinc: https://www.minizinc.org/index.html https://www.minizinc.org/index.html
iflp 7y ago
This is an interesting read, but I'd be interested in a more large-scale benchmark. Right now it could be possible that the SAT solver is just better optimized for the particular platform, instead of the SAT solver being superior algorithm-wise.
53x15 7y ago
Sudoku may be a poor example for illustrating some of the overarching points of this series of blog posts, which I take to be that modern SAT solvers are, as someone described them in a previous thread, "little diamonds of engineering", that they embody decades of research, that you can exploit their power cheaply and easily, and that it might take significant effort to beat them if you have a non-trivial problem. Since specialized solvers do thrash SAT-based solvers for conventional Sudoku, the author focuses the example less on absolute performance and more on simplicity, rapid prototyping, and comparison to casual non-SAT implementations. But conventional Sudoku is a small problem, and in most cases the SAT-based solver makes so few decisions that it doesn't benefit much from CDCL. Consider here[1] the comparison to JCZSolve(ZSolver) that the author mentions in part 1 of the series: For 17-clue puzzles (which are generally very easy), JCZSolve is 50x as fast as Minisat, and it makes on average ~1.9 decisions per puzzle compared to Minisat's ~3.0. But if you look at the hardest dataset JCZSolve is only 10x as fast as Minisat, and it makes on average ~365 decisions per puzzle compared to Minisat's ~121. I'm not aware of a highly specialized and optimized Solver for 16x16 clue or larger Sudoku, but given this trend my guess is that it would take a lot of effort to write one that's faster than what you get with Minisat for free. [1] https://github.com/t-dillon/tdoku/blob/master/benchmarks/GCE-c2-standard-4_clang-8_O3_native https://github.com/t-dillon/tdoku/blob/master/benchmarks/GCE...
vector_spaces 7y ago
Whenever I read about SAT solvers I think of Prolog and Minikanren and friends. Is there a relationship there? Do they use similar algorithms? I know that backtracking (mentioned in the article) is a thing in Prolog at least.
- triska 7y ago
  Yes, there are strong connections: In Prolog terminology, SAT is called CLP(B), constraint logic programming over Boolean variables, and several Prolog systems provide dedicated libraries to solve SAT instances efficiently. For instance, SICStus Prolog ships with a nice CLP(B) solver: https://sicstus.sics.se/sicstus/docs/latest3/html/sicstus.html/CLPB.html https://sicstus.sics.se/sicstus/docs/latest3/html/sicstus.ht... This particular solver uses Binary Decision Diagrams (BDDs) to model and solve SAT instances. CLP(B) blends in seamlessly with Prolog in the sense that Prolog variables and predicates are used to ask questions and obtain answers about satisfiability. For instance, we can formulate a Prolog query that asks: “Are there any X and Y such that the (X∧Y)∨X is satisfiable?” ?- sat(X*Y + X). X = 1, sat(Y=:=Y). The answer tells us that yes, the expression is satisfiable, if and only if X = 1. Moreover, we see from the answer that the truth value of the expression is then independent of Y, because Y is only constrained to be a Boolean variable (by the tautology Y⇔Y) and not involved in any other constraints. To obtain concrete assignments that make the expression true, we can use the library predicate labeling/1. On backtracking, all solutions are enumerated: ?- sat(X*Y + X), labeling([X,Y]). X = 1, Y = 0 ; X = Y, Y = 1. There are many different ways and approaches to implement SAT solvers, and this diversity is also reflected in Prolog implementations that provide them. For instance, in GNU Prolog, SAT solving is provided as a special case of integer constraints: http://www.gprolog.org/manual/html_node/gprolog061.html http://www.gprolog.org/manual/html_node/gprolog061.html The SAT solver of B-Prolog is so strong that it can compete with some dedicated SAT solvers. For a nice overview: https://www.cs.nmsu.edu/ALP/2013/03/the-sat-compiler-in-b-prolog/ https://www.cs.nmsu.edu/ALP/2013/03/the-sat-compiler-in-b-pr... A very nice SAT solver implementation in Prolog is explained in the paper A Pearl on SAT Solving in Prolog by Jacob M. Howe and Andy King: http://www.staff.city.ac.uk/~jacob/solver/flops.pdf http://www.staff.city.ac.uk/~jacob/solver/flops.pdf The paper shows that 20 lines of Prolog code suffice to implement an elegant solver for—as the authors put it—"solving some interesting, albeit modest, SAT instances". However, SAT is a quite low-level way to encode combinatorial tasks, and for this reason, CLP(FD/ℤ), i.e., constraint logic programming over finite domains/integers is typically used instead of SAT when solving combinatorial tasks with Prolog. Conceptually, we can think of CLP(ℤ) as a generalization of SAT solving, where variables can range over the entire integers instead of only 0 and 1. Strong and fast constraint solvers over integers are a major attraction of commercial Prolog systems, and often the key reason for buying one. From a logical perspective, propositional logic can be regarded as a special case of first-order predicate logic, so a language rooted in predicate logic, like Prolog, is also related to SAT solving in this way.
MaxBarraclough 7y ago
Links to previous HN discussions of this article: https://news.ycombinator.com/item?id=19953213 https://news.ycombinator.com/item?id=19953213 https://news.ycombinator.com/item?id=17684502 https://news.ycombinator.com/item?id=17684502 https://news.ycombinator.com/item?id=17778770 https://news.ycombinator.com/item?id=17778770
ausbah 7y ago
How do SAT problems compare to constraint satisfaction problems? Is the latter a subset of the former (with the right modeling)?
mshockwave 7y ago
I'm actually finding part 2 more interesting

237 points by dmit 7y ago

SAT solvers are something I would like to use more, but I feel like I simply never come across real world problems that they work well with. I've tried to use them for program/circuit synthesis, but the problem was intractable at any scale larger than a tiny proof-of-concept example. Does anyone have good suggestions for what to use SAT solvers for?

nightcracker 7y ago
At a local group we have weekly meetings where we cook dinner. Two people cook, and two people do the dishes. I used a SAT solver (z3) to find optimal schedules given that people want the tasks to be distributed fairly, but also given other secondary criteria such as mixing up which pairs cook together, prevent being assigned a task two weeks in a row or getting the same task twice in a row, etc.
- nurettin 7y ago
  It is pretty easy to come up with an integer space in order to simulate week days, the concept of consecutiveness and homogeneous distribution. However, as soon as we get custom rules and exceptions things start to become impossible and we have to start inventing a best effort solution which turns into minimization or maximization of each human variable. At this point some humans with higher status want to be favoured and you get a tug of war instead of an sat solver problem where nothing you suggest pleases anyone because they have a life and can't afford to tell you every little detail that interests them and they go back to manually picking their dates.
  - roenxi 7y ago
    In corporate deployment of a SAT or even a linear solver one of the bigger challenges is convincing people to solve the SAT/linear problem and then stop. I'd guess that most corporate deployments of a solver are (1) solve the easy part (2) add one extension to try and deal with a difficult part (3) deployment finishes because cost of a 2nd extension is too high, either computationally or in development time. I think there is a big untapped corporate demand for evolutionary optimisers. They scale a bit closer to problem difficulty as measured by humans and people get dazzled by the idea of finding an optimal solution to a bad model rather than an OK solution to an OK model of reality which is more flexible.
  - wenc 7y ago
    > they go back to manually picking their dates. I'm not sure if it's all or nothing. SAT are concerned with satisfying constraints, so you get feasible solutions. A feasible solution merely satisfies constraints, and does not take objectives into account. The optimization-equivalent is an Integer Program (IP), which gives you optimal solutions for a given objective function while satisfying all constraints. Most complex scheduling problems are solved as IPs or MIPS (Mixed Integer Programs). Priorities can be modeled as weights. Even if everybody's preferences cannot be met, you can arrive at some sort of weighted compromise (either in a least-squares sense, or some user-defined distance metric) The best MIP solvers today (e.g. CPLEX, Gurobi, Xpress) solve problems with 100k variables without breaking a sweat (caveat: they do not handle nonconvexities, but good modelers know how to develop linear/convex formulations). They are used in applications ranging from hospital scheduling to airline scheduling to oil refinery scheduling. In my experience computer scientists typically know about SAT solvers but only a small subset know about MIP solvers. Knowing about the latter expands one's horizons on what's possible.
    - nurettin 7y ago
      What I meant was, human capriciousness is hard to model and they change their initial premises on a whim. Especially in academic environments. On the other hand, military and hospital applications won't show that weakness.
      - wenc 7y ago
        Human capriciousness is indeed hard to model, so one solution is not do it. In timetabling applications, the algorithm provides a level of impartiality so even if some constituents don't get what they want, you can always blame the algorithm -- "it tried, but it had to satisfy other constraints". This removes some (but not all) of the politics behind timetabling. Influential persons may still try to wield their political power to bend the algorithm toward favoring them (e.g. in algorithmic terms, this could mean boosting their weight from 0.5 to 0.8 to beat out competition) but even in this compromised state, optimal timetabling is still better than doing it manually -- the optimization algorithm will at least try to maximize remaining preferences within the remainder degrees-of-freedom. Timetabling is an inherently political process anywhere (if one has ever done timetable for high school teachers....), but optimization algorithms do bring a level of impartiality to the process. Also, if folks aren't explicit about their preferences, or change their minds, it's no fault of the algorithm.
- mabbo 7y ago
  That's fascinating! I've always wanted to build a similar system for assigning chores around the house based on everyone "bidding" on how much they see the effort of each chore being. In theory, one should be able to come up with an assignment where everyone believes they're doing less than everyone else, by their own metric of work effort. Applying computer science to everyday life is so rare but lovely.
  - Pamar 7y ago
    I studied Simplex and related techniques at University, and took https://courses.edx.org/courses/course-v1:MITx+15.053x+3T2016/course/ https://courses.edx.org/courses/course-v1:MITx+15.053x+3T201... as a refresher. The course is now closed, but you can probably find something similar as a MOOC.
saagarjha 7y ago
SMT solvers (which are a generalization of SAT solvers) are quite useful for program verification and symbolic execution.
nextos 7y ago
I have applied SATs with some success to generative models where sampling methods would not work well, e.g. if you have many soft and hard constraints. Another alternative is to use neural guides.
- 2400 7y ago
  do you have any pointers on modeling with soft/hard constraints and SAT solvers?
KboPAacDA3 7y ago
These can be deployed against the Eternity II puzzle. I doubt any SAT solver will find a complete solution in our lifetimes, but a near solution would be satisfying. https://en.wikipedia.org/wiki/Eternity_II_puzzle https://en.wikipedia.org/wiki/Eternity_II_puzzle
- OscarCunningham 7y ago
  > satisfying Heh.
silly_giraffe 7y ago
I have used the Z3 solver(https://github.com/Z3Prover/z3 https://github.com/Z3Prover/z3) to optimize a job scheduling problem. Roughly, I have ~20k jobs, defined by N tasks (~1-50). A job is complete only if M tasks (typically 2-3) per job are done. Every task takes some variable amount of time to complete and can only be run during specific windows. Given the equipment can only perform P tasks in parallel, what is the optimal configuration of tasks (~500k) that will allow us to complete the most jobs? The search space for this problem is enormous, but Z3 will produce an impressive result within a few minutes.
- 2400 7y ago
  amazing, I tried doing this recently but I guess my modeling was not good enough and it would take hours to find the solution with a couple of dozen variables. Do you have any pointers on how to much these types of problems with a SMT/SAT solver efficiently?
  - silly_giraffe 7y ago
    The documentation and API quirks of z3 also led me down some performance sinks before I was able to tackle the larger models. Not a Z3/SMT expert, but what worked for me was to model every time tick as the sum of all tasks that could be performed at that instant. Set a constraint on each tick that sets the sum of these tasks to be <= P. Add the book-keeping on the task-job relationships and that was it. Using the Python bindings, the biggest performance impact I discovered was ensuring that my jobs and tasks were represented as z3.Bool and not z3.Int (requiring a roundabout way to do a summation on z3.Bools). Something like: tasks_this_tick = [(z3.Bool(task_id), 1) for task_id in current_tasks] model.add(z3.PbLe(tasks_this_tick, max_tasks_per_tick + 1)
kabes 7y ago
The meteor framework uses it for dependency resolution in their package system.
noneeeed 7y ago
I'm the same with Prolog. I love the language, but I have only once worked somewhere that used it for an actual problem.
debatem1 7y ago
I've done some program synthesis and equivalence proving with them. It was for sure trivial to express and nontrivial to express in a way that would actually get to a solution. I know of no general shortcuts for avoiding the part where it performs terribly for nonobvious reasons, but then I am not a SAT solver expert. I've also done a bit of work on concolic execution, which has yielded interesting insights but not useful results. I'll probably write something up for hn if/when it does yield results. As others have said, my first real use of it was for scheduling problems. It works but isn't really better than a hand rolled naive solver for the scale of problem I was looking at. They seem to be good for proving obvious things about cryptosystems. It's very interesting to see how quickly block length becomes a security parameter for things like Speck. Overall I like them and they clearly have potent uses, but... often I find myself shrugging, accepting some constraint, and using the more obvious approach. It may be that I just seldom have to solve a hard enough problem with full generality.
zeroonetwothree 7y ago
I used one to do the seating arrangement at my wedding. Doing it well manually is nearly impossible if you have a lot of constraints.
froh 7y ago
libsolv, a free package dependency solver using a satisfiability algorithm. https://github.com/openSUSE/libsolv https://github.com/openSUSE/libsolv https://en.opensuse.org/openSUSE:Libzypp_satsolver https://en.opensuse.org/openSUSE:Libzypp_satsolver

abbadadda 7y ago

SAT solvers Wikipedia: https://en.m.wikipedia.org/wiki/Boolean_satisfiability_problem https://en.m.wikipedia.org/wiki/Boolean_satisfiability_probl...

bcherny 7y ago

Previously posted 4 months ago and 1 year ago: https://hn.algolia.com/?dateRange=all&page=0&prefix=false&query=modern%20sat%20solvers%3A%20fast&sort=byPopularity&type=story https://hn.algolia.com/?dateRange=all&page=0&prefix=false&qu...

vasili111 7y ago

Can you please share your personal experience of using SAT solver with real world problem?

mochomocha 7y ago
Not SAT but this a recent example of using Mixed Integer Programming in real life: https://medium.com/netflix-techblog/predictive-cpu-isolation-of-containers-at-netflix-91f014d856c7 https://medium.com/netflix-techblog/predictive-cpu-isolation... (I'm one of the author of the article)
ackbar03 7y ago
Cracking product keys for... Uh... Research. You reverse engineer the binary, enter the conditions into an sat solver and boom. But I don't think most keys are implemented this way these days. Also if you want cool, check out uc Santa Barbara's team for the darpa cyber challenge a few years ago for an autonomous hacking system. Their framework, angr, makes use a lot of sat solvers although I didn't quite understand everything when I read their technical docs
- xfer 7y ago
  Based on my experience, most key requiring programs use public key crypto and pin their public key in the binary to verify the signature, which is the key.
  - nullc 7y ago
    That hasn't been my experience. I've seen some that use public key crypto, but mostly they do not because even the smallest secure cryptosystems have signatures on the order of at least 20 bytes (and more conventional choices more like 256-bit ECDSA... 64 bytes)-- which, after conversion to typeable characters, are a bit unwieldy.

foxes 7y ago

The programming language Mercury which is a functional, predicate based, moded language uses something like a precursor to a sat solver to "run" the program. As in you can ask for the input of a function to make your program true. I imagine all sorts of things can be done like this, and the sat solver is useful for verifying correctness.

atilimcetin 7y ago

You can also watch the talk from same author about the same subject here - https://www.youtube.com/watch?v=x2XtpCn0-bM https://www.youtube.com/watch?v=x2XtpCn0-bM

T-R 7y ago

SAT solvers are starting to be used as tooling for functional languages - Liquid Haskell uses one for refinement types[1], and Djinn uses one for suggesting functions given a type[2]. Similarly to Djinn, Edwin Brady gave a presentation on using an SMT solver to do live code suggestions/implementation inference in the successor to Idris[3]. [1] https://ucsd-progsys.github.io/liquidhaskell-blog/ https://ucsd-progsys.github.io/liquidhaskell-blog/ [2] http://lambda-the-ultimate.org/node/1178 http://lambda-the-ultimate.org/node/1178 [3] https://www.youtube.com/watch?v=mOtKD7ml0NU https://www.youtube.com/watch?v=mOtKD7ml0NU

pthariensflame 7y ago

If you’re looking for a higher-level interface to SAT, SMT, and general constraint solvers, I can recommend MiniZinc: https://www.minizinc.org/index.html https://www.minizinc.org/index.html

iflp 7y ago

This is an interesting read, but I'd be interested in a more large-scale benchmark. Right now it could be possible that the SAT solver is just better optimized for the particular platform, instead of the SAT solver being superior algorithm-wise.

53x15 7y ago

Sudoku may be a poor example for illustrating some of the overarching points of this series of blog posts, which I take to be that modern SAT solvers are, as someone described them in a previous thread, "little diamonds of engineering", that they embody decades of research, that you can exploit their power cheaply and easily, and that it might take significant effort to beat them if you have a non-trivial problem. Since specialized solvers do thrash SAT-based solvers for conventional Sudoku, the author focuses the example less on absolute performance and more on simplicity, rapid prototyping, and comparison to casual non-SAT implementations. But conventional Sudoku is a small problem, and in most cases the SAT-based solver makes so few decisions that it doesn't benefit much from CDCL. Consider here[1] the comparison to JCZSolve(ZSolver) that the author mentions in part 1 of the series: For 17-clue puzzles (which are generally very easy), JCZSolve is 50x as fast as Minisat, and it makes on average ~1.9 decisions per puzzle compared to Minisat's ~3.0. But if you look at the hardest dataset JCZSolve is only 10x as fast as Minisat, and it makes on average ~365 decisions per puzzle compared to Minisat's ~121. I'm not aware of a highly specialized and optimized Solver for 16x16 clue or larger Sudoku, but given this trend my guess is that it would take a lot of effort to write one that's faster than what you get with Minisat for free. [1] https://github.com/t-dillon/tdoku/blob/master/benchmarks/GCE-c2-standard-4_clang-8_O3_native https://github.com/t-dillon/tdoku/blob/master/benchmarks/GCE...

vector_spaces 7y ago

Whenever I read about SAT solvers I think of Prolog and Minikanren and friends. Is there a relationship there? Do they use similar algorithms? I know that backtracking (mentioned in the article) is a thing in Prolog at least.

triska 7y ago
Yes, there are strong connections: In Prolog terminology, SAT is called CLP(B), constraint logic programming over Boolean variables, and several Prolog systems provide dedicated libraries to solve SAT instances efficiently. For instance, SICStus Prolog ships with a nice CLP(B) solver: https://sicstus.sics.se/sicstus/docs/latest3/html/sicstus.html/CLPB.html https://sicstus.sics.se/sicstus/docs/latest3/html/sicstus.ht... This particular solver uses Binary Decision Diagrams (BDDs) to model and solve SAT instances. CLP(B) blends in seamlessly with Prolog in the sense that Prolog variables and predicates are used to ask questions and obtain answers about satisfiability. For instance, we can formulate a Prolog query that asks: “Are there any X and Y such that the (X∧Y)∨X is satisfiable?” ?- sat(X*Y + X). X = 1, sat(Y=:=Y). The answer tells us that yes, the expression is satisfiable, if and only if X = 1. Moreover, we see from the answer that the truth value of the expression is then independent of Y, because Y is only constrained to be a Boolean variable (by the tautology Y⇔Y) and not involved in any other constraints. To obtain concrete assignments that make the expression true, we can use the library predicate labeling/1. On backtracking, all solutions are enumerated: ?- sat(X*Y + X), labeling([X,Y]). X = 1, Y = 0 ; X = Y, Y = 1. There are many different ways and approaches to implement SAT solvers, and this diversity is also reflected in Prolog implementations that provide them. For instance, in GNU Prolog, SAT solving is provided as a special case of integer constraints: http://www.gprolog.org/manual/html_node/gprolog061.html http://www.gprolog.org/manual/html_node/gprolog061.html The SAT solver of B-Prolog is so strong that it can compete with some dedicated SAT solvers. For a nice overview: https://www.cs.nmsu.edu/ALP/2013/03/the-sat-compiler-in-b-prolog/ https://www.cs.nmsu.edu/ALP/2013/03/the-sat-compiler-in-b-pr... A very nice SAT solver implementation in Prolog is explained in the paper A Pearl on SAT Solving in Prolog by Jacob M. Howe and Andy King: http://www.staff.city.ac.uk/~jacob/solver/flops.pdf http://www.staff.city.ac.uk/~jacob/solver/flops.pdf The paper shows that 20 lines of Prolog code suffice to implement an elegant solver for—as the authors put it—"solving some interesting, albeit modest, SAT instances". However, SAT is a quite low-level way to encode combinatorial tasks, and for this reason, CLP(FD/ℤ), i.e., constraint logic programming over finite domains/integers is typically used instead of SAT when solving combinatorial tasks with Prolog. Conceptually, we can think of CLP(ℤ) as a generalization of SAT solving, where variables can range over the entire integers instead of only 0 and 1. Strong and fast constraint solvers over integers are a major attraction of commercial Prolog systems, and often the key reason for buying one. From a logical perspective, propositional logic can be regarded as a special case of first-order predicate logic, so a language rooted in predicate logic, like Prolog, is also related to SAT solving in this way.

MaxBarraclough 7y ago

Links to previous HN discussions of this article: https://news.ycombinator.com/item?id=19953213 https://news.ycombinator.com/item?id=19953213 https://news.ycombinator.com/item?id=17684502 https://news.ycombinator.com/item?id=17684502 https://news.ycombinator.com/item?id=17778770 https://news.ycombinator.com/item?id=17778770

ausbah 7y ago

How do SAT problems compare to constraint satisfaction problems? Is the latter a subset of the former (with the right modeling)?

mshockwave 7y ago

I'm actually finding part 2 more interesting