Variable renaming and satisfiability transport

Renaming the variables of a CNF along an injective map preserves satisfiability. This justifies re-indexing the Cook–Levin tableau variables from the Nat.pair-based scheme (convenient for injectivity bookkeeping in the correctness proof) to a flat mixed-radix scheme computable by a Turing machine with unary multiplication and addition only — the form the reduction machine actually emits (docs/A5-ReductionEmitter.md).

Main definitions

• SAT.Lit.mapVar, SAT.Clause.mapVar, SAT.CNF.mapVar — variable renaming

Main results

• SAT.CNF.eval_mapVar_eq — evaluation commutes with renaming, given pointwise-agreeing assignments on the occurring variables
• SAT.CNF.satisfiable_mapVar_iff — renaming along an injective map preserves satisfiability

def Complexity.SAT.Lit.mapVar (f : ℕ → ℕ) (ℓ : Lit) : Lit

Rename a literal's variable along f.

Equations

• Complexity.SAT.Lit.mapVar f ℓ = { sign := ℓ.sign, var := f ℓ.var }

def Complexity.SAT.Clause.mapVar (f : ℕ → ℕ) (c : Clause) : Clause

Rename every variable of a clause along f.

Equations

• Complexity.SAT.Clause.mapVar f c = List.map (Complexity.SAT.Lit.mapVar f) c

def Complexity.SAT.CNF.mapVar (f : ℕ → ℕ) (φ : CNF) : CNF

Rename every variable of a CNF along f.

Equations

• Complexity.SAT.CNF.mapVar f φ = List.map (Complexity.SAT.Clause.mapVar f) φ

@[simp]

theorem Complexity.SAT.CNF.mapVar_nil (f : ℕ → ℕ) : mapVar f [] = []

Renaming the empty CNF yields the empty CNF.

theorem Complexity.SAT.CNF.mapVar_cons (f : ℕ → ℕ) (c : Clause) (φ : CNF) : mapVar f (c :: φ) = Clause.mapVar f c :: mapVar f φ

Renaming distributes over cons: rename the head clause and the tail CNF.

theorem Complexity.SAT.CNF.mapVar_append (f : ℕ → ℕ) (φ ψ : CNF) : mapVar f (φ ++ ψ) = mapVar f φ ++ mapVar f ψ

Renaming distributes over CNF concatenation.

theorem Complexity.SAT.Assignment.get_of_length_le {α : Assignment} {v : ℕ} (h : List.length α ≤ v) : α.get v = false

Out-of-range variables read false.

def Complexity.SAT.Assignment.ofFn (M : ℕ) (g : ℕ → Bool) : Assignment

Tabulate the first M values of a Boolean function as an assignment.

Equations

• Complexity.SAT.Assignment.ofFn M g = List.map g (List.range M)

@[simp]

theorem Complexity.SAT.Assignment.ofFn_length (M : ℕ) (g : ℕ → Bool) : List.length (ofFn M g) = M

The tabulated assignment Assignment.ofFn M g has length M.

theorem Complexity.SAT.Assignment.ofFn_get {M v : ℕ} (g : ℕ → Bool) (h : v < M) : (ofFn M g).get v = g v

Reading Assignment.ofFn M g at an in-range variable v < M returns g v.

theorem Complexity.SAT.Clause.eval_mapVar_eq (α β : Assignment) (f : ℕ → ℕ) (c : Clause) (h : ∀ ℓ ∈ c, α.get (f ℓ.var) = β.get ℓ.var) : eval α (mapVar f c) = eval β c

Clause evaluation commutes with renaming, given assignments that agree pointwise (through f) on the clause's variables.

theorem Complexity.SAT.CNF.eval_mapVar_eq (α β : Assignment) (f : ℕ → ℕ) (φ : CNF) (h : ∀ c ∈ φ, ∀ ℓ ∈ c, α.get (f ℓ.var) = β.get ℓ.var) : eval α (mapVar f φ) = eval β φ

CNF evaluation commutes with renaming, given assignments that agree pointwise (through f) on the formula's variables.

theorem Complexity.SAT.CNF.Satisfiable.mapVar {f : ℕ → ℕ} (hf : Function.Injective f) {φ : CNF} (h : φ.Satisfiable) : (CNF.mapVar f φ).Satisfiable

Renaming preserves satisfiability, forward direction: push the satisfying assignment along the (injective) renaming.

theorem Complexity.SAT.CNF.Satisfiable.of_mapVar {f : ℕ → ℕ} {φ : CNF} (h : (CNF.mapVar f φ).Satisfiable) : φ.Satisfiable

Renaming reflects satisfiability, backward direction: pull the satisfying assignment back through the renaming (no injectivity needed).

theorem Complexity.SAT.CNF.satisfiable_mapVar_iff {f : ℕ → ℕ} (hf : Function.Injective f) (φ : CNF) : (mapVar f φ).Satisfiable ↔ φ.Satisfiable

Satisfiability is invariant under injective variable renaming.