Parsimonious elimination of negative exact-one literals

Every negative literal occurrence receives its own positive proxy. A positive complement gadget forces the proxy to be the opposite of the original variable, with a unique auxiliary extension. Each original variable keeps exactly its original occurrence count. A clause of width at most three yields at most thirteen clauses, and all newly added clauses are positive triples.

The construction is [Hunt, Marathe, Radhakrishnan and Stearns, Theorem 3.8, Figure 3.5] [HMRS98]. The occurrence indexing and quantitative accounting are original.

Main definitions

• Variable, formula: the occurrence-indexed positive compiler.
• extend: its canonical assignment extension.

Main results

• positive_formula: every emitted literal is positive.
• length_formula_le: a constant-factor clause bound on bounded-width inputs.
• oneModelCount_formula, assignments_agree_iff: count preservation and unique extensions.
• count_inl_formula, count_vars_formula_le: inherited occurrences are preserved exactly, and the occurrence-three restriction is preserved globally.
• nodup_formula: distinct variables within clauses remain distinct.

References

• Hunt, Marathe, Radhakrishnan and Stearns, Theorem 3.8, Figure 3.5 and Lemma 3.6.

@[reducible, inline]

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

Source variables and five private auxiliary slots for each negative occurrence.

def Cslib.Logic.PL.CNF.PositiveExactOne.auxiliary {V : Type u_1} (i j k : ℕ) : Variable V

An auxiliary slot at one clause and literal position. Slot zero is the positive proxy.

def Cslib.Logic.PL.CNF.PositiveExactOne.positiveLiteral {V : Type u_1} (i j : ℕ) (l : Literal V) : Literal (Variable V)

Replace a negative literal by its private positive proxy.

def Cslib.Logic.PL.CNF.PositiveExactOne.complementBlock {V : Type u_1} (i j : ℕ) (l : Literal V) : CNF (Variable V)

The positive complement constraints attached to one negative occurrence.

def Cslib.Logic.PL.CNF.PositiveExactOne.clauseClauses {V : Type u_1} (i : ℕ) (c : Clause V) : CNF (Variable V)

One source clause and the positive complement constraints for its negative occurrences.

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

Replace all negative literal occurrences by positive proxies and complement constraints.

def Cslib.Logic.PL.CNF.PositiveExactOne.extend {V : Type u_1} (φ : CNF V) (σ : V → Bool) : Variable V → Bool

Extend a source assignment: proxies complement the source variable and the remaining slots have the unique values of the false gadget. Unused slots are immaterial.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.extend_auxiliary_zero {V : Type u_1} (φ : CNF V) (σ : V → Bool) {i j : ℕ} {c : Clause V} {l : Literal V} (hc : φ[i]? = some c) (hl : c[j]? = some l) : extend φ σ (auxiliary i j 0) = !σ l.1

Canonical proxy values at an existing source occurrence.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.extend_auxiliary_constants {V : Type u_1} (φ : CNF V) (σ : V → Bool) (i j : ℕ) : extend φ σ (auxiliary i j 1) = false ∧ extend φ σ (auxiliary i j 2) = false ∧ extend φ σ (auxiliary i j 3) = true ∧ extend φ σ (auxiliary i j 4) = false

Canonical values of the constant gadget's four slots.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.evalOne_complementBlock_extend {V : Type u_1} (φ : CNF V) (σ : V → Bool) {i j : ℕ} {c : Clause V} {l : Literal V} (hc : φ[i]? = some c) (hl : c[j]? = some l) : evalOne (extend φ σ) (complementBlock i j l) = true

A negative occurrence's complement constraints hold under the canonical extension.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.evalOne_inheritedClause {V : Type u_1} (τ : Variable V → Bool) (i : ℕ) (c : Clause V) (hcomp : ∀ a ∈ List.zipIdx c, evalOne τ (complementBlock i a.2 a.1) = true) : Clause.evalOne τ (List.map (fun (x : Literal V × ℕ) => match x with | (l, j) => positiveLiteral i j l) (List.zipIdx c)) = Clause.evalOne (fun (v : V) => τ (Sum.inl v)) c

If every complement block holds, the inherited positive clause has the original exact-one value under the assignment read from source variables.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.evalOne_clauseClauses_iff {V : Type u_1} (τ : Variable V → Bool) (i : ℕ) (c : Clause V) : evalOne τ (clauseClauses i c) = true ↔ Clause.evalOne (fun (v : V) => τ (Sum.inl v)) c = true ∧ ∀ a ∈ List.zipIdx c, evalOne τ (complementBlock i a.2 a.1) = true

A compiled clause is exactly the source clause together with its complement constraints.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.evalOne_of_formula {V : Type u_1} (φ : CNF V) (τ : Variable V → Bool) (hτ : evalOne τ (formula φ) = true) : evalOne (fun (v : V) => τ (Sum.inl v)) φ = true

A satisfying positive output assignment restricts to a satisfying source assignment.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.evalOne_formula_extend {V : Type u_1} (φ : CNF V) (σ : V → Bool) : evalOne (extend φ σ) (formula φ) = evalOne σ φ

Canonical extension preserves the exact-one value of the whole source formula.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.oneSatisfiable_formula_iff {V : Type u_1} (φ : CNF V) : (formula φ).OneSatisfiable ↔ φ.OneSatisfiable

The positive output is exact-one satisfiable exactly when the source is.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.evalOne_complementBlock_of_formula {V : Type u_1} (φ : CNF V) (τ : Variable V → Bool) (hτ : evalOne τ (formula φ) = true) {i j : ℕ} {c : Clause V} {l : Literal V} (hc : φ[i]? = some c) (hl : c[j]? = some l) : evalOne τ (complementBlock i j l) = true

Every negative-occurrence complement block is satisfied by a satisfying output assignment.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.sourceVariable_mem_formula {V : Type u_1} {φ : CNF V} {v : V} (hv : v ∈ φ.vars) : Sum.inl v ∈ (formula φ).vars

Every source variable remains present, even when all its occurrences are negative.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.complementBlock_assignments_agree {V : Type u_1} (σ τ : Variable V → Bool) (i j : ℕ) (l : Literal V) (hσ : evalOne σ (complementBlock i j l) = true) (hτ : evalOne τ (complementBlock i j l) = true) (hsource : σ (Sum.inl l.1) = τ (Sum.inl l.1)) (v : Variable V) : v ∈ (complementBlock i j l).vars → σ v = τ v

Satisfying complement blocks with equal source values agree on all of their variables.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.assignments_agree_iff {V : Type u_1} {φ : CNF V} {σ τ : Variable V → Bool} (hσ : evalOne σ (formula φ) = true) (hτ : evalOne τ (formula φ) = true) : (∀ v ∈ (formula φ).vars, σ v = τ v) ↔ ∀ v ∈ φ.vars, σ (Sum.inl v) = τ (Sum.inl v)

Satisfying output assignments agree exactly when their source restrictions agree.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.oneModelCount_formula {V : Type u_1} [DecidableEq V] (φ : CNF V) : (formula φ).oneModelCount = φ.oneModelCount

Polarity elimination preserves the number of satisfying assignments on occurring variables.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.complementBlock_positive {V : Type u_1} (i j : ℕ) (v : V) : complementBlock i j (v, true) = []

A positive literal introduces no complement clauses.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.length_complementBlock_negative {V : Type u_1} (i j : ℕ) (v : V) : List.length (complementBlock i j (v, false)) = 4

A negative literal introduces four clauses.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.length_complementBlock_le {V : Type u_1} (i j : ℕ) (l : Literal V) : List.length (complementBlock i j l) ≤ 4

An individual complement block has at most four clauses.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.length_clauseClauses_le {V : Type u_1} (i : ℕ) (c : Clause V) : List.length (clauseClauses i c) ≤ 1 + 4 * List.length c

An individual source clause contributes at most four clauses per literal, plus itself.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.length_formula_le {V : Type u_1} {k : ℕ} {φ : CNF V} (hw : ∀ c ∈ φ, List.length c ≤ k) : List.length (formula φ) ≤ (1 + 4 * k) * List.length φ

Width at most k gives a factor 1 + 4*k bound on the number of clauses.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.positive_complementBlock {V : Type u_1} (i j : ℕ) (l : Literal V) (c : Clause (Variable V)) : c ∈ complementBlock i j l → ∀ a ∈ c, a.2 = true

All literals in a complement block are positive.

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

Every literal emitted by the compiler is positive.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.width_clauseClauses {V : Type u_1} {k : ℕ} (hk : 3 ≤ k) (i : ℕ) (c : Clause V) (hc : List.length c ≤ k) (a : Clause (Variable V)) : a ∈ clauseClauses i c → List.length a ≤ k

The inherited clause retains its width and every complement clause has width three.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.exactWidth_formula {V : Type u_1} {φ : CNF V} (hw : ∀ c ∈ φ, List.length c = 3) (c : Clause (Variable V)) : c ∈ formula φ → List.length c = 3

Exact-three input clauses yield exact-three positive clauses.

def Cslib.Logic.PL.CNF.PositiveExactOne.occurrenceVariables {V : Type u_1} (i j : ℕ) (l : Literal V) : List (Variable V)

Variable occurrences contributed by one transformed source literal, including its private complement gadget when needed.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.nodup_inheritedClause {V : Type u_1} (i : ℕ) (c : Clause V) (hc : (List.map Prod.fst c).Nodup) : (List.map Prod.fst (List.map (fun (x : Literal V × ℕ) => match x with | (l, j) => positiveLiteral i j l) (List.zipIdx c))).Nodup

Distinct source variables remain distinct in the inherited positive clause.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.nodup_complementBlock {V : Type u_1} (i j : ℕ) (l : Literal V) (c : Clause (Variable V)) : c ∈ complementBlock i j l → (List.map Prod.fst c).Nodup

Every complement clause has three distinct variables, regardless of its source literal.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.nodup_formula {V : Type u_1} {φ : CNF V} (hn : ∀ c ∈ φ, (List.map Prod.fst c).Nodup) (c : Clause (Variable V)) : c ∈ formula φ → (List.map Prod.fst c).Nodup

Distinct variables in every source clause give distinct variables in every output clause.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.width_formula {V : Type u_1} {φ : CNF V} (hw : ∀ c ∈ φ, List.length c ≤ 3) (c : Clause (Variable V)) : c ∈ formula φ → List.length c ≤ 3

Width at most three is preserved.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.length_vars_formula_le {V : Type u_1} {φ : CNF V} (hw : ∀ c ∈ φ, List.length c ≤ 3) : (formula φ).vars.length ≤ 39 * List.length φ

Width-three inputs have at most thirty-nine output literal occurrences per source clause.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.count_vars_clauseClauses {V : Type u_1} [DecidableEq V] (i : ℕ) (c : Clause V) (v : Variable V) : List.count v (clauseClauses i c).vars = (List.map (fun (a : Literal V × ℕ) => List.count v (occurrenceVariables i a.2 a.1)) (List.zipIdx c)).sum

Clause-block variable counts are the sum of the individual occurrence contributions.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.count_inl_occurrenceVariables {V : Type u_1} [DecidableEq V] (i j : ℕ) (l : Literal V) (v : V) : List.count (Sum.inl v) (occurrenceVariables i j l) = List.count v [l.1]

An original variable contributes exactly one occurrence at its original literal position.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.count_aux_occurrenceVariables {V : Type u_1} [DecidableEq V] (i j a b k : ℕ) (l : Literal V) : List.count (auxiliary a b k) (occurrenceVariables i j l) ≤ if a = i ∧ b = j then 3 else 0

A private occurrence contribution uses only its own clause and literal indices and has degree at most three at each auxiliary.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.count_inl_clause {V : Type u_1} [DecidableEq V] (i : ℕ) (c : Clause V) (v : V) : List.count (Sum.inl v) (clauseClauses i c).vars = List.count v (vars [c])

Original variable occurrence counts are unchanged in each compiled clause block.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.count_aux_clause {V : Type u_1} [DecidableEq V] (i a j k : ℕ) (c : Clause V) : List.count (auxiliary a j k) (clauseClauses i c).vars ≤ if a = i then 3 else 0

An auxiliary contributes at most three occurrences in a clause block, and no occurrences outside its own source clause index.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.vars_formula {V : Type u_1} (φ : CNF V) : (formula φ).vars = List.flatMap (fun (c : Clause V × ℕ) => (clauseClauses c.2 c.1).vars) (List.zipIdx φ)

Taking variable occurrences commutes with concatenating clause replacements.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.count_inl_formula {V : Type u_1} [DecidableEq V] (φ : CNF V) (v : V) : List.count (Sum.inl v) (formula φ).vars = List.count v φ.vars

Every original variable keeps exactly its original number of literal occurrences.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.count_aux_formula {V : Type u_1} [DecidableEq V] (φ : CNF V) (i j k : ℕ) : List.count (auxiliary i j k) (formula φ).vars ≤ 3

Every private auxiliary has at most three occurrences in the whole output.

theorem Cslib.Logic.PL.CNF.PositiveExactOne.count_vars_formula_le {V : Type u_1} [DecidableEq V] (φ : CNF V) (ho : ∀ (v : V), List.count v φ.vars ≤ 3) (v : Variable V) : List.count v (formula φ).vars ≤ 3

The positive compiler preserves the three-occurrence restriction.