SAT solving with higherorder continuations
Finding satisfying assignments to the variables of a boolean formula, called SATsolving, 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 mindbending and (I think) elegant way of finding a satisfying assignment to a boolean formula by bruteforce search. The idea is to do the search using continuationpassing style (CPS), but with one trick.
Continuations
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
value (x
).
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.
The parameter 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 tailcall! Due to tailcall 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 l
has the free variablesr
,k
, andx
; the continuation ofsum r
hasa
,k
, andx
. 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 SATsolver.
SATsolving 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 x
yet,
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 mindbending 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
particular with 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 (* shortcircuiting *)
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 assign
, x
, r
, and fail
.
 By capturing
assign
, the new failure continuation obtains a copy of the evaluator call stack at this point.  We must capture
x
andr
to form the adjusted assignment.  Capturing the outer
fail
forms a linked list of these frames consisting of evaluator stacks and variables.
Given that assign
is the main continuation, we should understand its inputs as
what are supposed to be the outputs of solve
.
 The
env
input is a (possibly) updated version ofr
with more variable bindings accumulated.  The
bool
input is the boolean value ofphi
under the returned assignment.  The
unit > 'r
input is a (possibly) updated version offail
with more stack frames added to it, i.e. moreVar
nodes 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 None
here
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 ()
Unexpected benefits
In contrast with the socalled pedestrian solver that enumerates assignments and
tries them, the implementation of solve
above has an interesting performance
benefit: it caches partial results. Shoutout 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
nonetheless!
To see this caching, suppose we have a fairly large formula with eight
variables.
Let’s order the variables according to when they first appear in a
lefttoright traversal. This is exactly the order in which variables are added
to the environment by solve
.
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 fail
,
jumping back to the eighth variable, and we reevaluate with x8 = false
only
the part of the formula that depended on that variable!
Conclusion
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”
implementation of solve
above, without using continuations.
There is, however, a general way of eliminating higherorder 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!