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_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_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.