Satisfiability (SAT) in Propositional Logic: Principles, Solvers, Complexity, and Applications

Foundations of Satisfiability and Formula Classification

Definition of Satisfiability (SAT):
- A propositional formula is satisfiable if there exists at least one world (truth assignment to its propositional variables) that makes the formula true ( $1$ ).
- The central semantic question of SAT is: "Is there a world where the formula is true?"
Taxonomy of Propositional Formulas:
- Tautology: A formula that evaluates to true ( $1$ ) across every possible row of its truth table (e.g., $A \lor \neg A$ ).
- Contradiction: A formula that evaluates to false ( $0$ ) across every row of its truth table (e.g., $A \land \neg A$ ).
- Satisfiable: A formula that evaluates to true ( $1$ ) in at least one row of its truth table (e.g., $A \land B$ ).
- Unsatisfiable: A formula that is a contradiction; no conceivable world satisfies it.
Relationship Between Classes:
- Every tautology is satisfiable because it possesses at least one satisfying world (in fact, all worlds satisfy it).
- Not every satisfiable formula is a tautology: for instance, $A \land B$ is satisfiable under the assignment $A = 1, B = 1$ , but evaluates to false whenever $A = 0$ or $B = 0$ .
Truth Table Classification of Propositional Formulas:

Truth table classifying tautology, contradiction, and satisfiable formulas

Formula 1 — $(A \rightarrow B) \lor (B \rightarrow A)$ :
- Evaluates to $1$ for all assignments ( $(0,0) \mapsto 1$ , $(0,1) \mapsto 1$ , $(1,0) \mapsto 1$ , $(1,1) \mapsto 1$ ).
- Classified as a tautology.
Formula 2 — $A \land \neg A$ :
- Evaluates to $0$ across all assignments ( $(0,0) \mapsto 0$ , $(0,1) \mapsto 0$ , $(1,0) \mapsto 0$ , $(1,1) \mapsto 0$ ).
- Classified as a contradiction (unsatisfiable).
Formula 3 — $(A \lor B) \land (\neg A \lor \neg B)$ :
- Evaluates to $0$ for $(0,0)$ , $1$ for $(0,1)$ , $1$ for $(1,0)$ , and $0$ for $(1,1)$ .
- Classified as satisfiable.
- Represents exclusive disjunction ( $\text{XOR}$ , asserting that exactly one of $A$ and $B$ is true).

Clause-Based Elimination and Unsatisfiability

Clause Semantics in Conjunctive Normal Form (CNF):
- A clause is defined as a disjunction (an "or") of literals, where a literal is an atomic variable or its negation.
- A disjunctive clause is false if and only if every literal within it evaluates to false simultaneously.
- Consequently, each individual clause rules out ("kills") exactly the truth assignments that falsify all of its constituent literals.
Elimination of Worlds in $(A \lor B) \land (\neg A \lor \neg B) \land (A \lor \neg B) \land (\neg A \lor B)$ :

Truth table showing clauses eliminating all possible truth assignments

The assignment $A = 0, B = 0$ is eliminated by the clause $A \lor B$ .
The assignment $A = 0, B = 1$ is eliminated by the clause $A \lor \neg B$ .
The assignment $A = 1, B = 0$ is eliminated by the clause $\neg A \lor B$ .
The assignment $A = 1, B = 1$ is eliminated by the clause $\neg A \lor \neg B$ .
Because every candidate world is eliminated by at least one conjunct, no world survives. The full conjunction is unsatisfiable.

Reductions to Satisfiability Solvers

Unification of Logical Inquiries via SAT:
- An automated decision procedure for satisfiability (a SAT solver) solves three fundamental questions of formal logic by reducing them to unsatisfiability checks:
- Tautology Checking: A formula $F$ is a tautology if and only if $\neg F$ is unsatisfiable.
- Logical Equivalence: Two formulas $F$ and $G$ are equivalent ( $F \equiv G$ ) if and only if $\neg (F \leftrightarrow G)$ is unsatisfiable.
- Argument Validity (Entailment): A set of premises $P_1, P_2, \dots, P_k$ logically entails a conclusion $C$ if and only if the conjunction $P_1 \land P_2 \land \dots \land P_k \land \neg C$ is unsatisfiable.
- The Counterexample Principle: All logical verification tasks search for a counterexample. If no counterexample exists within any possible valuation, the underlying assertion holds across all worlds.
Asymmetry of Verification (Certificates vs. Proofs):
- Satisfiable Output: When a formula is satisfiable, the solver produces a single satisfying assignment (e.g., $A = 1, B = 0$ ). This assignment serves as a concrete certificate that can be verified in linear time ( $\mathcal{O}(n)$ ) in seconds.
- Unsatisfiable Output: A solver cannot justify unsatisfiability merely by failing to find an assignment. Exhaustive truth-table inspection across $2^n$ rows is computationally infeasible for large $n$ .
- Modern SAT solvers construct a formal mathematical proof of unsatisfiability (refutation proof) during execution. An independent, small, mathematically verified program then checks this proof.

Declarative Programming and Real-World SAT Applications

Imperative vs. Declarative Programming Paradigms:
- Imperative Programming: The developer explicitly encodes execution steps, state mutations, loops, and conditional branching (e.g., Python, Java, C).
- Declarative Programming: The developer models the formal constraints defining what constitutes a valid solution. An external solver executes the combinatorial search (e.g., SQL, Prolog, SAT solvers, SMT solvers).
- In SAT modeling, specifications are encoded as propositional logic formulas; SAT solvers perform the underlying search.
Industrial Application 1: Package Dependency Resolution ("Dependency Hell"):
- Scenario: In June 2024, NumPy 2.0 was released. Several Python libraries required NumPy 1, whereas others required NumPy 2. An application must install a plotting library and a machine-learning library simultaneously without version conflicts.
- Variable Declarations:
- $A$ : Install the main application
- $P$ : Install the plotting library
- $M$ : Install the machine-learning library
- $N_1, N_2$ : NumPy 1, NumPy 2
- Constraint Formula:
- $A \land (A \rightarrow P) \land (A \rightarrow M) \land (P \rightarrow N_1) \land (M \rightarrow N_2) \land \neg (N_1 \land N_2)$
- Deterministic Unit Propagation:

Unit propagation forcing steps in dependency resolution

- Step 1:  $A = 1$  is forced by the unit conjunct  $A$ .
- Step 2:  $A \rightarrow P$  and  $A \rightarrow M$  force  $P = 1$  and  $M = 1$ .
- Step 3:  $P \rightarrow N_1$  and  $M \rightarrow N_2$  force  $N_1 = 1$  and  $N_2 = 1$ .
- Step 4: A contradiction occurs with  $\neg (N_1 \land N_2)$ , which forbids both being true.
- The system is unsatisfiable: the application cannot be installed under these dependencies.
- This logical chain of forced inferences constitutes a four-step proof, replacing an exhaustive search across  $2^5 = 32$  rows.

Python SymPy Implementation: ```python from sympy import symbols from sympy.logic.inference import satisfiable
A, P, M, N1, N2 = symbols('A P M N1 N2') # >> denotes ->, ~ denotes not rules = A & (A >> P) & (A >> M) & (P >> N1) & (M >> N2) & ~(N1 & N2) print(satisfiable(rules)) # False
Version 2 of the plotting library (P2) works with NumPy 2
P1, P2 = symbols('P1 P2') rules2 = ( A & (A >> (P1 | P2)) & (A >> M) & (P1 >> N1) & (P2 >> N2) & (M >> N2) & ~(N1 & N2) ) model = satisfiable(rules2) # returns a satisfying world print(sorted(str(v) for v, val in model.items() if val))
Output: ['A', 'M', 'N2', 'P2'] (indicates installing exactly these packages)
```
Package Managers Employing SAT Engines:
- conda and mamba (Python data science ecosystem) rely on the SAT solver libsolv.
- Linux package managers DNF (Fedora) and zypper (openSUSE) use libsolv.
- Composer (PHP) contains an integrated SAT solver.
- uv, Poetry, and Dart's pub use the PubGrub algorithm, a SAT-style constraint solver.
- Package dependency resolution is formally NP-complete, identical in computational complexity to SAT.
- Industrial Application 2: Cloud Storage Security and Access Control:
Scenario: A cloud storage bucket evaluates requests via the policy: $(R \land N) \lor S \lor P$ .
- $R$ : The request is a read operation ( $\neg R$ indicates a write operation)
- $N$ : The request originates from the company network
- $S$ : The request is digitally signed by a member of staff
- $P$ : The target file is tagged as public
Security Invariant: Only authorized staff members may write to files.
Verification Query: Check satisfiability of:
- $((R \land N) \lor S \lor P) \land \neg R \land \neg S$
Vulnerability Identification: The formula is satisfiable under the assignment $P = 1, R = 0, S = 0$ . This proves that any unauthorized stranger can overwrite any file tagged as public.
Policy Remediation: Replace the open clause $P$ with $P \land R$ (public status permits read operations only). The updated verification formula $((R \land N) \lor S \lor (P \land R)) \land \neg R \land \neg S$ becomes unsatisfiable, mathematically guaranteeing that no unsigned write request can proceed.
Industrial Scale:
- Amazon Web Services (AWS) translates access policies into logic, querying SMT solvers (Satisfiability Modulo Theories: SAT combined with theory solvers for arithmetic, strings, bitvectors) approximately $1 \times 10^9$ ( $1\text{ billion}$ ) times daily (recorded in 2022).
- Microsoft's SAGE tool applied SMT solvers for automated test-input generation (symbolic execution/fuzzing), uncovering one-third of all file-fuzzing security bugs during the development of Windows 7.
- Security verification at Meta / Facebook's London headquarters relies on SAT-based program analysis.
- Industrial Application 3: Automotive Product Configuration:
Context: Around 2001, DaimlerChrysler deployed SAT solvers to validate configuration rules for Mercedes-Benz passenger vehicles.
Complexity: The C-class line contained over $1\,000$ optional features. On average, more than $30\,000$ custom vehicles were manufactured before a single configuration was ever repeated.
Sample Configuration Rules:
- $S \rightarrow W$ : Sports package requires 19-inch wheels
- $T \rightarrow \neg W$ : Winter tyres do not fit 19-inch wheels
- $X \rightarrow (S \land T)$ : Alpine edition bundle includes both the sports package and winter tyres
Dead Option Detection: Can a customer order the Alpine edition ( $X = 1$ )?
- Assigning $X = 1$ forces $S = 1$ and $T = 1$ .
- In turn, $S = 1$ forces $W = 1$ , whereas $T = 1$ forces $\neg W = 1$ ( $W = 0$ ).
- This generates a direct clash ( $W \land \neg W$ ). The specification is unsatisfiable with $X$ .
- Option $X$ is a dead option caused by invalid product data, detected automatically without prototype testing.
- Industrial Application 4: Formal Hardware Equivalence Checking:
Chip designers regularly replace logic gate networks with smaller, lower-power equivalents.
Circuit 1: Original design $F = (A \land B) \lor (A \land C)$ ( $3$ gates).
Circuit 2: Optimized design $G = A \land (B \lor C)$ ( $2$ gates).
- Verification condition: Evaluate satisfiability of $\neg (F \leftrightarrow G)$ .
- Result: Unsatisfiable. The circuits produce identical outputs across all possible input states.
Circuit 3: Flawed optimization $G' = (A \land B) \lor C$ ( $2$ gates).
- Verification condition: Evaluate satisfiability of $\neg (F \leftrightarrow G')$ .
- Result: Satisfiable. A counterexample is found at $A = 0, B = 1, C = 1$ , where $F = 0$ but $G' = 1$ .
Economic Impact: The Intel Pentium floating-point division (FDIV) bug in 1994 incurred a replacement cost of $\$475\text{ million}$ . Following this incident, formal equivalence verification via SAT solvers became standard practice in microprocessor design.
- Industrial Application 5: Combinatorial Modeling (Sudoku):
Variable Encoding: Let propositional variable $x_{r,c,d}$ represent "row $r$ , column $c$ contains digit $d$ ".
Variable Count: For a $9 \times 9$ grid with $9$ digits, there are $9 \times 9 \times 9 = 729$ variables.
Clause Encodings: Approximately $10\,000$ clauses encode the rules (every cell contains at least one digit; no cell contains multiple digits; no digit appears twice in any row, column, or $3 \times 3$ box).
Computational Contrast: An exhaustive truth table contains $2^{729} \approx 10^{219}$ rows. A modern SAT solver completes the search in a few milliseconds.

Computational Complexity and Solver Architecture

The Cook-Levin Theorem and NP-Completeness:
- Formulated independently by Stephen Cook (1971) and Leonid Levin (1973).
- Theorem: Any computational problem whose proposed solutions can be verified in polynomial time can be reduced in polynomial time to SAT.
- SAT was the first problem proven to be NP-complete.
- An efficient (polynomial-time) SAT solver would yield polynomial-time solutions for scheduling, timetabling, package dependency management, hardware verification, and route planning.
- The question of whether a polynomial-time algorithm exists for all SAT instances is the P versus NP problem (a Clay Mathematics Institute Millennium Prize problem with a $\$1\text{ million}$ reward).
Historical Evolution of SAT Solvers:
- 1962 — DPLL (Davis-Putnam-Logemann-Loveland): Recursive backtracking search combined with unit propagation.
- 1996 — GRASP: Introduced Conflict-Driven Clause Learning (CDCL), allowing solvers to derive and store lemmas from contradictory search branches.
- 2001 — Chaff: Introduced the two-watched-literals data structure, accelerating unit propagation by $10\times$ to $100\times$ .
- 2003 — MiniSat: A compact, open-source CDCL solver architecture that became the standard research baseline.
- 2020 — Kissat: A state-of-the-art pure CDCL solver implemented in C.
- 2025 — AI-Driven Solvers: AI agents autonomously refactor and optimize low-level solver heuristics.
- The SAT Competition: An annual competitive benchmark comparing solver implementations across hundreds of industrial and combinatorial instances. In the 2025 competition, solvers were evaluated on $400$ benchmark problems, won by AE-Kissat-MAB.
The Conflict-Driven Clause Learning (CDCL) Core Loop:
- Guess (Decide): The solver heuristically chooses an unassigned variable and assigns it a tentative Boolean truth value ( $0$ or $1$ ).
- Propagate (Unit Propagation): If an unresolved clause has all of its literals assigned to false except one, the remaining unassigned literal is forced to true. Propagation repeats until no further units exist or a conflict occurs.
- Conflict Analysis: When a clause has all its literals evaluate to false, an assignment clash is detected.
- Learn: The solver analyzes the conflict graph to deduce a new learned clause that captures the root cause of the clash. Adding this clause prunes the search space, preventing the solver from ever re-entering the conflicting state.
- Back up (Non-chronological Backjumping): The solver backtracks to the decision level determined by the learned clause, bypassing redundant subtrees.

SAT in Mathematics and Theoretical AI

The Boolean Pythagorean Triples Problem:
- Conjecture: Can the set of positive integers $\{1, 2, \dots, n\}$ be partitioned into two sets (colored red and blue) such that no subset contains a monochromatic Pythagorean triple satisfying $a^2 + b^2 = c^2$ ?
- Example Triple: $3^2 + 4^2 = 5^2$ ( $9 + 16 = 25$ ).
- Encoding into SAT:
- Assign a Boolean variable $x_i$ denoting "integer $i$ is colored red".
- For each Pythagorean triple $(a, b, c)$ , generate two clauses preventing all three from being colored red or all three from being colored blue: $(x_a \lor x_b \lor x_c) \land (\neg x_a \lor \neg x_b \lor \neg x_c)$
- Resolution (Heule, Kullmann, and Marek, 2016):
- A valid two-coloring exists for all integers up to $n = 7824$ .
- The problem becomes unsatisfiable at $n = 7825$ .
- The computation required $2\text{ days}$ running across $800$ CPU cores, generating a $200\text{ terabyte}$ unsatisfiability proof certificate.
Additional Mathematical Theorems Settled by SAT Solvers:
- Schur Number Five (2017): The set of integers $\{1, \dots, 160\}$ can be partitioned into five sum-free subsets (where no subset contains $a, b, c$ such that $a + b = c$ ). Partitioning $\{1, \dots, 161\}$ is mathematically impossible.
- Keller's Conjecture (2020): Settled the final open case in dimension $7$ after remaining unsolved for $90\text{ years}$ .
- The Empty Hexagon Problem (2024): Proved that every planar set of $30$ points in general position (no three points collinear) contains an empty convex hexagon (a convex hexagon containing no other points of the set in its interior). Proved that $29$ points do not guarantee an empty hexagon. The resulting SAT proof was certified by a formally verified proof checker.
The Intersection of SAT and Artificial Intelligence:
- AI Improving SAT Solvers: In 2025, NVIDIA researchers deployed multi-agent systems of large language models to iteratively rewrite and optimize solver source code (SATLUTION). The evolved solvers solved $347$ out of the $400$ SAT Competition 2025 benchmark instances, surpassing the competition winner AE-Kissat-MAB (which solved $334$ ).
- SAT Verifying AI Systems (Marijn Heule's Architecture):
- Neural networks excel at heuristic guessing and translation, but suffer from hallucinations.
- In Heule's verification architecture, a language model translates a complex natural-language mathematical problem into formal logic; a SAT solver performs the exhaustive combinatorial search; and an independent proof checker formally certifies the refutation proof.
- "Neural networks are good at guessing. Logic is how we check the guesses."

The Exponential Limits of Truth Tables

The Combinatorial Explosion of Truth Tables:
- A truth table over $n$ propositional variables requires evaluating $2^n$ rows.
- At an evaluation throughput of $10^9$ ( $1\text{ billion}$ ) rows per second, execution time scales exponentially:
- $10$ variables: $2^{10} = 1\,024$ rows; execution time: $1\,\mu\text{s}$
- $20$ variables: $2^{20} = 1\,048\,576$ rows; execution time: $1\,\text{ms}$
- $50$ variables: $2^{50} \approx 1.1 \times 10^{15}$ rows; execution time: $13\,\text{days}$
- $100$ variables: $2^{100} \approx 1.3 \times 10^{30}$ rows; execution time: $40\times 10^{12}\,\text{years}$ ( $40\text{ trillion years}$ , approximately $3\,000$ times the estimated age of the universe)
- $729$ variables (Sudoku): $2^{729} \approx 2.8 \times 10^{219}$ rows; computationally intractable
- $1\,000\,000$ variables (modern industrial SAT problems): $2^{1000000}$ , a value possessing $301\,030$ decimal digits
Deductive Proof vs. Exhaustive Enumeration:
- Consider a chained implication over $100$ variables: $A_1 \rightarrow (A_2 \rightarrow (A_3 \rightarrow \dots \rightarrow (A_{100} \rightarrow A_1)\dots))$
- Evaluating this formula via a truth table requires constructing $2^{100}$ rows.
- Deductive Refutation Proof:
- Assume there exists an assignment that makes the formula false ( $0$ ).
- Recall that an implication $X \rightarrow Y$ evaluates to false if and only if $X = 1$ and $Y = 0$ .
- For the outer implication to be false, antecedent $A_1$ must be true ( $A_1 = 1$ ), and consequent $A_2 \rightarrow (A_3 \rightarrow \dots)$ must be false ( $0$ ).
- For $A_2 \rightarrow (A_3 \rightarrow \dots)$ to be false, $A_2 = 1$ and the inner subformula must be false.
- Continuing this chain of inferences, every variable $A_1, A_2, \dots, A_{100}$ is forced to evaluate to true ( $1$ ).
- Reaching the final implication forces $A_{100} = 1$ and the terminal consequent $A_1 = 0$ .
- This derives an immediate contradiction: $A_1 = 1$ (from step 1) and $A_1 = 0$ .
- Because no assignment can make the formula false, it is a tautology.
- This syntactic proof requires a few lines of logical derivation (and corresponds to a 201-line natural deduction box proof) rather than $2^{100}$ truth-table rows.
Semantic Limitations: Two-Valued vs. Three-Valued Logic (3VL):
- Classical propositional truth tables operate strictly under bivalence (every statement is either true or false).
- Database systems (such as SQL) implement a three-valued logic containing NULL, representing an unknown truth value.
- Consider the query: sql SELECT name FROM students WHERE grade >= 40 OR grade < 40;     
- In classical logic, $P \lor \neg P$ is a tautology, so this query would be expected to return every record in the table.
- In SQL 3VL, if grade is NULL, then grade >= 40 evaluates to unknown, and grade < 40 evaluates to unknown.
- The expression unknown OR unknown evaluates to unknown.
- Rows where the WHERE condition evaluates to unknown are filtered out. Consequently, students with NULL grades are omitted, demonstrating that classical two-valued truth tables cannot capture SQL query semantics.

Exercises and Model Solutions

Exercise 1:
- Problem: Determine whether the following formula is satisfiable: $(A \rightarrow B) \land (B \rightarrow C) \land A \land \neg C$
- Model Solution: The formula is unsatisfiable.
- The unit conjunct $A$ forces $A = 1$ .
- Applying $A = 1$ to $A \rightarrow B$ forces $B = 1$ .
- Applying $B = 1$ to $B \rightarrow C$ forces $C = 1$ .
- This directly contradicts the conjunct $\neg C$ , which forces $C = 0$ .
Exercise 2:
- Problem: Show that $(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)$ is a tautology by proving that its negation is unsatisfiable.
- Model Solution:
- The negation of an implication $X \rightarrow Y$ is logically equivalent to $X \land \neg Y$ .
- Therefore, $\neg ((A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A))$ is equivalent to: $(A \rightarrow B) \land \neg (\neg B \rightarrow \neg A)$
- Negating the inner implication gives $\neg B \land \neg (\neg A)$ , which simplifies to $\neg B \land A$ .
- Combining these yields: $(A \rightarrow B) \land \neg B \land A$
- From $A = 1$ and $A \rightarrow B$ , unit propagation forces $B = 1$ .
- This directly contradicts $\neg B = 1$ ( $B = 0$ ).
- Because the negation is unsatisfiable, the original implication is a tautology.
Exercise 3:
- Problem: Express the constraints preventing the Pythagorean triple $6, 8, 10$ ( $6^2 + 8^2 = 10^2$ ) from being monochromatic as two CNF clauses, using variables $x_i$ to denote that integer $i$ is colored red.
- Model Solution:
- $(x_6 \lor x_8 \lor x_{10}) \land (\neg x_6 \lor \neg x_8 \lor \neg x_{10})$
- The first clause requires at least one number to be red (preventing all three from being blue).
- The second clause requires at least one number to not be red (preventing all three from being red).
Exercise 4:
- Problem: Three examinations— $L$ , $P$ , and $M$ —must each be scheduled into either slot 1 or slot 2. Exams $L$ and $P$ share students, and exams $P$ and $M$ share students (so shared pairs cannot be scheduled in the same time slot). Formulate this problem in propositional logic using variables $L_1, L_2, P_1, P_2, M_1, M_2$ , and determine whether the formula is satisfiable.
- Model Solution:
- Constraint Formulation:
  - Each exam must be assigned to at least one slot: $(L_1 \lor L_2) \land (P_1 \lor P_2) \land (M_1 \lor M_2)$
  - Exams sharing students cannot share slot 1 or slot 2: $\neg (L_1 \land P_1) \land \neg (L_2 \land P_2) \land \neg (P_1 \land M_1) \land \neg (P_2 \land M_2)$
  - The complete formula is the conjunction of these clauses: $(L_1 \lor L_2) \land (P_1 \lor P_2) \land (M_1 \lor M_2) \land \neg (L_1 \land P_1) \land \neg (L_2 \land P_2) \land \neg (P_1 \land M_1) \land \neg (P_2 \land M_2)$
- Satisfiability: The formula is satisfiable.
  - A valid satisfying assignment is $L_1 = 1, P_2 = 1, M_1 = 1$ (with $L_2 = 0, P_1 = 0, M_2 = 0$ ).
  - This schedules exams $L$ and $M$ into slot 1, and exam $P$ into slot 2, satisfying all conflict constraints.

Satisfiability (SAT) in Propositional Logic: Principles, Solvers, Complexity, and Applications

Foundations of Satisfiability and Formula Classification

Clause-Based Elimination and Unsatisfiability

Reductions to Satisfiability Solvers

Declarative Programming and Real-World SAT Applications

Version 2 of the plotting library (P2) works with NumPy 2

Output: ['A', 'M', 'N2', 'P2'] (indicates installing exactly these packages)

Computational Complexity and Solver Architecture

SAT in Mathematics and Theoretical AI

The Exponential Limits of Truth Tables

Exercises and Model Solutions