SAT: Semantic Layer

This file contains the mathematical definition of Boolean satisfiability. No Turing machines are used here. Everything is pure recursion on inductive types; a reader can audit these definitions in a few minutes and check that they really capture "α satisfies φ".

All later claims about the SAT verifier are stated against the predicates defined here. If this file is wrong, nothing downstream rescues us.

Definitions

• Lit — a literal (sign, var) where var : Nat is a variable index and sign : Bool says whether the literal is positive.
• Clause — a list of literals (disjunction).
• CNF — a list of clauses (conjunction).
• Assignment — a List Bool giving the value of each variable.
• Lit.eval — α[ℓ.var] = ℓ.sign (out-of-range reads as false).
• Clause.eval — disjunction over literals.
• CNF.eval — conjunction over clauses.
• CNF.Satisfiable — some assignment makes CNF.eval true.

Out-of-range convention

A variable index i ≥ α.length is treated as assigned to false. This is standard in SAT textbooks ("unassigned variables default to 0") and makes the language closed under padding: a short satisfying assignment always exists, equal to a prefix of any longer one. This is essential for polynomial balance in the NP reduction.

structure Complexity.SAT.Lit : Type

A literal: sign = true means the positive literal x_var; sign = false means ¬x_var.

• sign : Bool

  Polarity of the literal: true for x_var, false for ¬x_var.

• var : ℕ

  Index of the variable this literal mentions.

def Complexity.SAT.instDecidableEqLit.decEq (x✝ x✝¹ : Lit) : Decidable (x✝ = x✝¹)

Equations

• Complexity.SAT.instDecidableEqLit.decEq { sign := a, var := a_1 } { sign := b, var := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Complexity.SAT.instDecidableEqLit : DecidableEq Lit

Equations

• Complexity.SAT.instDecidableEqLit = Complexity.SAT.instDecidableEqLit.decEq

@[reducible, inline]

abbrev Complexity.SAT.Clause : Type

A clause is a disjunction of literals. The empty clause is unsatisfiable (an empty disjunction is false).

Equations

• Complexity.SAT.Clause = List Complexity.SAT.Lit

@[reducible, inline]

abbrev Complexity.SAT.CNF : Type

A CNF formula is a conjunction of clauses. The empty CNF is satisfiable (an empty conjunction is true).

Equations

• Complexity.SAT.CNF = List Complexity.SAT.Clause

@[reducible, inline]

abbrev Complexity.SAT.Assignment : Type

An assignment is a bit-string. Position i holds the value of variable i. Indices past the end read as false.

Equations

• Complexity.SAT.Assignment = List Bool

@[inline]

def Complexity.SAT.Assignment.get (α : Assignment) (i : ℕ) : Bool

Value of variable i under assignment α, with out-of-range = false.

Equations

• α.get i = α[i]?.getD false

@[inline]

def Complexity.SAT.Lit.eval (α : Assignment) (ℓ : Lit) : Bool

ℓ = (s, v) is satisfied by α iff α.get v = s.

Equations

• Complexity.SAT.Lit.eval α ℓ = (α.get ℓ.var == ℓ.sign)

@[inline]

def Complexity.SAT.Clause.eval (α : Assignment) (c : Clause) : Bool

A clause is satisfied iff at least one literal is.

Equations

• Complexity.SAT.Clause.eval α c = List.any c (Complexity.SAT.Lit.eval α)

@[inline]

def Complexity.SAT.CNF.eval (α : Assignment) (φ : CNF) : Bool

A CNF is satisfied iff every clause is.

Equations

• Complexity.SAT.CNF.eval α φ = List.all φ (Complexity.SAT.Clause.eval α)

def Complexity.SAT.CNF.Satisfiable (φ : CNF) : Prop

φ is satisfiable if some assignment makes CNF.eval true.

Equations

• φ.Satisfiable = ∃ (α : Complexity.SAT.Assignment), Complexity.SAT.CNF.eval α φ = true

@[simp]

theorem Complexity.SAT.CNF.eval_nil (α : Assignment) : eval α [] = true

The empty CNF evaluates to true (empty conjunction).

@[simp]

theorem Complexity.SAT.CNF.eval_cons (α : Assignment) (c : Clause) (φ : CNF) : eval α (c :: φ) = (Clause.eval α c && eval α φ)

Evaluating c :: φ is the conjunction of evaluating c and evaluating φ.

theorem Complexity.SAT.CNF.satisfiable_nil : Satisfiable []

The empty formula is trivially satisfiable.

theorem Complexity.SAT.CNF.not_satisfiable_empty_clause : ¬Satisfiable [[]]

The formula [[]] (one empty clause) is unsatisfiable.

@[inline]

def Complexity.SAT.Lit.maxVar (ℓ : Lit) : ℕ

Largest variable index appearing in a literal (just ℓ.var).

Equations

• ℓ.maxVar = ℓ.var

def Complexity.SAT.Clause.maxVar : Clause → ℕ

Largest variable index in a clause (0 if empty).

Equations

• Complexity.SAT.Clause.maxVar [] = 0
• Complexity.SAT.Clause.maxVar (ℓ :: ℓs) = max ℓ.var (Complexity.SAT.Clause.maxVar ℓs)

@[simp]

theorem Complexity.SAT.Clause.maxVar_nil : maxVar [] = 0

The empty clause has maxVar = 0.

@[simp]

theorem Complexity.SAT.Clause.maxVar_cons (ℓ : Lit) (ℓs : Clause) : maxVar (ℓ :: ℓs) = max ℓ.var ℓs.maxVar

maxVar of ℓ :: ℓs is the max of ℓ.var and maxVar ℓs.

theorem Complexity.SAT.Clause.var_le_maxVar {ℓ : Lit} {c : Clause} (hℓ : ℓ ∈ c) : ℓ.var ≤ c.maxVar

Every literal's var in a clause is at most c.maxVar.

def Complexity.SAT.CNF.maxVar : CNF → ℕ

Largest variable index in a CNF (0 if empty).

Equations

• Complexity.SAT.CNF.maxVar [] = 0
• Complexity.SAT.CNF.maxVar (c :: cs) = max c.maxVar (Complexity.SAT.CNF.maxVar cs)

@[simp]

theorem Complexity.SAT.CNF.maxVar_nil : maxVar [] = 0

The empty CNF has maxVar = 0.

@[simp]

theorem Complexity.SAT.CNF.maxVar_cons (c : Clause) (cs : CNF) : maxVar (c :: cs) = max c.maxVar cs.maxVar

maxVar of c :: cs is the max of c.maxVar and maxVar cs.

theorem Complexity.SAT.CNF.clause_maxVar_le_maxVar {c : Clause} {φ : CNF} (hc : c ∈ φ) : c.maxVar ≤ φ.maxVar

Every clause's maxVar is at most φ.maxVar.

theorem Complexity.SAT.Assignment.get_append_left (α β : Assignment) (i : ℕ) (h : i < List.length α) : (α ++ β).get i = α.get i

Assignment.get on α ++ β agrees with α at in-range indices.

theorem Complexity.SAT.Lit.eval_append_of_lt (α β : Assignment) (ℓ : Lit) (h : ℓ.var < List.length α) : eval (α ++ β) ℓ = eval α ℓ

Appending to an assignment doesn't change Lit.eval for in-range literals.

theorem Complexity.SAT.Assignment.get_take (α : Assignment) (i k : ℕ) (hi : i < k) : get (List.take k α) i = α.get i

α.get i is preserved by truncating to any length k > i.

theorem Complexity.SAT.Lit.eval_take (α : Assignment) (ℓ : Lit) (k : ℕ) (hk : ℓ.var < k) : eval (List.take k α) ℓ = eval α ℓ

Lit.eval is invariant under truncation when the literal's var is in range.

theorem Complexity.SAT.Clause.eval_take (α : Assignment) (c : Clause) (k : ℕ) (hk : c.maxVar < k) : eval (List.take k α) c = eval α c

Clause.eval is preserved by truncation of α to length above c.maxVar.

theorem Complexity.SAT.CNF.eval_take (α : Assignment) (φ : CNF) (k : ℕ) (hk : φ.maxVar < k) : eval (List.take k α) φ = eval α φ

CNF.eval is preserved by truncation of α to length above φ.maxVar.

theorem Complexity.SAT.CNF.satisfiable_iff_short_witness (φ : CNF) : φ.Satisfiable ↔ ∃ (α : Assignment), List.length α ≤ φ.maxVar + 1 ∧ eval α φ = true

PolyBalanced witness lemma. A satisfiable formula has a satisfying assignment of length at most φ.maxVar + 1.

theorem Complexity.SAT.Lit.eval_eq_of_agree (α β : Assignment) (ℓ : Lit) (h : α.get ℓ.var = β.get ℓ.var) : eval α ℓ = eval β ℓ

If two assignments give the same value at every index (via Assignment.get), they produce the same literal evaluation.

theorem Complexity.SAT.Clause.eval_eq_of_agree (α β : Assignment) (c : Clause) (h : ∀ (i : ℕ), α.get i = β.get i) : eval α c = eval β c

Pointwise agreement of Assignment.get implies equal Clause.eval.

theorem Complexity.SAT.CNF.eval_eq_of_agree (α β : Assignment) (φ : CNF) (h : ∀ (i : ℕ), α.get i = β.get i) : eval α φ = eval β φ

Pointwise agreement of Assignment.get implies equal CNF.eval.

theorem Complexity.SAT.Assignment.get_append_replicate_false (α : Assignment) (k i : ℕ) : (α ++ List.replicate k false).get i = α.get i

Appending falses doesn't change Assignment.get: out-of-range positions default to false anyway.

theorem Complexity.SAT.CNF.eval_append_replicate_false (α : Assignment) (k : ℕ) (φ : CNF) : eval (α ++ List.replicate k false) φ = eval α φ

Padding an assignment with falses doesn't change CNF.eval.

@[implicit_reducible]

instance Complexity.SAT.CNF.decidableSatisfiable (φ : CNF) : Decidable φ.Satisfiable

Brute-force decidability. Satisfiability is decidable by enumerating all 2^(φ.maxVar + 1) assignments of length φ.maxVar + 1. Not poly-time, but establishes that the semantic layer is concretely computable and enables decide on small instances.

Equations

• φ.decidableSatisfiable = decidable_of_iff (∃ (f : Fin (φ.maxVar + 1) → Bool), Complexity.SAT.CNF.eval (List.ofFn f) φ = true) ⋯

@[simp]

theorem Complexity.SAT.Clause.eval_append (α : Assignment) (c d : Clause) : eval α (c ++ d) = (eval α c || eval α d)

Evaluating a concatenation of clauses is the disjunction of the evaluations.

@[simp]

theorem Complexity.SAT.CNF.eval_append (α : Assignment) (φ ψ : CNF) : eval α (φ ++ ψ) = (eval α φ && eval α ψ)

Evaluating a concatenation of CNFs is the conjunction of the evaluations.