Constant-factor parsimonious compilation to positive exact-one clauses

The two local constructions compose without another occurrence splitter or planarization. Every source clause contributes at most thirteen signed exact-one clauses; replacing their negative occurrences contributes at most thirteen times as many positive clauses. These are bounds on actual emitted lists. Every source variable keeps its occurrence count and no new variable occurs more than three times.

Main definitions

• PositiveExactOneCompile.rawFormula: the structured-variable positive compiler.
• PositiveExactOneCompile.formula: its compact natural-variable output.

Main results

• oneModelCount_formula, oneSatisfiable_formula: parsimony and correctness.
• length_formula_le, length_vars_formula_le: explicit constant-factor bounds.

References

The local gadgets are from [HuntMaratheRadhakrishnanStearns1998, Theorem 3.8]. The composition and quantitative bounds are original.

@[reducible, inline]

abbrev Cslib.Logic.PL.CNF.PositiveExactOneCompile.Variable (V : Type u_2) : Type u_2

The two disjoint families of local auxiliary variables.

def Cslib.Logic.PL.CNF.PositiveExactOneCompile.rawFormula {V : Type u_1} (φ : CNF V) : CNF (Variable V)

Replace disjunctions by uniquely extensible exact-one clauses and remove all negations.

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

Compact natural names for all output variables.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.length_rawFormula_le {V : Type u_1} (φ : CNF V) : List.length (rawFormula φ) ≤ 169 * List.length φ

Both local stages have constant size: at most 169 clauses per source clause.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.width_rawFormula {V : Type u_1} (φ : CNF V) (c : Clause (Variable V)) : c ∈ rawFormula φ → List.length c = 3

Every emitted clause has exactly three literal occurrences.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.positive_rawFormula {V : Type u_1} (φ : CNF V) (c : Clause (Variable V)) : c ∈ rawFormula φ → ∀ l ∈ c, l.2 = true

All output literal polarities are positive.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.nodup_rawFormula {V : Type u_1} (φ : CNF V) (c : Clause (Variable V)) : c ∈ rawFormula φ → (List.map Prod.fst c).Nodup

Every emitted clause has three distinct variables, including when source literals repeat.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.count_vars_rawFormula_le {V : Type u_1} [DecidableEq V] (φ : CNF V) (hw : ∀ c ∈ φ, List.length c ≤ 3) (ho : ∀ (v : V), List.count v φ.vars ≤ 3) (v : Variable V) : List.count v (rawFormula φ).vars ≤ 3

Occurrence-three inputs retain that bound through both local replacements.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.oneModelCount_rawFormula {V : Type u_1} [DecidableEq V] (φ : CNF V) (hw : ∀ c ∈ φ, List.length c ≤ 3) : (rawFormula φ).oneModelCount = φ.modelCount

Model counts are preserved through both uniquely extensible stages.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.length_formula_le {V : Type u_1} [DecidableEq V] (φ : CNF V) : List.length (formula φ) ≤ 169 * List.length φ

Compact numbering preserves the constant-factor clause bound.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.width_formula {V : Type u_1} [DecidableEq V] (φ : CNF V) (c : Clause ℕ) : c ∈ formula φ → List.length c = 3

Every compact output clause has exactly three literal occurrences.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.positive_formula {V : Type u_1} [DecidableEq V] (φ : CNF V) (c : Clause ℕ) : c ∈ formula φ → ∀ l ∈ c, l.2 = true

Compact numbering does not change the positive polarity of any literal.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.nodup_formula {V : Type u_1} [DecidableEq V] (φ : CNF V) (c : Clause ℕ) : c ∈ formula φ → (List.map Prod.fst c).Nodup

Compaction preserves distinct variables within every output clause.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.length_vars_formula_le {V : Type u_1} [DecidableEq V] (φ : CNF V) : (formula φ).vars.length ≤ 507 * List.length φ

The actual output has at most 507 literal occurrences per source clause.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.count_vars_formula_le {V : Type u_1} [DecidableEq V] (φ : CNF V) (hw : ∀ c ∈ φ, List.length c ≤ 3) (ho : ∀ (v : V), List.count v φ.vars ≤ 3) (v : ℕ) : List.count v (formula φ).vars ≤ 3

Compact numbering preserves the degree-three restriction.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.oneModelCount_formula {V : Type u_1} [DecidableEq V] (φ : CNF V) (hw : ∀ c ∈ φ, List.length c ≤ 3) : (formula φ).oneModelCount = φ.modelCount

The final natural-variable output has exactly the source model count.

theorem Cslib.Logic.PL.CNF.PositiveExactOneCompile.oneSatisfiable_formula {V : Type u_1} [DecidableEq V] (φ : CNF V) (hw : ∀ c ∈ φ, List.length c ≤ 3) : (formula φ).OneSatisfiable ↔ φ.Satisfiable

The compiler preserves satisfiability between ordinary and exact-one semantics.