Dense variable numbering for CNF formulas

CNF.denseRelabel φ renames each variable of a CNF formula φ by its index in φ.distinctVars. Unlike CNF.compact (which uses first positions in φ.vars and can leave gaps when variables repeat), CNF.denseRelabel φ maps the occurring variables bijectively onto 0, …, φ.numVars - 1 in order of first occurrence (a library adaptation to the declared-variable model of [OAI26c]).

The renaming preserves clause lengths, clause count, numVars, Satisfiable, modelCount, and gives φ.denseRelabel.modelCountOn (Finset.range φ.numVars) = φ.modelCount. It is computable in polynomial time for any variable encoding, both into unary variable indices and into binary natural-number indices (encCNF).

Main definitions

• Cslib.Logic.PL.CNF.denseRelabel: rename variables by their positions in distinctVars.

Main results

• Cslib.Logic.PL.CNF.vars_denseRelabel_toFinset, Cslib.Logic.PL.CNF.numVars_denseRelabel, Cslib.Logic.PL.CNF.distinctVars_denseRelabel, Cslib.Logic.PL.CNF.count_vars_denseRelabel, Cslib.Logic.PL.CNF.count_vars_denseRelabel_le: the occurring variables of φ.denseRelabel are 0, …, φ.numVars - 1 in order, with preserved literal-occurrence counts.
• Cslib.Logic.PL.CNF.satisfiable_denseRelabel, Cslib.Logic.PL.CNF.modelCount_denseRelabel, Cslib.Logic.PL.CNF.modelCountOn_denseRelabel: satisfiability and model counts are preserved.
• Cslib.Logic.PL.CNF.computableInPolyTime_denseRelabel_unary, Cslib.Logic.PL.CNF.computableInPolyTime_denseRelabel, Cslib.Complexity.SAT.computableInPolyTime_denseRelabel: dense relabeling is computable in polynomial time.

References

• OpenAI, The Exponential Time Hypothesis is False

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

Rename each variable of φ by its index in φ.distinctVars, producing dense variable indices 0, …, φ.numVars - 1.

@[simp]

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

Dense relabeling preserves all clause lengths in order.

@[simp]

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

Dense relabeling preserves the number of clauses.

theorem Cslib.Logic.PL.CNF.all_length_le_denseRelabel {V : Type u_1} [DecidableEq V] {k : ℕ} (φ : CNF V) : (∀ c ∈ φ.denseRelabel, List.length c ≤ k) ↔ ∀ c ∈ φ, List.length c ≤ k

Dense relabeling preserves any uniform upper bound on clause lengths.

@[simp]

theorem Cslib.Logic.PL.CNF.vars_denseRelabel_toFinset {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.denseRelabel.vars.toFinset = Finset.range φ.numVars

The occurring variables of φ.denseRelabel are Finset.range φ.numVars.

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

Every variable occurring in φ.denseRelabel is strictly below φ.numVars.

@[simp]

theorem Cslib.Logic.PL.CNF.numVars_denseRelabel {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.denseRelabel.numVars = φ.numVars

Dense relabeling preserves the number of distinct occurring variables.

@[simp]

theorem Cslib.Logic.PL.CNF.distinctVars_denseRelabel {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.denseRelabel.distinctVars = List.range φ.numVars

The distinct variables of φ.denseRelabel in order of first occurrence are 0, …, φ.numVars - 1.

theorem Cslib.Logic.PL.CNF.count_vars_denseRelabel {V : Type u_1} [DecidableEq V] (φ : CNF V) {v : V} (hv : v ∈ φ.vars) : List.count (List.idxOf v φ.distinctVars) φ.denseRelabel.vars = List.count v φ.vars

Dense variable relabeling preserves the exact literal-occurrence count of every occurring variable.

theorem Cslib.Logic.PL.CNF.count_vars_denseRelabel_le {V : Type u_1} [DecidableEq V] (φ : CNF V) {B : ℕ} (h : ∀ (v : V), List.count v φ.vars ≤ B) (i : ℕ) : List.count i φ.denseRelabel.vars ≤ B

Any upper bound on original literal-occurrence counts is preserved by CNF.denseRelabel.

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

Reading original variable values at their distinctVars indices recovers the evaluation of φ.

@[simp]

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

Dense relabeling preserves satisfiability.

@[simp]

theorem Cslib.Logic.PL.CNF.modelCount_denseRelabel {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.denseRelabel.modelCount = φ.modelCount

Dense relabeling preserves the occurring-variable model count.

theorem Cslib.Logic.PL.CNF.modelCountOn_denseRelabel {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.denseRelabel.modelCountOn (Finset.range φ.numVars) = φ.modelCount

Dense relabeling preserves the declared-variable model count on Finset.range φ.numVars.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_denseRelabel_unary {W : Type} [DecidableEq W] (enc : W ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime denseRelabel (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encUnary Turing.MultiTapeTM.encBool)))

Dense relabeling is polynomial-time into unary variable indices for any variable encoding.

theorem Cslib.Logic.PL.CNF.computableInPolyTime_denseRelabel {W : Type} [DecidableEq W] (enc : W ↪ List Bool) : Turing.MultiTapeTM.ComputableInPolyTime denseRelabel (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encList (Turing.MultiTapeTM.encPair enc Turing.MultiTapeTM.encBool))) Complexity.encCNF

Dense relabeling is polynomial-time into binary natural-number variable indices (encCNF) for any variable encoding.

theorem Cslib.Complexity.SAT.computableInPolyTime_denseRelabel : Turing.MultiTapeTM.ComputableInPolyTime Logic.PL.CNF.denseRelabel encCNF encCNF

Dense variable relabeling on CNF ℕ is computable in polynomial time.