Occurrence splitting

Each literal occurrence receives its own copy of its variable, indexed by its clause and literal positions. Binary implication cycles force all copies of an original variable to agree. Literal occurrences include repetitions within one clause. This is the construction in Papadimitriou, Proposition 9.3. Only the bound on occurrences of each variable is formalized here; the additional bound of two occurrences per signed literal is not claimed.

Adapted from lean-trominoes at 6d5b36c15cec6cb18d30137b7f1c7fb92ea24332, PeriodicThreeSATThree.lean, PeriodicThreeSATThreeCorrectness.lean, and PeriodicThreeSATThreeExactSize.lean. This construction uses ordinary CNF formulas and Boolean assignments.

The model-count preservation proof is original here, an elementary consequence of copies_agree.

Main definitions

• Cslib.Logic.PL.CNF.occurrenceClauses: separate the literal occurrences.
• Cslib.Logic.PL.CNF.toThreeOccurrence: add implication cycles to the separated clauses.

Main results

• Cslib.Logic.PL.CNF.eval_toThreeOccurrence_iff: correspondence of satisfying assignments.
• Cslib.Logic.PL.CNF.satisfiable_toThreeOccurrence: equisatisfiability.
• Cslib.Logic.PL.CNF.modelCount_toThreeOccurrence: preservation of satisfying-assignment counts.
• Cslib.Logic.PL.CNF.width_toThreeOccurrence: preservation of width bounds of at least two.
• Cslib.Logic.PL.CNF.count_vars_toThreeOccurrence_le: at most three literal occurrences.
• Cslib.Logic.PL.CNF.length_toThreeOccurrence, Cslib.Logic.PL.CNF.length_vars_toThreeOccurrence, Cslib.Logic.PL.CNF.numVars_toThreeOccurrence: exact linear clause, literal and variable counts.

References

• C. H. Papadimitriou, Computational Complexity, Proposition 9.3

def Cslib.Logic.PL.CNF.occurrenceClauses {V : Type u_1} (φ : CNF V) : CNF (V × ℕ × ℕ)

Replace each literal by a copy named by its original variable and its two positions.

Cslib.Logic.PL.occurrences enumerates the same positions as a flat list of triples (clause index, literal index, literal). This clause-preserving traversal instead names each copy (original variable, clause index, literal index), retaining the original clause boundaries.

def Cslib.Logic.PL.CNF.occurrenceCopies {V : Type u_1} [DecidableEq V] (φ : CNF V) (v : V) : List (V × ℕ × ℕ)

The copies belonging to one variable, in their original occurrence order.

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

Split literal occurrences, then add one directed implication cycle per original variable.

theorem Cslib.Logic.PL.CNF.map_length_occurrenceClauses {V : Type u_1} (φ : CNF V) : List.map List.length φ.occurrenceClauses = List.map List.length φ

Copying literals preserves the list of clause lengths.

theorem Cslib.Logic.PL.CNF.relabel_occurrenceClauses {V : Type u_1} (φ : CNF V) : relabel Prod.fst φ.occurrenceClauses = φ

Forgetting copy indices recovers the original formula.

theorem Cslib.Logic.PL.CNF.map_fst_vars_occurrenceClauses {V : Type u_1} (φ : CNF V) : List.map Prod.fst φ.occurrenceClauses.vars = φ.vars

Forgetting copy indices recovers the original variable-occurrence list.

theorem Cslib.Logic.PL.CNF.eval_occurrenceClauses {V : Type u_1} (φ : CNF V) (σ : V → Bool) : eval (σ ∘ Prod.fst) φ.occurrenceClauses = eval σ φ

Copied clauses evaluated by an original assignment have the original value.

theorem Cslib.Logic.PL.CNF.copies_agree {V : Type u_1} [DecidableEq V] {φ : CNF V} {τ : V × ℕ × ℕ → Bool} (h : eval τ φ.toThreeOccurrence = true) {x y : V × ℕ × ℕ} (hx : x ∈ φ.occurrenceClauses.vars) (hy : y ∈ φ.occurrenceClauses.vars) (he : x.1 = y.1) : τ x = τ y

Every cycle block forces its copies to agree.

theorem Cslib.Logic.PL.CNF.eval_toThreeOccurrence_iff {V : Type u_1} [DecidableEq V] (φ : CNF V) (τ : V × ℕ × ℕ → Bool) : eval τ φ.toThreeOccurrence = true ↔ ∃ (σ : V → Bool), eval σ φ = true ∧ ∀ x ∈ φ.occurrenceClauses.vars, σ x.1 = τ x

An assignment satisfies the split formula exactly when its occurring copies agree with a satisfying assignment of the original formula. Together with copies_agree, this retains the assignment correspondence, rather than just equisatisfiability.

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

Occurrence splitting preserves satisfiability, including empty clauses and formulas.

theorem Cslib.Logic.PL.CNF.width_toThreeOccurrence {V : Type u_1} [DecidableEq V] {φ : CNF V} {k : ℕ} (hk : 2 ≤ k) (hφ : ∀ c ∈ φ, List.length c ≤ k) (c : Clause (V × ℕ × ℕ)) : c ∈ φ.toThreeOccurrence → List.length c ≤ k

Cycles are binary, so a width bound of at least two is preserved.

theorem Cslib.Logic.PL.CNF.nodup_vars_occurrenceClauses {V : Type u_1} (φ : CNF V) : φ.occurrenceClauses.vars.Nodup

Every literal occurrence gets a distinct copy, even repeated literals in one clause.

theorem Cslib.Logic.PL.CNF.count_vars_toThreeOccurrence {V : Type u_1} [DecidableEq V] (φ : CNF V) (x : V × ℕ × ℕ) : List.count x φ.toThreeOccurrence.vars = 3 * List.count x φ.occurrenceClauses.vars

A copy occurs exactly three times in the output: once in a source clause, once as the antecedent of an implication, and once as its consequent.

theorem Cslib.Logic.PL.CNF.count_vars_toThreeOccurrence_le {V : Type u_1} [DecidableEq V] (φ : CNF V) (x : V × ℕ × ℕ) : List.count x φ.toThreeOccurrence.vars ≤ 3

Every variable has at most three literal occurrences, counting repetitions.

theorem Cslib.Logic.PL.CNF.length_occurrenceCopies {V : Type u_1} [DecidableEq V] (φ : CNF V) (v : V) : (φ.occurrenceCopies v).length = List.count v φ.vars

The number of copies belonging to an original variable is its literal-occurrence count.

theorem Cslib.Logic.PL.CNF.length_toThreeOccurrence {V : Type u_1} [DecidableEq V] (φ : CNF V) : List.length φ.toThreeOccurrence = List.length φ + φ.vars.length

Splitting adds exactly one binary clause per input literal occurrence.

theorem Cslib.Logic.PL.CNF.length_vars_toThreeOccurrence {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.toThreeOccurrence.vars.length = 3 * φ.vars.length

Splitting triples the total number of literal occurrences.

theorem Cslib.Logic.PL.CNF.numVars_toThreeOccurrence {V : Type u_1} [DecidableEq V] (φ : CNF V) : φ.toThreeOccurrence.numVars = φ.vars.length

There is exactly one distinct output variable per input literal occurrence.

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

Occurrence splitting preserves the number of satisfying assignments on occurring variables, including empty formulas, empty clauses, and repeated literals.