Introduction to Propositional Satisfiability
IA085: Satisfiability and Automated Reasoning
Martin Jonáš
FI MUNI, Spring 2025
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 May 7)
• seminar every other week
• project (write your own small SAT solver) – mandatory
Exam
• oral exam
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, 2025
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 φ (i.e., Atoms(φ) ⊆ dom(µ)) 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 ψ (i.e., (Atoms(φ) ∪ Atoms(ψ)) ⊆ dom(µ))
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 are {}? and {∅}?
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.
23 / 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
Validity
• a φ is valid if every total assignment for φ is its model
• φ is valid ⇔ ¬φ is not satisfiable
Entailment
• φ |= ψ ⇔ (φ → ψ) 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