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