A Primer on Boolean Satisfiability
June 23, 2017
First steps to adding the magic of SAT to your problemsolving toolbox.
The SAT problem asks if a boolean formula has a satisfying assignment—a way to bind its variables to values that makes the formula evaluate to true.
SAT is a classic NPcomplete problem. It’s easy to check the correctness of a solution (by evaluating the formula), but there is no known polynomialtime algorithm for finding one. If we had such an algorithm, we could solve every hard (NP) problem by efficient reduction to SAT. But as far as we know, the worst case scenario for deciding SAT involves trying all possible assignments for a formula with variables.
The good news is that the worst case happens surprisingly rarely in practice. Modern SAT solvers routinely defy the intractability of SAT to decide formulas with millions of variables and constraints. This has made SAT a goto approach for solving hard problems in realworld applications such as configuring cars, verifying microchips and code, and flying space shuttles.
This post explains the basics of SAT and its applications. We’ll review the syntax and semantics of propositional (boolean) logic, define satisfiability more precisely, talk about methods for checking satisfiability, and see how to transform boolean formulas into CNF, the input language of SAT solvers. We’ll also build a tiny toy SAT solver based on DPLL, the algorithm at the core of all modern solvers.^{1}
 Propositional Logic
 Satisfiability and Validity
 Checking Satisfiability and Validity
 Normal Forms
 SAT Solving with DPLL
 Next Steps
The complete source code for this post can be found here.
Propositional Logic
Syntax
A formula in propositional logic is made up of constants, variables, and logical connectives. There are two constant symbols, and , and infinitely many variable identifiers, . The logical connectives include the standard operators of boolean algebra: , , , , and . Books and research papers often write atom to describe a variable or a constant, and literal to describe an atom or its negation.
 An atom is
 a constant (true) or (false)
 a variable
 A literal is an atom or its negation .
 A formula is an atom or the application of a logical connective to formulas:
 (not)
 (and)
 (or)
 (implies)
 (iff).
Semantics
The meaning of a formula is a truth value or . To determine a formula’s meaning, we evaluate it in an environment, called an interpretation, that assigns truth values to the formula’s variables. For example, is one possible interpretation for the formula .
We write if the formula evaluates to under the interpretation , and otherwise. The symbols and are read as “satisfies” and “falsifies”, respectively. An interpretation that satisfies a formula is also called its model. The following rules show how to evaluate formulas:
 (the constant evaluates to under every interpretation)
 (the constant evaluates to under every interpretation)
 if and only if
 if and only if
 if and only if and
 if and only if or
 if and only if or
 if and only if either and or and .
These rules operationalize the familiar truth table method for evaluating boolean expressions. They correspond closely to the code you’d write to implement an interpreter for propositional logic. For example, here is such an interpreter in Racket:
; Returns true (#t) if I ⊨ f and false (#f) if I ⊭ f.
(define (evaluate f I)
(match f
['⊤ true]
['⊥ false]
[(? symbol? xi) (lookup I xi)]
[`(¬ ,f1) (not (evaluate f1 I))]
[`(∧ ,fs ...) (for/and ([fi fs]) (evaluate fi I))]
[`(∨ ,fs ...) (for/or ([fi fs]) (evaluate fi I))]
[`(→ ,f1 ,f2) (or (not (evaluate f1 I)) (evaluate f2 I))]
[`(↔ ,f1 ,f2) (equal? (evaluate f1 I) (evaluate f2 I))]))
> ; { x1 ↦ false, x2 ↦ true } ⊨ ¬x1 ∧ x2
(evaluate '(∧ (¬ x1) x2) (assign 'x1 false 'x2 true))
#t
> ; { x1 ↦ true, x2 ↦ true } ⊭ ¬x1 ∧ x2
(evaluate '(∧ (¬ x1) x2) (assign 'x1 true 'x2 true))
#f
Satisfiability and Validity
Satisfiability
Given a way to evaluate formulas, we can now state what it means for a formula to be satisfiable:
A formula is satisfiable if and only if there is an interpretation under which evaluates to ; that is, for some . Otherwise, is unsatisfiable.
Validity
Another important property of formulas is validity:
A formula is valid if and only if it evaluates to under all interpretations; that is, for all . We write to say that is valid.
Duality
Satisfiability and validity are duals of each other:
A formula is valid if and only if its negation is unsatisfiable.
This simple observation follows directly from the definitions of satisfiability and validity and the semantics of negation. It also has a key practical consequence:
If we have a procedure for checking satisfiability, we can use it to check validity, and vice versa.
As a result, a SAT solver is both a satisfiability checker and a theorem prover.
This is why we can use SAT (and SMT) solvers to build tools that reason about code. For example, to prove that a program correctly implements its specification, a verifier needs to check the validity of the formula , where encodes all program behaviors and encodes the specification. Automated verifiers do this by using solvers to decide if , the negation of the verification formula, is satisfiable. If so, a satisfying assignment represents a concrete counterexample: a behavior of the program that violates the specification. If not, the program is correct.
Checking Satisfiability and Validity
So, how do we show that a formula is satisfiable or, dually, valid? There are two main approaches: search and deduction. As we’ll see later on, a SAT solver uses both.
Search
The search approach is straightforward. To decide if a formula is valid, we check that it evaluates to under every possible interpretation.
Using our Racket interpreter for propositional logic, we can implement the search approach as follows:
; Returns true (#t) if f is valid and false (#f) otherwise,
; by checking that every interpretation satisfies f.
(define (searchvalid? f)
(let allsat? ([vars (variables f)] [I (assign)])
(match vars
[(list)
(evaluate f I)]
[(list v vs ...)
(and (allsat? vs (extend I v false))
(allsat? vs (extend I v true)))])))
> ; ⊨ (x1 ∧ x2) → (x1 ∨ ¬x2)
(searchvalid? '(→ (∧ x1 x2) (∨ x1 (¬ x2))))
#t
> ; ⊭ (x1 ∨ ¬x2) → (x1 ∧ x2)
(searchvalid? '(→ (∨ x1 (¬ x2)) (∧ x1 x2)))
#f
Deduction
The deduction approach is more involved.
We start by assuming that the formula is invalid; so, for some .
Then, we apply proof rules for propositional logic to derive all possible consequences of our assumption. A proof rule consists of a premise and a conclusion. The premise states the facts that have to be established (either from the assumption or previous derivations) before we can apply the rule. The conclusion states the facts that we can derive (add to the set of known facts) as the result of applying the rule.
①  ② 
③  ④ 
⑤  ⑥ 
⑦  ⑧ 
⑨  ⑩ 
Applying proof rules produces a proof tree, with branches resulting from the introduction of alternative facts. If every branch of the proof tree contains a contradiction (e.g., both the fact and the fact ), then we know that our initial assumption was untrue and must be valid. Otherwise, is invalid, and we can read off the falsifying interpretation from the proof tree.
For example, we can prove that is valid as follows:
 by assumption
 by 1 and ⑧
 by 1 and ⑧
 by 3 and ③
 by 3 and ③, branch
 by 5 and ⑨, contradicts 4
 by 5 and ⑨, contradicts 2
Here is an excerpt from an implementation of the deduction approach:
; Returns true (#t) if f is valid and false (#f) otherwise,
; by checking that all branches of f's proof tree are
; closed (i.e., contain a contradiction).
(define (deducevalid? f)
(let allclosed? ([facts `((I ⊭ ,f))]) ; assumption
(match facts
[`(,gs ... (I ⊨ (¬ ,f1)) ,hs ...) ; (1)
(allclosed? `((I ⊭ ,f1) ,@gs ,@hs))]
; proof rules (2)(10)
[(or `(,_ ... (I ⊨ ,fi) ,_ ... (I ⊭ ,fi) ,_ ...)
`(,_ ... (I ⊭ ,fi) ,_ ... (I ⊨ ,fi) ,_ ...))
(printf "Contradiction on ~a: ~a\n" fi facts)
#t]
[_
(printf "Open branch: ~a\n" facts)
#f])))
> ; ⊨ (x1 ∧ (x1 → x2)) → x2
(deducevalid? '(→ (∧ x1 (→ x1 x2)) x2))
Contradiction on x1: ((I ⊭ x1) (I ⊨ x1) (I ⊭ x2))
Contradiction on x2: ((I ⊨ x2) (I ⊨ x1) (I ⊭ x2))
#t
> ; ⊭ (x1 ∨ ¬x2) → (x1 ∧ x2)
(deducevalid? '(→ (∨ x1 (¬ x2)) (∧ x1 x2)))
Contradiction on x1: ((I ⊨ x1) (I ⊭ x1))
Open branch: ((I ⊭ x2) (I ⊭ x1))
#f
Normal Forms
As we just saw, generic search and deduction can decide the satisfiability (or validity) of arbitrary propositional formulas. But practical decision procedures, including SAT solvers, are designed to work on formulas with restricted syntactic structure.
These restrictions are called normal forms because every formula in a given logic has an equivalent formula in the normal form. Two formulas are equivalent if and only if they have the same meaning under every interpretation—that is, is valid.
NNF, DNF, and CNF
There are three widely used normal forms for propositional logic.
 Negation Normal Form (NNF)
 A formula in NNF uses only , , and as connectives, with negations appearing only in literals. For example, is in NNF but is not.
 Disjunctive Normal Form (DNF)
 A formula in DNF is a disjunction of conjunctions of literals: , where is a literal. For example, is in DNF.
 Conjunctive Normal Form (CNF)
 A formula in CNF is a conjunction of disjunctions of literals: , where is a literal. For example, is in CNF. The disjunctive subformulas of a CNF formula, , are called clauses.
We can convert any propositional formula to these forms using simple rewrite rules. ```racket ; Converts f to NNF by first limiting operators ; to ∧∨¬ and then pushing ¬ down to the leaves ; (literals) of the formula. (define (nnf f) (nnfneg (nnfops f)))
; Converts f to DNF by first converting f to NNF, ; then distributing ∧ over ∨, and finally flattening ; out nested conjunctions and disjunctions. (define (dnf f) (unnest (distribute ‘∧ ‘∨ (nnf f))))
; Converts f to CNF as done for the DNF conversion but ; swapping ∧ for ∨ and vice versa. (define (cnf f) (unnest (distribute ‘∨ ‘∧ (nnf f))))
; NNF: ¬ (x1 → (¬ (x1 ∧ x2))) (nnf
(¬ (→ x1 (¬ (∧ x1 x2))))) '(∧ x1 (∧ x1 x2)) ; DNF: (x1 ∨ x2) ∧ (¬ (x3 ∧ x4)) (dnf
(∧ (∨ x1 x2) (¬ (∧ x3 x4)))) ‘(∨ (∧ x1 (¬ x3)) (∧ x2 (¬ x3)) (∧ x1 (¬ x4)) (∧ x2 (¬ x4))) ; CNF: (x1 ∧ x2) ∨ (¬ (x3 ∨ x4)) (cnf(∨ (∧ x1 x2) (¬ (∨ x3 x4)))) '(∧ (∨ x1 (¬ x3)) (∨ x2 (¬ x3)) (∨ x1 (¬ x4)) (∨ x2 (¬ x4)))
``
Properties of normal forms
What makes NNF, DNF, and CNF practically interesting? CNF is the input language of SAT solvers. NNF is often used by SATbased tools as an intermediate representation for optimizing formulas prior to CNF conversion. And DNF is easy to decide: we can decide the satisfiability of DNF formulas in linear time!^{2}
So why do SAT solvers use CNF instead of DNF? After all, can’t we trivially decide the satisfiability of any propositional formula by first converting it to DNF?
The problem is that converting an arbitrary formula to an equivalent formula in DNF can lead to an exponential increase in formula size, as seen in the above code example. By using DNF, we’d just pay the exponential penalty in the conversion process instead of the decision process.
At this point, you might notice that the same kind of exponential explosion happens when converting a formula to an equivalent CNF representation. Given this, how is it possible to make effective use of SAT solvers, which take CNF formulas as input?
Equisatisfiability
The key is to observe that we don’t need to convert formulas to an equivalent CNF representation to check their satisfiability. Instead, all we need is to convert the input formula to a CNF formula such that and are either both satisfiable or both unsatisfiable. This relation between and is called equisatisfiability, and it’s a weaker notion than equivalence (for example, and are equisatisfiable though not equivalent). But crucially, we have an efficient procedure for converting any propositional formula to an equisatisfiable CNF formula.
Tseitin’s encoding
To convert a formula to an equisatisfiable CNF representation, we use a procedure called Tseitin’s encoding. This procedure has two important properties. First, the size of the resulting CNF formula is linear in the size of the original formula . Second, a satisfying interpretation for , if any, can be straightforwardly converted to a satisfying interpretation for . So, applying a SAT solver to Tseitin’s encoding of a formula lets us obtain not only a yes/no decision but also a satisfying interpretation if the solver produces one.
The key idea behind Tseitin’s encoding is to use new propositional variables, called auxiliary variables, to refer to the subformulas in the input formula .
We begin by introducing a fresh propositional variable to represent the subformula . This involves creating a conjunction of formulas of the form , and then replacing each occurrence of with in this conjunction.
For example, to transform , we generate the following conjunction, where represents and represents :
Next, we convert the resulting conjunction to an equivalent CNF formula using
the cnf
procedure we saw previously. Continuing the above example, we’d
produce the following clauses, which are satisfiable if and only if the original
formula is satisfiable:
CNF representation of  
CNF representation of  
CNF representation of  
CNF representation of 
This conversion step won’t lead to exponential explosion because the introduction of auxiliary variables eliminated all nested subexpressions from the ’s. In particular, the initial transformation step ensures that the righthand side of each formula is an application of a logical connective to original or auxiliary variables.
Putting these two steps together, we get a basic implementation of Tseitin’s encoding:
; Converts f to an equisatisfiable formula in CNF
; using Tseitin's encoding.
(define (tseitin f)
(cnf (auxiliaries f)))
> ; Tseitin: x1 → (x2 ∧ x3)
(tseitin `(→ x1 (∧ x2 x3)))
'(∧
a6743
(∨ (¬ a6743) (¬ x1) a6744)
(∨ x1 a6743)
(∨ (¬ a6744) a6743)
(∨ x2 (¬ a6744))
(∨ x3 (¬ a6744))
(∨ (¬ x2) (¬ x3) a6744))
SAT Solving with DPLL
The DPLL algorithm
A SAT solver is a procedure for deciding if a given CNF formula is satisfiable. Most SAT solvers are based on the DPLL algorithm, invented in 1962 by Davis, Putnam, Logemann, and Loveland. DPLL is a sound and complete procedure for deciding the satisfiability of CNF formulas: it is guaranteed to terminate, and it outputs “yes” if and only if the input formula has a satisfying interpretation.
The key idea behind DPLL is to combine backtracking search with deduction, as shown in the following pseudocode:
1
2
3
4
5
6
DPLL(f):
g = BCP(f)
if g reduces to ⊤ then return true
if g reduces to ⊥ then return false
x = choose(vars(g))
return DPLL(g ∧ x)  DPLL(g ∧ ¬x)
Given a CNF formula , DPLL first performs deduction in the form of boolean constraint propagation (BCP). The BCP procedure applies unit resolution until fixed point:
The unit rule uses singleliteral, or unit, clauses contained in to make two simple deductions. First, if includes both a unit clause and a clause that contains , then we can replace with in . Second, if contains the negation of , then we can replace with in .
It’s easy to see that BCP leads to valid conclusions (it’s sound) but that it can’t decide the satisfiability of arbitrary CNF formulas (it’s incomplete).
To ensure completeness, DPLL employs backtracking search (lines 56). If BCP doesn’t manage to reduce to a constant, then we pick one of the remaining variables, and call DPLL recursively assuming that the variable is either or . If the formula is satisfiable under either assumption, then we know that it has a satisfying assignment (expressed in the assumptions). Otherwise, the formula is unsatisfiable.
A toy SAT solver
While competitive SAT solvers make many improvements to DPLL to make it scale, even a basic implementation of the algorithm is quick to solve problems with a hundred or so variables and clauses:
; If f is satisfiable, returns a model of f given as a list of
; integers (positive or negative literals). Otherwise returns false.
(define (dpll f)
(define g (bcp f))
(match g
[`((,lit) ...) lit] ; model
[`(,_ ... () ,_ ...) #f] ; unsat
[`((,assigned) ... (,lit ,_ ,_ ...) ,_ ...) ; search
(let* ([undecided (drop g (length assigned))]
[result (or (dpll `((,lit) ,@undecided))
(dpll `((,( lit)) ,@undecided)))])
(and result `(,@assigned ,@result)))]))
The above implementation represents a CNF formula as a list of clauses. A clause
is represented as a list of integers, where positive and negative integers stand
for positive and negative literals, respectively. For example, we represent the
formula as the list '((1
3) (1 2 3))
. The empty list represents the empty clause, which evaluates to
under all interpretations.
Applying our toy solver to this problem, which contains 50 variables and 80 clauses, produces a model in a millisecond:
> (define f (readcnf "example.cnf"))
> (time (dpll f))
cpu time: 1 real time: 1 gc time: 0
'( 16 17 21 28 13 ...)
A naive backtracking search, on the other hand, doesn’t come back after two hours when applied to the same problem:
; If f is satisfiable, returns a model of f given as a list of
; integers (positive or negative literals). Otherwise returns false.
(define (searchsat f)
(let search ([vars (variables f)] [I (list)])
(if (evaluate f I)
I
(match vars
[(list) #f]
[(list v vs ...)
(or (search vs (cons v I))
(search vs (cons ( v) I)))]))))
> (define f (readcnf "example.cnf"))
> (time
(withhandlers ([exn? (lambda (e) (displayln (exnmessage e)))])
(searchsat f)))
user break
cpu time: 10007420 real time: 10003982 gc time: 6017
Next Steps
To learn more about how competitive SAT solvers work, see these excellent review papers:
 [1] Joao MarquesSilva, Ines Lynce, and Sharad Malik. Chapter 4: ConflictDriven Clause Learning SAT Solvers. Handbook of Satisfiability. 2008.
 [2] Carla P. Gomes, Henry Kautz, Ashish Sabharwal, and Bart Selman. Chapter 2: Satisfiability Solvers. Handbook of Knowledge Representation. 2008.
Or take a look at the source code for MiniSAT, on which most other solvers are based.
To choose the best solver for your problem, check out the results from the latest SAT competition.
Happy SAT solving!

This post is based on Lecture 1 of my graduate course on ComputerAided Reasoning for Software. The lecture covers the material in Chapter 1 of The Calculus of Computation and Decision Procedures. ↩

To decide the satisfiability of a DNF formula, we scan each of the subformulas to find one that doesn’t include both a variable and its negation, or the constant . An interpretation that satisfies this subformula (by assigning and to the nonnegated and negated variables, respectively) satisfies the entire formula. ↩