Compact variable numbering for CNF formulas

Variables are renamed by their first positions in the list of literal occurrences. The resulting indices are smaller than the number of occurrences, even when the original names have a succinct encoding. Repeated variables retain the same name. This prepares reductions whose output indices are unary without expanding binary input names into unary integers.

Main definitions

• Cslib.Logic.PL.CNF.compact: rename variables by their first occurrences.

Main results

• Cslib.Logic.PL.CNF.satisfiable_relabel_idxOf: renaming variables by their positions in a list containing them preserves satisfiability.
• Cslib.Logic.PL.CNF.satisfiable_compact: compaction preserves satisfiability.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 2.3

def Cslib.Logic.PL.CNF.compact {V : Type u_1} [DecidableEq V] (φ : CNF V) : CNF ℕ

Rename each variable by its first position among all literal occurrences.

@[simp]

theorem Cslib.Logic.PL.CNF.map_length_compact {V : Type u_1} [DecidableEq V] (φ : CNF V) : List.map List.length φ.compact = List.map List.length φ

Compaction keeps all clauses, their order, and their lengths.

@[simp]

theorem Cslib.Logic.PL.CNF.length_compact {V : Type u_1} [DecidableEq V] (φ : CNF V) : List.length φ.compact = List.length φ

Compaction preserves the number of clauses.

theorem Cslib.Logic.PL.CNF.mem_vars_compact_lt {V : Type u_1} [DecidableEq V] (φ : CNF V) {v : ℕ} (hv : v ∈ φ.compact.vars) : v < φ.vars.length

Every renamed variable is below the number of literal occurrences.

theorem Cslib.Logic.PL.CNF.eval_relabel_idxOf {V : Type u_1} [DecidableEq V] (φ : CNF V) {l : List V} (hl : ∀ (v : V), v ∈ φ.vars → v ∈ l) (σ : V → Bool) : eval (fun (i : ℕ) => l[i]?.elim false σ) (relabel (fun (a : V) => List.idxOf a l) φ) = eval σ φ

Renaming each variable by its position in a list l containing all variables of φ is undone by reading the names back from l.

theorem Cslib.Logic.PL.CNF.satisfiable_relabel_idxOf {V : Type u_1} [DecidableEq V] (φ : CNF V) {l : List V} (hl : ∀ (v : V), v ∈ φ.vars → v ∈ l) : (relabel (fun (a : V) => List.idxOf a l) φ).Satisfiable ↔ φ.Satisfiable

Renaming by positions in a list containing all variables preserves satisfiability.

theorem Cslib.Logic.PL.CNF.eval_compact {V : Type u_1} [DecidableEq V] (φ : CNF V) (σ : V → Bool) : eval (fun (i : ℕ) => φ.vars[i]?.elim false σ) φ.compact = eval σ φ

Reading original names at the compact positions recovers the original evaluation.

theorem Cslib.Logic.PL.CNF.satisfiable_compact {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.compact.Satisfiable ↔ φ.Satisfiable

Compaction preserves satisfiability, without requiring a finite variable type.