SAT Encoding: An Introduction

As I dug thru material to teach a course on SAT solving, I wanted to distill my understanding about SAT encoding — the process of transforming a problem into a SAT problem — in a form that is accessible to readers with basic knowledge of propositional logic. Also, instead of merely providing a theoretical exposition, I wanted to provide executable examples of how well known computer science problems can be mechanically encoded as SAT problems and solved using off-the-shelf SAT solvers.

In this context, here’s my first brain dump about SAT encoding :)

Satisfiability (SAT)

Given a boolean formula B composed of a set of propositional variables V and the & (and), | (or), and ! (negation) boolean connectives, the satisfiability (SAT) problem asks “is there an assignment M of true (T) or false (F) values to the variables V such that B evaluates to true under M?” If such an assignment M exists, then it is said to satisfy B and it is referred to as a model of B. For example, given a formula B=(a|b) & (!a|b) & (a|!b), the answer to the corresponding SAT problem is yes and M=[a:T, b:T] is a model of B.

CNF

A boolean formula is in Conjunctive Normal Form (CNF) if the formula is a conjunction (and) of clauses where each clause is a disjunction (or) of literals and each literal is either a propositional variable or the negation of a propositional variable. The above formula B is an example of CNF formula.

There has been lot of effort in devising techniques and creating tools to solve SAT problems, i.e., to determine if a CNF formula is satisfiable and identify the model of the formula. We refer to such tools as SAT solvers.

SAT Encoding

Satisfiability is interesting as any problem can be encoded as a CNF formula and a SAT solver can be used to solve the corresponding SAT problem; of course, being able to find an answer is a different discussion :)

Illustration

To illustrate how such encoding may work, consider the simple problem of sorting three numbers by encoding it as a SAT problem.

We will represent the three numbers as integer variables N1, N2, and N3. Since there are three numbers, each number can occur in one of the three positions P1, P2, and P3 in the sorted output where the number in position P1 is less than the number in position P2 is less than the number in position P3. We can represent each of these nine possibilities by a propositional variable vNxPm that denotes number Nx occurs in position Px in the output.

Given this construction, all solutions to this problem have to satisfy the following constraints.

1. Each number Nx can occur in only one position. Specifically, for each Nx, exactly one of vNxPm should be true.
2. Each position Pm can contain only one number. Specifically, for each Pm, exactly one of vNxPm should be true.
3. If Nx occurs to the left of Ny in the output, then Nx should be less than or equal to Ny. Specifically, if vNxPm and vNyPn are true and m=n-1, then Nx ≤ Ny should be true.

To encode the problem as a SAT problem, we have to translate all of these constraints into a single CNF formulae. Here’s how we can do it.

1. The first constraint can be expressed as a conjunction of two constraints: Nx occurs in at least one position and Nx occurs in at most one position.
   The first of these two constraints can be easily expressed as a CNF formula (vNxP1|vNxP2|vNxP3).
   The second of these two constraints is not so easy to express as a CNF formula because the constraint translates into
   i) if vNxP1, then both vNxP2 and vNxP3 should be false,
   ii) if vNxP2, then both vNxP3 and vNxP1 should be false, and
   iii) if vNxP3, then both vNxP1 and vNxP2 should be false.
   (i) can be expressed as a conjunction: if vNxP1, then vNxP2 is false and if vNxP1, then vNxP3 is false. As a boolean formula, we can write it as
   (vNxP1 -> !vNxP2) & (vNxP1 -> !vNxP3).
   Since A->B is logically equivalent to !A|B, we can rewrite the formula as
   (!vNxP1|!vNxP2) & (!vNxP1|!vNxP3), which is in CNF.
   Similarly, we can rewrite (ii) and (iii) as
   (!vNxP2|!vNxP3) & (!vNxP3|!vNxP1)
   and
   (!vNxP3|!vNxP1) & (!vNxP3|!vNxP2), respectively.
   So, for each Nx and for each equivalent circular permutations [Pm, Pn, Po] of [P1, P2, P3] sequence, we can express the first constraint as a CNF formula:(vNxPm|vNxPn|vNxPo) & (!vNxPm|!vNxPn) & (!vNxPm|!vNxPo). Consequently, we will represent this constraint with 3x3x3=27 clauses.
2. Since constraint 2 is similar to 1, for each Pm and for each equivalent circular permutations [Nx, Ny, Nz] of [N1, N2, N3] sequence, we can express the second constraint as a CNF formula:
   (vNxPm|vNyPm|vNzPm) & (!vNxPm|!vNyPm) & (!vNxPm|!vNzPm). Consequently, we will represent this constraint with 3x3x3=27 clauses.
3. As integer operators cannot occur in boolean formulae, we have to enumerate the possibilities to express the third constraint as a boolean formula. Since only consecutive positions are considered (m=n-1), we consider position pairs (P1, P2) and (P2, P3).
   Also, since relational operators cannot occur in boolean formulae, we have to encode the relations as propositional variables: for each pair of numbers (Nx,Ny), vNxLNy represents Nx ≤Ny, i.e., if vNxLNy is true if and only if Nx≤Ny.
   Now, for each position pair (Pm, Pn) and number pair (Nx, Ny), we can express the third constraint as a boolean formula: ((vNxPm & vNyPn) -> vNxLNy). As we did before, we can rewrite it as (!(vNxPm & vNyPn)|vNxLNy) which is equivalent to (!vNxPm|!vNyPn|vNxLNy). Consequently, we will represent this constraint with 2x9=18 clauses.

At the end of this encoding, we will have a total of 60 clauses that we then combine into a CNF formula.

Independent of the numbers to be sorted, the resulting formula will always be the same. So, once we have encoded the problem as a CNF formula, we can reuse the formula with minor extension to solve different problem instances.

For example, to sort the numbers 10, 3, and 4 using the above encoding, we map the numbers to N1, N2, and N3, we determine the truth value of vNxLNy for each number pair based on the mapping, and extend the CNF formula from the encoding with one clause denoting the truth value of Nx≤Ny for each pair of numbers (Nx, Ny), i.e., if Nx≤Ny, then clause vNxLNy is added; otherwise, clause !vNxLNy is added. We feed the resulting CNF formula to a SAT solver and extract the result from the resulting model: each vNxPm variable that is assigned true in the model is interpreted as Nx occuring in position Pm in the sorted output.

Is this optimal in size?

No but it can be.

For example, while encoding constraint 1, we decided (for demonstration purposes) to generate (vNxPm|vNxPn|vNxPo) & (!vNxPm|!vNxPn) & (!vNxPm|!vNxPo) for every number Nx and circular permutation pair. This will end up adding two duplicates of (vNxPm|vNxPn|vNxPo) clause due to symmetry.

Another example is, while encoding constraint 3, if the truth value of vNxLNy is determined to be true, then the containing clause need not be generated as it will trivially be true. If we ignore this observation during encoding, we may end up generating useless clauses. The same observation applies to the literal !vNxLNy.

Depending on how we state constraints and encode them as clauses, we may generate redundant clauses and possibly redundant propositional variables that can bloat the final formula and may contribute to the execution time. So, we should watch out for redundancy during SAT encoding.

Ok, can this really work?

Here’s a Groovy script that sorts any three given numbers by encoding the sorting problem as a SAT problem and solving it using Z3 solver.

Reflections

Clearly, a tedious process to solve a simple problem of sorting three numbers. One that should be avoided in real systems :)

That said, it does illustrate how a problem involving integer arithmetic and relational operators can be encoded and solved as a SAT problem.

Further, as you might have observed, the SAT encoding relies heavily on enumeration of possibilities and it was composed of just two steps:

1. Identifying various constraints on the input to the problem, the output of the problem, and the relation between the input and the output.
2. Expressing these constraints in terms of common constraint patterns that can be easily translated into CNF formulae.

In this sense, using SAT encoding is a simpler and more mechanical approach to solve problems provided 1) identifying required constraints is easy and 2) existing SAT solvers can find models of any given formula (when they exist) in a reasonable amount of time. Don’t you think?

For You To Do

Think how can the sorter be extended to sort any given n numbers.

What next?

Next time, I will list common constraint patterns and their encodings as CNF formulae.