Boolean Satisfiability notes
Home
Table of Contents
These are my notes from Donald Knuth's The Art of Computer Programming: Satisfiability, Volume 4, Fascicle 6.
1. Introduction
A efficient algorithm for SAT would involve deciding a CNF on \(N\) variables in \(N^{O(1)}\) steps. It is possible (and D.K. believes so) that SAT is in \(P\) but the algorithm is "unknowable", meaning we might get an existence proof of such an algorithm.
D.K. defines a literal to be either a variable or its complement. Two literals are distinct if \(l_1 \neq l_2\). They are strictly distinct if \(|l_1| \neq |l_2|\).
1.1. SAT is equivalent to a covering problem
def Tₙ (n : ℕ) : CNF := {{1, ¬1}, {2, ¬ 2}, ..., {n, ¬n}}
variable (S : Cnf)
def is_sat S : Prop :=
let n := number_of_variables S in
∃ L : set (Literals),
-- (1) L has size n
L.size = n
-- (2) every clause had a literal that is in L.
∧ ∀ (c : Clause) ∈ S, ∃ l ∈ L, l ∈ c