SAT solvers

So far, we have been focusing on model checking (post, post), in this post we will start discussing one tool several model checkers use: SAT solvers.

The Boolean Satisfiability Problem (or SAT) is very famous in computer science. Mainly, since it was the first problem to be shown to be NP-complete (a complexity class) but I will not get into complexity in this post.

The problem is to decide whether a given a propositional logic formula is satisfiable or not. A possible (brute force) solution, would be to check every possible assignment for the variables and check whether the formula is satisfied for that assignment. We can see that this solution would imply checking (in the worst case) 2^|VARS| assignments, which as the number of variables increases, the number of checks increases exponentially!

Fortunately, there are many heuristics and algorithms that make SAT feasible in practice for certain inputs even having many many variables. Thus multiple tools are available and are used in the context of formal verification.

For example, SAT solvers are used for Bounded Model Checking (checking the prefixes of the model of length <= k). To translate a state machine over a set of boolean variables V to sat in order to consider k steps, for each variable v in V the variables v_i (i <= k) is created (i.e. the value of variable v in step i) and the initial and transition relation constraints are expressed in terms of step i for every i lower than the bound.

Then by calling the SAT solver, we can check whether some problematic state is reachable (within these k steps).

For example:

if we want to express the first two steps of this state machine (initial and next state), a possible translation could be as follows:

s0_0, s1_0, s2_0, s3_0, s4_0, s5_0: boolean //i.e. the value of each state in step 0
s0_1, s1_1, s2_1, s3_1, s4_1, s5_1: boolean //i.e. the value of each state in step 1
a0, b0, c0: boolean // the value of the variables in step 0
a1, b1, c1: boolean // the value of the variables in step 1

Represent each state at step 0:
assert (s0_0 implies (!a0 and b0 and c0)) // the notation is just to explain the ideas, not the actual input to the sat solver: this assertion indicates which propositions (a, b or c) hold when in s0 at step 0; the ! character represents negation.
assert (s1_0 implies (a0 and b0 and !c0))
assert (s2_0 implies (a0 and !b0 and c0))
assert (s3_0 implies (!a0 and b0 and !c0))
assert (s4_0 implies (!a0 and !b0 and c0))
assert (s5_0 implies (a0 and b0 and c0))

Represent each state at step 1:
assert (s0_1 implies (!a1 and b1 and c1))
assert (s1_1 implies (a1 and b1 and !c1))
assert (s2_1 implies (a1 and !b1 and c1))
assert (s3_1 implies (!a1 and b1 and !c1))
assert (s4_1 implies (!a1 and !b1 and c1))
assert (s5_1 implies (a1 and b1 and c1))

represent the initial states

assert (s0_0 and !s1_0 and !s2_0 and !s3_0 and !s4_0 and !s5_0)

according to the current state at step 0, define the next state

assert (s0_0 implies ((s1_1 or s2_1) and (!s0_1 and !s3_1 and !s4_1 and !s5_1)))
and the same for the remaining states..
assert (s1_0 implies (s3_1 and (!s0_1 and !s1_1 and !s2_1 and !s4_1 and !s5_1)))
...

If we want to check the property:  "if a, then not b and c"

Then we can check for each of the steps, that is:

assert ( (a0 implies not (b0 and c0)) or (a1 implies not (b1 and c1)) )

In this case, the model is satisfiable: for the first two steps it holds that "if a, then not b and c".

If we added two more steps, then when checking:

assert ( (a0 implies not (b0 and c0)) or (a1 implies not (b1 and c1)) or (a2 implies not (b2 and c2)) or (a3 implies not (b3 and c3)) )

the model is shown unsatisfiable.

In the next post I'll explain how to run a sat solver (Minisat) to check these examples