SAT solving with higher-order continuations
Finding satisfying assignments to the variables of a boolean formula, called SAT-solving, is a model of a whole class of problems. This means that there are many problems out there whose solutions can be implemented in terms of finding such a satisfying assignment.
I want to share a particularly mind-bending and (I think) elegant way of finding a satisfying assignment to a boolean formula by brute-force search. The idea is to do the search using continuation-passing style (CPS), but with one trick.
At every point of a program’s execution, it is associated to some execution state. This state represents what remains to be done with the result of evaluating the current expression. Normally, this execution state is implicit, and in particular, is implied by the programming language’s order of operations.
For example, suppose we are performing a postorder traversal of a binary tree, collapsing it by summing the integer values contained within each node of the tree.
type tree = Leaf | Node of tree * int * tree let rec sum = function 0 | Leaf -> | Node (l, x, r) ->let a = sum l in let b = sum r in (* writing the order of operations explicitly *) a + b + x
When we encounter some node of the tree, we had to get there somehow. On one
hand, if this node is the root of the tree, then there is nothing to do with the
calculated sum; this is the starting position. The calculated sum is simply the
result of the program. On the other hand, if we reached this node as a right
subtree of a parent node, then what remains to be done with the result of this
node is to add it with the parent node’s left subtree sum (
a) and integer
This order of operations is captured concretely by the call stack.
Continuations enter the picture as a representation of the call stack.
Rather than let the language handle the call stack, we will represent it ourselves using functions, in particular using closures.
let rec sum' t k = match t with 0 | Leaf -> k | Node (l, x, r) ->fun a -> sum l @@ fun b -> sum r @@ k (a + b + x)
In this implementation, rather than using
let and relying on the language
implementation to create stack frames for us, we are passing explicit functions
expressing what to do with the result.
k is a continuation. It contains an accumulation of pending
operations to be performed once the result of processing the given tree is
ready. We can make a few observations about this code.
- Each recursive call is now a tail-call! Due to tail-call optimization, no new stack frames will be allocated by the compiler at all. We are doing it all by hand.
- The continuations themselves form a stack. By looking at the
free variables of the continuations we construct when making recursive
calls, we see that they refer to the outer continuation
k. This effectively forms a linked list of continuations – there’s the stack!
- Specifically, the continuation of
sum lhas the free variables
x; the continuation of
x. The compiler will allocate heap objects to store these captured variables – these are the stack frames!
Overall, this merely looks like a more cumbersome way of writing code. However, it does buy us some interesting abilities. Since the execution state is explicit, it becomes possible to store it! This enables us to “time travel” back to a previous point of the program’s execution. It is exactly this ability that I exploit in implementing a backtracking SAT-solver.
SAT-solving with continuations
A pedestrian way of implementing a backtracking SAT solver is first to write an evaluator for boolean formulas, and then to write an enumerator of truth assignments. We try each truth assignment with the evaluator until we find one that makes the formula true.
Here is what such an evaluator looks like.
type formula = of formula * formula | Conj of formula * formula | Disj of formula | Neg of string | Var type env = (string * bool) list let rec eval (r : env) = function List.assoc x r | Var x -> not (eval r e) | Neg e -> | Conj (e1, e2) -> eval r e1 && eval r e2 | Disj (e1, e2) -> eval r e1 || eval r e2
What remains to implement a solver in this way is to collect all the variable names present in the formula, and enumerate all possible assignments.
Instead, we can do it all in one pass using CPS.
The crucial observation is that when we encounter a variable
x, we may or may
not have already picked a value for it. If we haven’t picked a value for
then we want to try to evaluate the rest of the tree with
x = true and if
that doesn’t work, then with
x = false.
What if that still doesn’t work? Then we have to go back to the previous variable and try a different value for it.
What if we run out of previous variables to go back to? Then the formula is unsatisfiable; we will have tried every truth assignment and not found one that makes the formula true.
The mind-bending aspect of this solution is that there are two stacks, not
just one. We will have an “ordinary” call stack for the evaluator, but also have
a secondary stack whose frames are introduced when we pick tentative values for
variables. This secondary stack’s frames will contain a copy of the evaluator
stack at that point, enabling the solver to jump back to that point and try
evaluating the rest of the tree but with an adjusted truth assignment, in
x = false.
I twice emphasize “evaluate the rest of tree” above because that is precisely the current continuation of the evaluator at the point that we encounter the variable.
Let’s see how the code looks.
let rec solve (r : env) (fail : unit -> 'r) (phi : formula) bool -> (unit -> 'r) -> 'r) : 'r = (assign : env -> match phi with begin match List.assoc_opt x r with | Var x -> Some b -> (* we already have a value for `x` *) | assign r b failNone -> (* we don't have a value for `x` *) | true) :: r) true @@ fun () -> assign ((x, false) :: r) false fail assign ((x, end | Conj (e1, e2) -> fun r b1 fail -> solve r fail e1 @@ if b1 then (* short-circuiting *) fun r b2 fail -> assign r (b1 && b2) fail solve r fail e2 @@ else false fail assign r | Disj (e1, e2) ->fun r b1 fail -> solve r fail e1 @@ if b1 then true fail assign r else fun r b2 fail -> solve r fail e2 @@ assign r (b1 || b2) fail
When I first wrote this code, I was frankly surprised that it worked, because I didn’t really understand why it worked. Since then I’ve thought a lot about it, and I will try to offer an intuitive explanation.
Let’s understand the
fail continuation as a stack of variables and
execution states to return to. To see this, consider that the only place where
we construct a value for this continuation is in the case
Var, and the free
variables of that continuation are
- By capturing
assign, the new failure continuation obtains a copy of the evaluator call stack at this point.
- We must capture
rto form the adjusted assignment.
- Capturing the outer
failforms a linked list of these frames consisting of evaluator stacks and variables.
assign is the main continuation, we should understand its inputs as
what are supposed to be the outputs of
envinput is a (possibly) updated version of
rwith more variable bindings accumulated.
boolinput is the boolean value of
phiunder the returned assignment.
unit -> 'rinput is a (possibly) updated version of
failwith more stack frames added to it, i.e. more
Varnodes to jump back to to try alternatives.
There is a little something missing from
solve above. How exactly are we
supposed to call it? In other words, what initial continuations should we
provide, to recover a function
formula -> env option that decides whether a
formula is satisfiable, giving in that case a satisfying assignment?
We need to pick an initial frame for the
fail stack. This frame will be
reached only if we try all the values of all the variables – we return
as the formula is unsatisfiable.
We need to pick an initial frame for the
assign stack. This frame will be
reached when we finish evaluating the formula, and we will be given the
assignment that resulted in the given
bool. Also, we will receive the failure
continuation, which we can call to try different values of the variables until
we get a
bool we like. Of course, the initial
env that we pass will be
empty, as we haven’t seen any variables yet.
let solve' (phi : formula) : env option = fun () -> None) phi @@ fun r result fail -> solve  (if result then Some r else fail ()
In contrast with the so-called pedestrian solver that enumerates assignments and
tries them, the implementation of
solve above has an interesting performance
benefit: it caches partial results. Shout-out to Max
Kopinsky (github) for noticing this.
To be clear, it isn’t obvious that this is a net benefit, since we are using
extra memory to hold an evaluator stack for each variable, but it is interesting
To see this caching, suppose we have a fairly large formula with eight
Let’s order the variables according to when they first appear in a
left-to-right traversal. This is exactly the order in which variables are added
to the environment by
Under this order, by the time we encounter the eighth variable, we have already
evaluated some chunk of the formula that didn’t depend on that variable. When we
finish evaluating the formula and see that
result = false, we call
jumping back to the eighth variable, and we reevaluate with
x8 = false only
the part of the formula that depended on that variable!
This article explains execution states, continuations as representations thereof, and shows an interesting use of them to implement a backtracking search by storing continuations in the closures of other continuations. This layering of continuations gives rise to a fascinating kind of control flow, enabling backtracking to certain leaves of a tree to make different choices at those points.
It is not immediately obvious how one can recover a nice, “direct”
solve above, without using continuations.
There is, however, a general way of eliminating higher-order functions called
defunctionalization. In short, whereas CPS gives us control of stack
frames, defunctionalization forces us moreover to manually construct and
destruct closures. Defunctionalizing
solve gives us a program using
explicit stacks in the form of lists of frames, represented as explicit data
structures. This representation makes it plainly obvious that the failure
continuation stores a copy of the evaluator continuation.
Looking at the defunctionalization of
solve in more details would be the topic
of a future post!