Modern SAT solvers: fast, neat and underused

I have used the Z3 solver(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.

  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)

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.

SMT solvers (which are a generalization of SAT solvers) are quite useful for program verification and symbolic execution.

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

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.

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.

I'm the same with Prolog. I love the language, but I have only once worked somewhere that used it for an actual problem.

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.

libsolv, a free package dependency solver using a satisfiability algorithm.

https://github.com/openSUSE/libsolv

https://en.opensuse.org/openSUSE:Libzypp_satsolver

The meteor framework uses it for dependency resolution in their package system.

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.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

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-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

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.

Not SAT but this a recent example of using Mixed Integer Programming in real life: https://medium.com/netflix-techblog/predictive-cpu-isolation... (I'm one of the author of the article)

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