The Work Stack

A Brute Force Approach

As mentioned in a previous post determining the satisfiability of a boolean formula is quite trivial with a brute force algorithm. Here we will look at the brute force algorithm and establish the way that we will talk about solvers 'doing work'.

The most common way to implement a depth first search algorithm is with a stack. For our problem we will be pusing sets of variable assignments onto the stack and pooping them off for processing. We'll illustrate this with a very simple formula

p&q

For formula p&q there are four possible variable assignments.

1. p = true, q = true
   
2. p= true, q = false
3. p = false, q = true
4. p = false, q = false
   

Our search algorithm needs to be able to find each one of those combinations so that we can test the formula for satisfiability.

We begin by selecting a variable, p, at random and pushing it's two possible assignments onto the stack. So our stack looks like:

• p=false
• p=true
  

Each element in the stack will be called a state, because every element in the stack represents a distinct possible (partial) variable assignment for the formula.

Next we will pop the top of the stack, p=true, and select a variable which has not yet been assigned, in this case there is only q. We make two new states with the two possible assignments to q and push them onto the top of the stack. Our stack now looks like:

• p=false, q=false
• p=false, q=true
• p=false

Again we pop the top of the stack. We note that the state we have popped is a complete assignment of the variables in the formula. So we ask does it make the formula true (and therefore satisfiable). By subsituting the assignments for the variables into the formula we get

false & false

which is not true. We must keep searching.

We pop the next value off the stack, p=false, q=true, this is also a full assignment of the variables in the formula. This state does not make the formula true either. We discard these full assignments and keep searching.

We pop the next value off the stack, p=true, this is a partial assignment and so we make two new states with the two possible assignments to q and push them onto the top of the stack. Our stack now looks like:

• p=true, q=false
• p=true, q=true

Popping the top of the stack, p=true, q=false, we find a full assignment which does not make the formula true. We pop the next, and final, element from the stack and find that p=true, q=true makes p&q true and therefore satisfiable.

The Algorithm In Pseudocode

Note that {x,y,z} is the notation for a set and U is the union operator.

F = formula for satisfiability
W = Work stack (initially empty)
S = Current State (set of variable assignments)

Select an unassigned variable V
W.push({V = true})
W.push({V = false})

while (true)
if (W.isEmpty())
return unsatisfiable
else
S = W.pop()
if (isFullAssignment(S,F) and satisfies(S,F))
return satisfiable
else
V = getUnassigned(F,S)
S1 = S U {V = true}
S2 = S U {V = false}
W.push(S1)
W.push(S2)
end