The largest variable index, by slot

CNF.maxVar folds over clauses and then over literals. An algorithm instead loops over a flat slot index and takes the largest value it sees. The two are the same number, and this module says why: each bounds the family of variable indices and each is attained by it.

Main results

• Complexity.var_le_maxVar — every literal's index is at most maxVar
• Complexity.exists_slot_eq_maxVar — and some literal attains it
• Complexity.maxOver_slotVar — the loop computes maxVar

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

theorem Complexity.var_le_maxVar (φ : SAT.CNF) {j : ℕ} (hj : j < List.length φ) {p : ℕ} (hp : p < List.length φ[j]) : φ[j][p].var ≤ φ.maxVar

Every literal's index is at most the formula's largest.

theorem Complexity.exists_lit_eq_maxVar (c : SAT.Clause) : 0 < List.length c → ∃ (p : ℕ) (hp : p < List.length c), c[p].var = c.maxVar

Some literal of a nonempty clause attains its largest index.

theorem Complexity.exists_clause_eq_maxVar (φ : SAT.CNF) : 0 < List.length φ → ∃ (j : ℕ) (hj : j < List.length φ), φ[j].maxVar = φ.maxVar

Some clause of a nonempty formula attains its largest index.

theorem Complexity.exists_slot_eq_maxVar (φ : SAT.CNF) (h3 : φ.Is3CNF) (h : 0 < List.length φ) : ∃ (j : ℕ) (hj : j < List.length φ) (p : ℕ) (hp : p < List.length φ[j]), φ[j][p].var = φ.maxVar

Some literal attains the formula's largest index.

The loop computes maxVar

noncomputable def Complexity.slotVar (w : List Bool) : List Bool

The variable index at a flat slot, read off the encoding.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.slotVar_mem_FP : slotVar ∈ FP

theorem Complexity.slotVar_eq (φ : SAT.CNF) {i j p : ℕ} (hj : j < List.length φ) (hp : p < List.length φ[j]) (hdj : i / 3 = j) (hdp : i % 3 = p) : (slotVar (pair φ.encode (List.replicate i true))).length = φ[j][p].var

theorem Complexity.maxOver_slotVar (φ : SAT.CNF) (h3 : φ.Is3CNF) : maxOver slotVar φ.encode (3 * List.length φ) = φ.maxVar

The loop computes maxVar.