Introduction to Propositional Satisfiability
IA085: Satisfiability and Automated Reasoning
Martin Jonáš
FI MUNI, Spring 2024
Contents
Propositional satisfiability (SAT)
• (A ∨ ¬B) ∧ (¬A ∨ C)
• is it satisfiable?
Satisfiability modulo theories (SMT)
• x = 1 ∧ x = y + y ∧ y > 0
• is it satisfiable over reals?
• is it satisfiable over integers?
Automated theorem proving (ATP)
• axioms: ∀x (x + x = 0), ∀x∀y (x + y = y + x)
• do they imply ∀x∀y ((x + y) + (y + x) = 0)?
1 / 38
Contents
For each of the problems (SAT/SMT/ATP)
• necessary definitions and theoretical results
• algorithms to solve the problem
• usage in practice and practical considerations
2 / 38
Organization of the Course
Schedule and Requirements
During semester
• lecture every week (except April 10, May 1, May 8)
• seminar every other week
• project (write your own small SAT solver) -- mandatory
Exam
• oral exam
• you will have access to the lecture slides
3 / 38
Project
Implement your own SAT solver
• you can use any reasonable programming language (C, C++, C#, Go, Java,
Python, Rust, . . .)
• you are encouraged to work in pairs (but you do not have to)
• technical requirements are specified in the information system
• more advanced features → bonus points for the exam
• the scores will be evaluated periodically through the semester, you will see
the ranking
4 / 38
Who am I?
• author of SMT solver Q3B for quantified formulas over bit-vector theory
• for 3 years post-doctoral researcher in Fondazione Bruno Kessler: research
focused on SMT-based verification of software and SAT-based verification of
hardware
• PhD thesis about satisfiability of quantified formulas over bit-vector theory
• author of several research papers about solving SMT and using it in practice
• co-organizer of SMT-COMP 2024
5 / 38
Propositional Logic
Propositional logic
Propositional logic deals with propositions, their relationships, and arguments
based on them.
Does not deal objects and their properties, just with separate atomic claims.
``Martin has brown hair''
``Martin does not have hair''
No relationship as far as propositional logic is concerned.
.
6 / 38
Propositional logic
Propositional logic deals with propositions, their relationships, and arguments
based on them.
Does not deal objects and their properties, just with separate atomic claims.
``Martin has brown hair'' (A)
``Martin does not have hair'' (B)
No relationship as far as propositional logic is concerned.
.
6 / 38
Propositional logic
Propositional logic deals with propositions, their relationships, and arguments
based on them.
Does not deal objects and their properties, just with separate atomic claims.
``Martin has brown hair'' (A)
``Martin does not have hair'' (B)
No relationship as far as propositional logic is concerned.
``Martin has brown hair''
if ``Martin has brown hair`` then ``Martin does have hair''
Implies ``Martin does have hair'' .
6 / 38
Propositional logic
Propositional logic deals with propositions, their relationships, and arguments
based on them.
Does not deal objects and their properties, just with separate atomic claims.
``Martin has brown hair'' (A)
``Martin does not have hair'' (B)
No relationship as far as propositional logic is concerned.
``Martin has brown hair'' (A)
if ``Martin has brown hair`` then ``Martin does have hair'' (A → B)
Implies ``Martin does have hair'' (B).
6 / 38
Syntax
Let V = {A, B, C, . . .} be a countable set of propositional variables. The set of
propositional formulas is defined inductively as
• ⊤ and ⊥ are propositional formulas,
• v is a propositional formula for each v ∈ V (called propositional atom),
• if φ is a propositional formula, ¬φ is a propositional formula,
• if φ and ψ are propositional formulas, φ ∧ ψ, φ ∨ ψ, φ → ψ, and φ ↔ ψ are
propositional formulas.
Example
• A ∧ B
• (A ∨ B) ↔ ¬C
Formulas of form v or ¬v are called literals.
7 / 38
Semantics: Truth Assignments
Atoms(φ) = the set of all atoms of formula φ.
(Total) truth assignment for formula φ
• assigns true (⊤) or false (⊥) to each propositional variable in φ
• a function µ: V′ → {⊤, ⊥} where Atoms(φ) ⊆ V′
• can be written as a set of non-contradictory literals containing all variables
of φ
Example
• formula φ = A ∨ B,
• total assignment µ(A) = ⊤, µ(B) = ⊥,
• written as µ = {A, ¬B}.
8 / 38
Semantics: Satisfaction
Define when a truth assignment µ satisfies the formula φ, written µ |= φ:
• µ |= ⊤,
• µ |= v if µ(v) = ⊤,
• µ |= ¬ψ if not µ |= ψ,
• µ |= ψ1 ∧ ψ2 if µ |= ψ1 and µ |= ψ2,
• µ |= ψ1 ∨ ψ2 if µ |= ψ1 or µ |= ψ2,
• µ |= ψ1 → ψ2 if not µ |= ψ1 or µ |= ψ2,
• µ |= ψ1 ↔ ψ2 if µ |= ψ1 if and only if µ |= ψ2,
9 / 38
Semantics: Model
If µ |= φ, we say that µ is a model of φ.
Example
{A, ¬B, C} is a model of A ∧ (B ↔ ¬C)
An assignment µ is a partial model of φ if each extension of µ that is a truth
assignment to φ is a model of φ.
Example
{A, B} is a partial model of (A ∧ B) ∨ (A ∧ C)
10 / 38
Propositional Entailment
Formula φ propositionally entails formula ψ (written φ |= ψ) if every µ that is a
truth assignment for both φ and ψ satisfies
if µ |= φ then also µ |= ψ
Example
• A |= A ∨ B
• (A → B) ∧ A |= B
• (A ∨ B) ∧ (¬A ∨ C) |= (B ∨ C)
• A ̸|= A ∧ B
11 / 38
Propositional Equivalence
Formulas φ and ψ are propositionally equivalent (written φ ≡ ψ) if
φ |= ψ and ψ |= φ
Example
• A ∧ (B ∨ C) ≡ (A ∧ B) ∨ (A ∧ C)
• A ∧ (A ∨ B) ≡ A
• ¬(A ∧ B) ≡ ¬A ∨ ¬B
12 / 38
Negation Normal Form
Negation Normal Form (NNF)
• negations are applied only to propositional atoms
• the formula does not contain implication (→) and equivalence (↔)
Transformation to NNF
1. rewrite all φ ↔ ψ to (φ → ψ) ∧ (φ ← ψ)
2. rewrite all φ → ψ to ¬φ ∨ ψ
3. apply De Morgan rules until fixed point
– rewrite ¬(φ ∧ ψ) to (¬φ) ∨ (¬ψ)
– rewrite ¬(φ ∨ ψ) to (¬φ) ∧ (¬ψ)
13 / 38
Conversion to NNF: Complexity
What is the complexity of conversion to NNF?
φ ↔ ψ (¬φ ∨ ψ) ∧ (φ ∨ ¬ψ)
Each equivalence doubles the size of the formula → translation can be
exponential!
14 / 38
Conversion to NNF: Complexity
What is the complexity of conversion to NNF?
φ ↔ ψ (¬φ ∨ ψ) ∧ (φ ∨ ¬ψ)
Each equivalence doubles the size of the formula → translation can be
exponential!
Or is it? It depends on the representation of the formulas.
14 / 38
Representation of Formulas
(¬φ ∨ ψ) ∧ (φ ∨ ¬ψ)
Tree
φ ψ φ ψ
¬ ¬
∨ ∨
∧
Directed acyclic graph (DAG)
φ ψ
¬ ¬
∨ ∨
∧
In practice, we represent formulas as DAGs.
15 / 38
Conversion to NNF: Complexity
Theorem
When representing formulas as DAGs, the transformation to NNF is linear.
Proof idea.
The DAG contains two nodes for each subformula φ: one for φ, one for ¬φ.
16 / 38
Conversion to NNF: Complexity
Theorem
When representing formulas as DAGs, the transformation to NNF is linear.
Proof idea.
The DAG contains two nodes for each subformula φ: one for φ, one for ¬φ.
Proof details (bonus).
Recursively define function NNF(φ) = (φ+, φ−). Given NNF(ψ) = (ψ+, ψ−) and
NNF(ρ) = (ρ+, ρ−):
NNF(ψ ∧ ρ) = (ψ+
∧ ρ+
, ψ−
∨ ρ−
)
NNF(¬ψ) = (ψ−
, ψ+
)
NNF(ψ ↔ ρ) = ((ψ−
∨ ρ+
) ∧ (ψ+
∨ ρ−
)
positive
, (ψ+
∧ ρ−
) ∨ (ψ−
∧ ρ+
)
negative
).
For more details, see Property 1 in Gabriele Masina, Giuseppe Spallitta, Roberto
Sebastiani: On CNF Conversion for SAT Enumeration.
16 / 38
Conjunctive Normal Form
Clause
• disjunction of literals
• A ∨ ¬B ∨ C
• written as {A, ¬B, C} thanks to idempotence, commutativity, and associativity
• what is {}?
Formula in Conjunctive Normal Form (CNF)
• conjunction of clauses
• (A ∨ ¬B ∨ C) ∧ (B ∨ ¬C) ∧ C
• written as {{A, ¬B, C}, {B, ¬C}, {C}} thanks to idempotence, commutativity,
and associativity
• what is {}?
• what is {∅}?
17 / 38
Conjunctive Normal Form
• Easy to represent (clause = list[int], formula = list[clause]).
• Easy to write algorithms, do not have to deal with the structure of the
formula.
• Most of modern SAT solvers have input in CNF.
18 / 38
Conjunctive Normal Form
Transformation to CNF (naive)
1. transform to NNF
2. apply distributivity until fixed point
– rewrite φ ∨ (ψ ∧ ρ) to (φ ∨ ψ) ∧ (φ ∨ ρ)
– rewrite (ψ ∧ ρ) ∨ φ to (ψ ∨ φ) ∧ (ρ ∨ φ)
This is again exponential, try with 1≤i≤n(Ai ∧ Bi).
Can we do better? What if the DAG representation is used? What if we use a
different algorithm?
19 / 38
Conversion to CNF: Naive
Theorem
There exists an infinite family of formulas Φ = {φi | i ∈ N} such that for each
equivalent family of formulas with φCNF
i ≡ φi, the size |φCNF
i | grows exponentially
with respect to |φi| (even for DAG representation).
20 / 38
Conversion to CNF: Naive
Theorem
There exists an infinite family of formulas Φ = {φi | i ∈ N} such that for each
equivalent family of formulas with φCNF
i ≡ φi, the size |φCNF
i | grows exponentially
with respect to |φi| (even for DAG representation).
Proof.
Let parityi(A1, A2, . . . , Ai) = A1 ⊕ A2 ⊕ . . . ⊕ Ai. We can show that
• parityi can be defined by a formula φi of size O(i),
• each formula φCNF
i in CNF that defines parityi has 2i−1 clauses.
20 / 38
Conversion to CNF: Naive
Theorem
There exists an infinite family of formulas Φ = {φi | i ∈ N} such that for each
equivalent family of formulas with φCNF
i ≡ φi, the size |φCNF
i | grows exponentially
with respect to |φi| (even for DAG representation).
Proof.
Let parityi(A1, A2, . . . , Ai) = A1 ⊕ A2 ⊕ . . . ⊕ Ai. We can show that
• parityi can be defined by a formula φi of size O(i),
• each formula φCNF
i in CNF that defines parityi has 2i−1 clauses.
We cannot do better than exponential.
20 / 38
Conversion to CNF: Naive
Theorem
There exists an infinite family of formulas Φ = {φi | i ∈ N} such that for each
equivalent family of formulas with φCNF
i ≡ φi, the size |φCNF
i | grows exponentially
with respect to |φi| (even for DAG representation).
Proof.
Let parityi(A1, A2, . . . , Ai) = A1 ⊕ A2 ⊕ . . . ⊕ Ai. We can show that
• parityi can be defined by a formula φi of size O(i),
• each formula φCNF
i in CNF that defines parityi has 2i−1 clauses.
We cannot do better than exponential.
Or can we? Yes, we can! Later today.
20 / 38
Disjunctive Normal Form
Cube
• conjunction of literals
• A ∧ ¬B ∧ C
Formula in Disjunctive Normal Form (DNF)
• disjunction of cubes
• (A ∧ ¬B ∧ C) ∨ (B ∧ ¬C) ∨ C
We will not be dealing with DNF often in this course.
21 / 38
Propositional Satisfiability (SAT)
Satisfiability Problem
Problem (SAT)
Given a propositional formula, decide whether it is satisfiable.
Problem (CNF-SAT)
Given a propositional formula in CNF, decide whether it is satisfiable.
Problem (3-SAT)
Given a propositional formula in CNF with each clause of size 3, decide whether it
is satisfiable.
22 / 38
Satisfiability Problem
Problem (SAT)
Given a propositional formula, decide whether it is satisfiable.
Problem (CNF-SAT)
Given a propositional formula in CNF, decide whether it is satisfiable.
Problem (3-SAT)
Given a propositional formula in CNF with each clause of size 3, decide whether it
is satisfiable.
22 / 38
Hardness of Propositional Satisfiability: Theory
Theorem
SAT, CNF-SAT, and 3-SAT are NP-complete.
Proof ideas.
• Whether an assignment is a model can be checked in polynomial time.
• A computation of Turing machine of polynomial length can be encoded by a
CNF formula of polynomial size.
There are no known polynomial algorithms for propositional satisfiability.
23 / 38
Hardness of Propositional Satisfiability: Practice
Modern SAT solvers can decide satisfiability of formulas with thousands of
variables and millions of clauses thanks to
• clever algorithms (worst case exponential)
• clever data structures
• clever heuristics
Give it a try:
• MiniSAT (http://minisat.se/)
• CaDiCaL (https://github.com/arminbiere/cadical)
• Kissat (https://github.com/arminbiere/kissat)
24 / 38
Applications: Other Logical Problems
Other logical problems can be reduced1 to satisfiability
Entailment
• φ |= ψ ⇔ φ ∧ ¬ψ is not satisfiable
Validity
• a φ is valid if every total assignment for φ is its model
• φ is valid ⇔ ¬φ is not satisfiable
1
in the sense of Turing reductions
25 / 38
Applications: Hardware Design
[Example from: https://www21.in.tum.de/~lammich/2015_SS_Seminar_SAT/
resources/Equivalence_Checking_11_30_08.pdf]
Are circuits C1 and C2 equivalent?
Is ¬(formula(C1) ↔ formula(C2)) UNSAT? (called a miter formula)
Works only for reasonably small circuits. For larger circuits (millions of gates),
more involved techniques are necessary, e.g., SAT-sweeping.
26 / 38
Applications: Package Dependency
• package P has n versions:
xP
1 , xP
2 , . . ., xP
n
• only one can be installed at a time:
¬xP
i ∨ ¬xP
j for all packages P and versions i ̸= j
• packages have dependencies:
xP
3 → (xQ
1 ∨ xQ
2 ) ∧ xR
8
• I have version 1 of package Q and want to install version 3 of package P:
xP
3 ∧ xQ
8
• what dependencies I need to install:
Is the formula SAT? What is its model?
Used for example by package manager Cabal for Haskell.
27 / 38
Applications: Open Problems in Mathematics
Definition
A triple (a, b, c) ∈ N is called Pythagorean if a2 + b2 = c2.
Question
Can every set of numbers N = {1, 2, . . . , n} be colored by two colors such that
there is no monochromatic Pythagorean triple?
2
https://www.cs.utexas.edu/~marijn/ptn/
28 / 38
Applications: Open Problems in Mathematics
Definition
A triple (a, b, c) ∈ N is called Pythagorean if a2 + b2 = c2.
Question
Can every set of numbers N = {1, 2, . . . , n} be colored by two colors such that
there is no monochromatic Pythagorean triple?
The answer is no (n = 7825) and was found by a SAT solver in 20162. Previous
lower bound was that n = 7664 can be colored.
2
https://www.cs.utexas.edu/~marijn/ptn/
28 / 38
Applications: Open Problems in Mathematics
1. Define a formula Fi whose models are two-colorings of {1, 2, . . . , i} with no
monochromatic Pythagorean triples.
Fi =
(a,b,c) is a Pythagorean triple
(xa ∨ xb ∨ xc) ∧ (¬xa ∨ ¬xb ∨ ¬xc)
2. F7824: 6492 variables and 18930 clauses; F7825: 6494 variables and 18944
clauses.
3. Preprocessing: reduce this to 3740 variables and 14652 clauses; and 3745
variables and 14672 clauses.
4. Use parallel SAT solver and tweak some of its heuristics.
5. Use a parallel machine with 800 cores for 2 days.
6. Find that F7824 is satisfiable and F7825 is unsatisfiable.
7. Get a largest unsatisfiability proof ever (200 terabytes).
29 / 38
Thinking with Clauses
Clauses = Implications
Important view during this course: clauses = implications.
{A, B} (i.e., A ∨ B)
• ¬A → B
• ¬B → A
{A, B, C} (i.e., A ∨ B ∨ C)
• (¬A ∧ ¬B) → C
• (¬A ∧ ¬C) → B
• . . .
30 / 38
2-SAT
2-CNF = formula in CNF with clauses of size 2
2-SAT = decide satisfiability of formula in 2-CNF
Example
Is the following 2-CNF formula satisfiable?
{A, B}, {¬B, C}, {¬C, A}
{¬A, ¬B}, {B, ¬A}, {C, ¬D}
31 / 38
2-SAT
2-CNF = formula in CNF with clauses of size 2
2-SAT = decide satisfiability of formula in 2-CNF
Example
Is the following 2-CNF formula satisfiable?
{A, B}, {¬B, C}, {¬C, A}
{¬A, ¬B}, {B, ¬A}, {C, ¬D}
Theorem
2-SAT can be solved in linear time.
31 / 38
2-SAT
Theorem
2-SAT can be solved in linear time.
32 / 38
2-SAT
Theorem
2-SAT can be solved in linear time.
Proof.
Let φ be in 2-CNF. Construct a graph G = (V, E) with
• V = {v | v ∈ Atoms(φ)} ∪ {¬v | v ∈ Atoms(φ)}
• E = {(¬a, b) | {a, b} ∈ φ}
φ is satisfiable ⇔ G has no cycle that contains both v and ¬v for some v
32 / 38
Encoding Graph Coloring
Given an undirected graph G = (V, E), can it be colored by three colors (red, green,
blue) so that no edge has endpoints of the same color?
Encoding
• variables vr, vg, vb for each v ∈ V
33 / 38
Encoding Graph Coloring
Given an undirected graph G = (V, E), can it be colored by three colors (red, green,
blue) so that no edge has endpoints of the same color?
Encoding
• variables vr, vg, vb for each v ∈ V
• at least one color constraint: {vr, vg, vb} for each v ∈ V
33 / 38
Encoding Graph Coloring
Given an undirected graph G = (V, E), can it be colored by three colors (red, green,
blue) so that no edge has endpoints of the same color?
Encoding
• variables vr, vg, vb for each v ∈ V
• at least one color constraint: {vr, vg, vb} for each v ∈ V
• at most one color constraints {¬vr, ¬vg}, {¬vg, ¬vb}, {¬vr, ¬vb} for each v ∈ V
33 / 38
Encoding Graph Coloring
Given an undirected graph G = (V, E), can it be colored by three colors (red, green,
blue) so that no edge has endpoints of the same color?
Encoding
• variables vr, vg, vb for each v ∈ V
• at least one color constraint: {vr, vg, vb} for each v ∈ V
• at most one color constraints {¬vr, ¬vg}, {¬vg, ¬vb}, {¬vr, ¬vb} for each v ∈ V
• coloring constraint uc → ¬vc for each edge {u, v} ∈ E and each color
c ∈ {r, g, b} ≡ clause {¬uc, ¬vc}
33 / 38
Encoding Graph Coloring
Given an undirected graph G = (V, E), can it be colored by three colors (red, green,
blue) so that no edge has endpoints of the same color?
Encoding
• variables vr, vg, vb for each v ∈ V
• at least one color constraint: {vr, vg, vb} for each v ∈ V
• at most one color constraints {¬vr, ¬vg}, {¬vg, ¬vb}, {¬vr, ¬vb} for each v ∈ V
• coloring constraint uc → ¬vc for each edge {u, v} ∈ E and each color
c ∈ {r, g, b} ≡ clause {¬uc, ¬vc}
• models of the formula ≃ valid colorings
33 / 38
Conversion to CNF: Tseitin encoding
Conversion to equivalent CNF can be exponential, but do we really need
equivalence?
Definition
The formulas φ and ψ are equisatisfiable if both are satisfiable or both
unsatisfiable.
Theorem
For each formula φ there exists an equisatisfiable formula φCNF with O(|φ|)
clauses of size at most three.
Proof.
Tseitin encoding.
34 / 38
Conversion to CNF: Tseitin encoding by example
φ = (A ∧ B) ∨ C
35 / 38
Conversion to CNF: Tseitin encoding by example
φ = (A ∧ B) ∨ C
A B C
∧
∨
35 / 38
Conversion to CNF: Tseitin encoding by example
φ = (A ∧ B) ∨ C
A B C
∧
∨ψ
ρ
35 / 38
Conversion to CNF: Tseitin encoding by example
φ = (A ∧ B) ∨ C
A B C
∧
∨ψ
ρ
(Aρ ↔ (A ∧ B)) ∧
(Aψ ↔ (Aρ ∨ C)) ∧
Aψ
35 / 38
Conversion to CNF: Tseitin encoding by example
φ = (A ∧ B) ∨ C
A B C
∧
∨ψ
ρ
(Aρ ↔ (A ∧ B)) ∧ (Aρ → (A ∧ B)) ∧
(Aρ ← (A ∧ B)) ∧
(Aψ ↔ (Aρ ∨ C)) ∧ ≡ (Aψ → (Aρ ∨ C)) ∧
(Aψ ← (Aρ ∨ C)) ∧
Aψ Aψ
35 / 38
Conversion to CNF: Tseitin encoding by example
φ = (A ∧ B) ∨ C
A B C
∧
∨ψ
ρ
(Aρ ↔ (A ∧ B)) ∧ (Aρ → (A ∧ B)) ∧ {¬Aρ, A}, {¬Aρ, B},
(Aρ ← (A ∧ B)) ∧ {¬A, ¬B, Aρ},
(Aψ ↔ (Aρ ∨ C)) ∧ ≡ (Aψ → (Aρ ∨ C)) ∧ ≡ {¬Aψ, Aρ, C},
(Aψ ← (Aρ ∨ C)) ∧ {¬Aρ, Aψ}, {¬C, Aψ},
Aψ Aψ {Aψ}
35 / 38
Conversion to CNF: Tseitin encoding
1. Create a new Tseitin variable Aψ for each subformula of φ.
2. Add unit clause {Aφ}.
3. Define semantics of the new Tseitin variables Aψ:
ψ definition of Aψ added clauses
ρ1 ∨ ρ2 Aψ → (Aρ1
∨ Aρ2
) {¬Aψ, Aρ1
, Aρ2
}
Aψ ← (Aρ1 ∨ Aρ2 ) {¬Aρ1 , Aψ}, {¬Aρ2 , Aψ}
ρ1 ∧ ρ2 Aψ → (Aρ1
∧ Aρ2
) {¬Aψ, Aρ1
}, {¬Aψ, Aρ2
}
Aψ ← (Aρ1
∧ Aρ2
) {¬Aρ1
, ¬Aρ2
, Aψ}
¬ρ Aψ → ¬Aρ {¬Aψ, ¬Aρ}
Aψ ← ¬Aρ {Aρ, Aψ}
ρ1 ↔ ρ2 Aψ → (Aρ1
↔ Aρ2
) {¬Aψ, ¬Aρ1
, Aρ2
}, {¬Aψ, Aρ1
, ¬Aρ2
}
Aψ ← (Aρ1
↔ Aρ2
) {¬Aρ1
, ¬Aρ2
, Aψ}, {Aρ1
, Aρ2
, Aψ}
36 / 38
Conversion to CNF: Tseitin encoding
Tseitin encoding
• often used in practice
• also works for DAG representation of formulas → one Tseitin variable for
each node in the DAG
• transforming to increase shared subexpression helps (B ∧ A) (A ∧ B)
• additional preprocessing helps: (A ∨ (B ∨ C)) (A ∨ B ∨ C) and then encode
Aφ ↔ (A ∨ B ∨ C) as one Tseitin variable and four implications
• some of the clauses are not needed (Plaisted-Greenbaum)
37 / 38
Next time
Classical SAT algorithms
• propositional resolution
• Davis-Putnam-Logemann-Loveland algorithm (DPLL)
38 / 38