Parsimonious conversion of ordinary clauses to exact-one clauses

Each clause of width at most three is replaced by the four-clause disjunction gadget of [Hunt, Marathe, Radhakrishnan and Stearns, Theorem 3.8, Figure 3.4] [HMRS98]. Missing literals are replaced by distinct, uniquely forced false variables. Unlike repeating a source literal, this preserves the number of occurrences of every source variable. Even an empty clause has an exact-three, unsatisfiable output. Clauses longer than three are truncated; correctness therefore requires the width bound.

Main definitions

• FromSAT.clause: the constant-size replacement of one clause.
• FromSAT.formula: replace every clause with separately indexed auxiliaries.
• FromSAT.assignment: the canonical extension of a source assignment.

Main results

• FromSAT.length_clause_le, FromSAT.length_formula_le: constant-factor clause bounds.

References

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

@[reducible, inline]

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

Source variables and clause-indexed auxiliary slots.

def Cslib.Logic.PL.CNF.FromSAT.aux {V : Type u_1} (i k : ℕ) : Variable V

An auxiliary slot local to one source clause.

def Cslib.Logic.PL.CNF.FromSAT.lift {V : Type u_1} (l : Literal V) : Literal (Variable V)

Embed a signed source literal.

def Cslib.Logic.PL.CNF.FromSAT.padding {V : Type u_1} (i k : ℕ) : Literal (Variable V)

A positive padding literal, used only when the corresponding source position is absent.

def Cslib.Logic.PL.CNF.FromSAT.core {V : Type u_1} (i : ℕ) (p q r : Literal (Variable V)) : CNF (Variable V)

The uniquely extensible disjunction gadget in local slots three through seven.

def Cslib.Logic.PL.CNF.FromSAT.forcePadding {V : Type u_1} (i k : ℕ) : CNF (Variable V)

Force padding slot k false, using its own three auxiliary slots.

def Cslib.Logic.PL.CNF.FromSAT.clause {V : Type u_1} (i : ℕ) : Clause V → CNF (Variable V)

Replace one clause by exact-three exact-one clauses, retaining each of its first three source occurrences once. Literals after the third are dropped.

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

Replace the source clauses, distinguishing auxiliaries by clause position.

def Cslib.Logic.PL.CNF.FromSAT.sourceValue {V : Type u_1} (σ : V → Bool) (c : Clause V) (k : ℕ) : Bool

The source truth value at a clause position; absent positions are false.

def Cslib.Logic.PL.CNF.FromSAT.auxiliaryValue {V : Type u_1} (σ : V → Bool) (c : Clause V) (k : ℕ) : Bool

Canonical auxiliary values, including all three possible false-padding blocks.

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

Extend an assignment by the uniquely determined values of all occurring auxiliaries.

theorem Cslib.Logic.PL.CNF.FromSAT.length_clause_le {V : Type u_1} (i : ℕ) (c : Clause V) : List.length (clause i c) ≤ 13

A clause contributes at most thirteen clauses.

theorem Cslib.Logic.PL.CNF.FromSAT.width_clause {V : Type u_1} (i : ℕ) (c : Clause V) (d : Clause (Variable V)) : d ∈ clause i c → List.length d = 3

Every output clause has exactly three literal occurrences.

theorem Cslib.Logic.PL.CNF.FromSAT.length_formula_le {V : Type u_1} (φ : CNF V) : List.length (formula φ) ≤ 13 * List.length φ

Clause replacement increases the number of clauses by at most a factor of thirteen.

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

Every output clause is exact-three, including on malformed source inputs.

theorem Cslib.Logic.PL.CNF.FromSAT.clause_sound {V : Type u_1} (i : ℕ) (c : Clause V) (hc : List.length c ≤ 3) (τ : Variable V → Bool) (hτ : evalOne τ (clause i c) = true) : Clause.eval (fun (v : V) => τ (Sum.inl v)) c = true

Every satisfying replacement restricts to a satisfying source clause.

theorem Cslib.Logic.PL.CNF.FromSAT.clause_complete {V : Type u_1} (φ : CNF V) (σ : V → Bool) (i : ℕ) (c : Clause V) (hi : φ[i]? = some c) (hc : List.length c ≤ 3) : evalOne (assignment φ σ) (clause i c) = Clause.eval σ c

The canonical extension satisfies a local gadget exactly when its source clause holds.

theorem Cslib.Logic.PL.CNF.FromSAT.formula_sound {V : Type u_1} (φ : CNF V) (hw : ∀ c ∈ φ, List.length c ≤ 3) (τ : Variable V → Bool) (hτ : evalOne τ (formula φ) = true) : eval (fun (v : V) => τ (Sum.inl v)) φ = true

Restricting an exact-one output assignment recovers an ordinary satisfying assignment.

theorem Cslib.Logic.PL.CNF.FromSAT.evalOne_formula_assignment {V : Type u_1} (φ : CNF V) (σ : V → Bool) (hw : ∀ c ∈ φ, List.length c ≤ 3) : evalOne (assignment φ σ) (formula φ) = eval σ φ

The canonical extension satisfies the output exactly when the source assignment does.

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

Width-three ordinary satisfiability is equivalent to exact-one output satisfiability.

theorem Cslib.Logic.PL.CNF.FromSAT.length_vars_formula_le {V : Type u_1} (φ : CNF V) : (formula φ).vars.length ≤ 39 * List.length φ

Three literal occurrences per output clause give a constant-factor literal bound.

theorem Cslib.Logic.PL.CNF.FromSAT.count_inl_clause {V : Type u_1} [DecidableEq V] (i : ℕ) (c : Clause V) (hc : List.length c ≤ 3) (v : V) : List.count (Sum.inl v) (clause i c).vars = List.count v (vars [c])

Every inherited variable occurs exactly as often in its clause replacement as in the source clause. This includes repeated literals with either polarity.

theorem Cslib.Logic.PL.CNF.FromSAT.auxiliary_index {V : Type u_1} {i j k : ℕ} {c : Clause V} (h : Sum.inr (j, k) ∈ (clause i c).vars) : j = i

The replacement uses auxiliaries only in its own clause index.

theorem Cslib.Logic.PL.CNF.FromSAT.count_aux_clause {V : Type u_1} [DecidableEq V] (i j k : ℕ) (c : Clause V) : List.count (Sum.inr (j, k)) (clause i c).vars ≤ 3

No local auxiliary exceeds three occurrences.

theorem Cslib.Logic.PL.CNF.FromSAT.nodup_clause {V : Type u_1} (i : ℕ) (c : Clause V) (d : Clause (Variable V)) : d ∈ clause i c → (List.map Prod.fst d).Nodup

Every replacement clause has three distinct variable names, even when source variables are repeated.

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

Taking variable occurrences commutes with concatenating clause replacements.

theorem Cslib.Logic.PL.CNF.FromSAT.count_inl_formula {V : Type u_1} [DecidableEq V] (φ : CNF V) (hw : ∀ c ∈ φ, List.length c ≤ 3) (v : V) : List.count (Sum.inl v) (formula φ).vars = List.count v φ.vars

Source occurrence counts are preserved exactly by the whole replacement.

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

Each auxiliary belongs to just one source clause, so the local degree bound is global.

theorem Cslib.Logic.PL.CNF.FromSAT.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 : Variable V) : List.count v (formula φ).vars ≤ 3

A three-occurrence source produces a three-occurrence exact-one formula.

theorem Cslib.Logic.PL.CNF.FromSAT.inl_mem_vars_formula {V : Type u_1} (φ : CNF V) (hw : ∀ c ∈ φ, List.length c ≤ 3) (v : V) : Sum.inl v ∈ (formula φ).vars ↔ v ∈ φ.vars

Exactly the used source variables occur among the inherited output variables.

theorem Cslib.Logic.PL.CNF.FromSAT.clause_agree {V : Type u_1} (i : ℕ) (c : Clause V) (σ τ : Variable V → Bool) (hσ : evalOne σ (clause i c) = true) (hτ : evalOne τ (clause i c) = true) (hs : ∀ l ∈ c, σ (Sum.inl l.1) = τ (Sum.inl l.1)) (v : Variable V) : v ∈ (clause i c).vars → σ v = τ v

Two satisfying local assignments that agree on source variables agree everywhere used by the replacement. This is the unique-extension property on the actual variable support.

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

Satisfying output assignments are determined exactly by their source restrictions.

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

The ordinary and exact-one counts coincide, on occurring variables on both sides.