Parsimonious exact-one clause gadgets

The disjunction gadget is the four-clause construction of [Hunt, Marathe, Radhakrishnan and Stearns, Theorem 3.8, Figure 3.4(a)] [HMRS98]. It admits exactly one auxiliary assignment for each satisfying assignment of the three source literals. The positive constant gadget is their Lemma 3.6; it forces one designated variable false and has a unique assignment to all four variables. Attaching that constant to a positive ternary clause gives a parsimonious complement constraint, as in their Figure 3.5.

Main definitions

• disjunctionClauses: four exact-three clauses replacing one ordinary disjunction.
• forceFalseClauses: three positive clauses forcing a designated variable false.
• complementClauses: four positive clauses enforcing opposite terminal values.

Main results

• disjunctionHolds_iff: disjunction correctness and the unique five auxiliary values.
• evalOne_disjunctionClauses_iff: the corresponding formula-level characterization.
• evalOne_forceFalseClauses_iff, evalOne_complementClauses_iff: unique constant and complement extensions.

References

• Hunt, Marathe, Radhakrishnan and Stearns, Theorem 3.8, Figures 3.4–3.5 and Lemma 3.6.

def Cslib.Logic.PL.CNF.ExactOneGadget.One (a b c : Bool) : Prop

Exactly one of three Boolean values is true.

@[instance_reducible]

instance Cslib.Logic.PL.CNF.ExactOneGadget.instDecidableOne (a b c : Bool) : Decidable (One a b c)

def Cslib.Logic.PL.CNF.ExactOneGadget.DisjunctionHolds (p q r u v w t x : Bool) : Prop

The four scalar exact-one constraints in the parsimonious disjunction gadget.

@[instance_reducible]

instance Cslib.Logic.PL.CNF.ExactOneGadget.instDecidableDisjunctionHolds (p q r u v w t x : Bool) : Decidable (DisjunctionHolds p q r u v w t x)

def Cslib.Logic.PL.CNF.ExactOneGadget.firstAux (p q : Bool) : Bool

The first auxiliary value of the disjunction gadget.

def Cslib.Logic.PL.CNF.ExactOneGadget.secondAux (p q : Bool) : Bool

The second auxiliary value of the disjunction gadget.

def Cslib.Logic.PL.CNF.ExactOneGadget.thirdAux (p q : Bool) : Bool

The third auxiliary value of the disjunction gadget.

def Cslib.Logic.PL.CNF.ExactOneGadget.fourthAux (p q : Bool) : Bool

The fourth auxiliary value of the disjunction gadget.

def Cslib.Logic.PL.CNF.ExactOneGadget.fifthAux (p q r : Bool) : Bool

The fifth auxiliary value of the disjunction gadget.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.disjunctionHolds_iff (p q r u v w t x : Bool) : DisjunctionHolds p q r u v w t x ↔ (p || q || r) = true ∧ u = firstAux p q ∧ v = secondAux p q ∧ w = thirdAux p q ∧ t = fourthAux p q ∧ x = fifthAux p q r

Every satisfying source triple has exactly the displayed auxiliary extension, and the all-false source triple has none.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.disjunctionHolds_canonical_iff (p q r : Bool) : DisjunctionHolds p q r (firstAux p q) (secondAux p q) (thirdAux p q) (fourthAux p q) (fifthAux p q r) ↔ (p || q || r) = true

The canonical auxiliary values satisfy the gadget exactly on satisfying source triples.

def Cslib.Logic.PL.CNF.ExactOneGadget.disjunctionClauses {V : Type u_1} (p q r : Literal V) (u v w t x : V) : CNF V

Replace a signed three-literal disjunction by four exact-three clauses. Auxiliary literals are positive, while the second and third source literals are negated.

def Cslib.Logic.PL.CNF.ExactOneGadget.forceFalseClauses {V : Type u_1} (c d e f : V) : CNF V

A positive three-clause gadget with one true auxiliary and three false variables. The first variable is the false terminal and has two internal occurrences.

def Cslib.Logic.PL.CNF.ExactOneGadget.complementClauses {V : Type u_1} (p q c d e f : V) : CNF V

Opposite terminal values, enforced using a uniquely determined positive false gadget.

def Cslib.Logic.PL.CNF.ExactOneGadget.disjunction : CNF ℕ

The fixed disjunction gadget with source variables 0, 1, 2 and auxiliaries 3 through 7. Its incidence drawing is independent of the literal polarities.

def Cslib.Logic.PL.CNF.ExactOneGadget.forceFalse : CNF ℕ

The fixed positive false gadget, with false terminal 0.

def Cslib.Logic.PL.CNF.ExactOneGadget.complement : CNF ℕ

The fixed positive complement gadget, with terminals 0, 1 and auxiliaries 2 through 5.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.evalOne_triple_iff {V : Type u_1} (σ : V → Bool) (a b c : Literal V) : Clause.evalOne σ [a, b, c] = true ↔ One (Literal.eval σ a) (Literal.eval σ b) (Literal.eval σ c)

The scalar exact-one predicate is the evaluation of three literals.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.evalOne_disjunctionClauses_iff {V : Type u_1} (σ : V → Bool) (p q r : Literal V) (u v w t x : V) : evalOne σ (disjunctionClauses p q r u v w t x) = true ↔ DisjunctionHolds (Literal.eval σ p) (Literal.eval σ q) (Literal.eval σ r) (σ u) (σ v) (σ w) (σ t) (σ x)

Formula evaluation recovers the four scalar constraints.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.evalOne_disjunctionClauses_iff_canonical {V : Type u_1} (σ : V → Bool) (p q r : Literal V) (u v w t x : V) : evalOne σ (disjunctionClauses p q r u v w t x) = true ↔ (Literal.eval σ p || Literal.eval σ q || Literal.eval σ r) = true ∧ σ u = firstAux (Literal.eval σ p) (Literal.eval σ q) ∧ σ v = secondAux (Literal.eval σ p) (Literal.eval σ q) ∧ σ w = thirdAux (Literal.eval σ p) (Literal.eval σ q) ∧ σ t = fourthAux (Literal.eval σ p) (Literal.eval σ q) ∧ σ x = fifthAux (Literal.eval σ p) (Literal.eval σ q) (Literal.eval σ r)

The formula has precisely the canonical disjunction extension.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.evalOne_forceFalseClauses_iff {V : Type u_1} (σ : V → Bool) (c d e f : V) : evalOne σ (forceFalseClauses c d e f) = true ↔ σ c = false ∧ σ d = false ∧ σ e = true ∧ σ f = false

The positive false gadget has exactly the values (false, false, true, false).

theorem Cslib.Logic.PL.CNF.ExactOneGadget.evalOne_complementClauses_iff {V : Type u_1} (σ : V → Bool) (p q c d e f : V) : evalOne σ (complementClauses p q c d e f) = true ↔ σ p = !σ q ∧ σ c = false ∧ σ d = false ∧ σ e = true ∧ σ f = false

The positive complement gadget forces opposite terminals and uniquely fixes every auxiliary variable.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.length_disjunctionClauses {V : Type u_1} (p q r : Literal V) (u v w t x : V) : List.length (disjunctionClauses p q r u v w t x) = 4

The disjunction gadget has four clauses.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.length_forceFalseClauses {V : Type u_1} (c d e f : V) : List.length (forceFalseClauses c d e f) = 3

The positive false gadget has three clauses.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.length_complementClauses {V : Type u_1} (p q c d e f : V) : List.length (complementClauses p q c d e f) = 4

The positive complement gadget has four clauses.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.length_vars_disjunctionClauses {V : Type u_1} (p q r : Literal V) (u v w t x : V) : (disjunctionClauses p q r u v w t x).vars.length = 12

The disjunction gadget has twelve literal occurrences.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.length_vars_forceFalseClauses {V : Type u_1} (c d e f : V) : (forceFalseClauses c d e f).vars.length = 9

The positive false gadget has nine literal occurrences.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.length_vars_complementClauses {V : Type u_1} (p q c d e f : V) : (complementClauses p q c d e f).vars.length = 12

The positive complement gadget has twelve literal occurrences.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.width_disjunctionClauses {V : Type u_1} (p q r : Literal V) (u v w t x : V) (c : Clause V) : c ∈ disjunctionClauses p q r u v w t x → List.length c = 3

Every clause of a disjunction gadget is ternary.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.width_forceFalseClauses {V : Type u_1} (c d e f : V) (a : Clause V) : a ∈ forceFalseClauses c d e f → List.length a = 3

Every clause of a false gadget is ternary.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.width_complementClauses {V : Type u_1} (p q c d e f : V) (a : Clause V) : a ∈ complementClauses p q c d e f → List.length a = 3

Every clause of a complement gadget is ternary.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.positive_forceFalseClauses {V : Type u_1} (c d e f : V) (a : Clause V) : a ∈ forceFalseClauses c d e f → ∀ (l : Literal V), l ∈ a → l.snd = true

The false gadget contains only positive literals.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.positive_complementClauses {V : Type u_1} (p q c d e f : V) (a : Clause V) : a ∈ complementClauses p q c d e f → ∀ (l : Literal V), l ∈ a → l.snd = true

The complement gadget contains only positive literals.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.disjunction_occurrences : List.count 0 disjunction.vars = 1 ∧ List.count 1 disjunction.vars = 1 ∧ List.count 2 disjunction.vars = 1 ∧ List.count 3 disjunction.vars = 2 ∧ List.count 4 disjunction.vars = 3 ∧ List.count 5 disjunction.vars = 2 ∧ List.count 6 disjunction.vars = 1 ∧ List.count 7 disjunction.vars = 1

Occurrence counts of every variable in the fixed disjunction gadget.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.forceFalse_occurrences : List.count 0 forceFalse.vars = 2 ∧ List.count 1 forceFalse.vars = 2 ∧ List.count 2 forceFalse.vars = 3 ∧ List.count 3 forceFalse.vars = 2

The false port has degree two; no variable in the fixed false gadget exceeds degree three.

theorem Cslib.Logic.PL.CNF.ExactOneGadget.complement_occurrences : List.count 0 complement.vars = 1 ∧ List.count 1 complement.vars = 1 ∧ List.count 2 complement.vars = 3 ∧ List.count 3 complement.vars = 2 ∧ List.count 4 complement.vars = 3 ∧ List.count 5 complement.vars = 2

Each complement terminal has degree one, leaving its original incidence capacity intact.