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

Author: Vaibhav Karve

Created: 2024-02-04 Sun 21:01

Validate