# 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