Exactly-one constraints

CNF.exactlyOne vs holds exactly when one variable of the list vs is true: one clause asks for at least one of them, and one binary clause for each pair of distinct variables forbids two. This is the standard one-hot encoding of a finite-valued quantity by Boolean variables.

CNF.atMostOne emits a clause for every ordered pair of distinct variables, so each pair appears twice. The quadratic size is the same as for unordered pairs, and the semantics (CNF.eval_atMostOne) then holds for lists with repetitions too, without a Nodup hypothesis.

Main definitions

• Cslib.Logic.PL.CNF.atLeastOne, Cslib.Logic.PL.CNF.atMostOne, Cslib.Logic.PL.CNF.exactlyOne.

Main results

• Cslib.Logic.PL.CNF.eval_exactlyOne: the semantics.
• Cslib.Logic.PL.CNF.eq_true_iff_of_eval_exactlyOne: once one variable of the list is known to be true, every variable of the list is true exactly when it is that one.
• Cslib.Logic.PL.CNF.fst_mem_of_mem_exactlyOne: the variables of the constraints are those of the list.

References

• S. Arora, B. Barak, Computational Complexity: A Modern Approach, Section 2.3

def Cslib.Logic.PL.CNF.atLeastOne {V : Type u_1} (vs : List V) : CNF V

At least one variable of vs is true.

theorem Cslib.Logic.PL.CNF.eval_atLeastOne {V : Type u_1} (σ : V → Bool) (vs : List V) : eval σ (atLeastOne vs) = true ↔ ∃ (x : V), x ∈ vs ∧ σ x = true

def Cslib.Logic.PL.CNF.atMostOne {V : Type u_1} [DecidableEq V] (vs : List V) : CNF V

No two distinct variables of vs are true.

def Cslib.Logic.PL.CNF.exactlyOne {V : Type u_1} [DecidableEq V] (vs : List V) : CNF V

Exactly one variable of vs is true.

theorem Cslib.Logic.PL.CNF.eval_atMostOne {V : Type u_1} [DecidableEq V] (σ : V → Bool) (vs : List V) : eval σ (atMostOne vs) = true ↔ ∀ (x : V), x ∈ vs → ∀ (y : V), y ∈ vs → σ x = true → σ y = true → x = y

theorem Cslib.Logic.PL.CNF.fst_mem_of_mem_atMostOne {V : Type u_1} [DecidableEq V] {vs : List V} {c : Clause V} (hc : c ∈ atMostOne vs) {l : Literal V} (hl : l ∈ c) : l.fst ∈ vs

The variables of CNF.atMostOne vs are among vs.

theorem Cslib.Logic.PL.CNF.fst_mem_of_mem_exactlyOne {V : Type u_1} [DecidableEq V] {vs : List V} {c : Clause V} (hc : c ∈ exactlyOne vs) {l : Literal V} (hl : l ∈ c) : l.fst ∈ vs

The variables of CNF.exactlyOne vs are among vs.

theorem Cslib.Logic.PL.CNF.eval_exactlyOne {V : Type u_1} [DecidableEq V] (σ : V → Bool) (vs : List V) : eval σ (exactlyOne vs) = true ↔ (∃ (x : V), x ∈ vs ∧ σ x = true) ∧ ∀ (x : V), x ∈ vs → ∀ (y : V), y ∈ vs → σ x = true → σ y = true → x = y

CNF.exactlyOne vs holds exactly when some variable of vs is true and no two distinct variables of vs are.

theorem Cslib.Logic.PL.CNF.eq_true_iff_of_eval_exactlyOne {V : Type u_1} [DecidableEq V] {σ : V → Bool} {vs : List V} (h : eval σ (exactlyOne vs) = true) {x : V} (hx : x ∈ vs) (hσx : σ x = true) {y : V} (hy : y ∈ vs) : σ y = true ↔ y = x

If exactly one variable of vs is true and x ∈ vs is true, then each y ∈ vs is true exactly when y = x.

theorem Cslib.Logic.PL.CNF.eval_exactlyOne_of_iff {V : Type u_1} [DecidableEq V] {σ : V → Bool} {vs : List V} {x : V} (hx : x ∈ vs) (h : ∀ (y : V), y ∈ vs → (σ y = true ↔ y = x)) : eval σ (exactlyOne vs) = true

An assignment that makes exactly the variable x ∈ vs true among vs satisfies CNF.exactlyOne vs.

theorem Cslib.Logic.PL.CNF.eq_true_iff_of_eval_exactlyOne_map {V : Type u_1} [DecidableEq V] {ι : Type u_2} {σ : V → Bool} {f : ι → V} (hf : Function.Injective f) {l : List ι} (h : eval σ (exactlyOne (List.map f l)) = true) {x : ι} (hx : x ∈ l) (hσx : σ (f x) = true) {y : ι} (hy : y ∈ l) : σ (f y) = true ↔ y = x

CNF.eq_true_iff_of_eval_exactlyOne for the one-hot encoding l.map f of a quantity ranging over l, along an injective naming f of its values.

theorem Cslib.Logic.PL.CNF.eval_exactlyOne_map_of_iff {V : Type u_1} [DecidableEq V] {ι : Type u_2} {σ : V → Bool} {f : ι → V} (hf : Function.Injective f) {l : List ι} {x : ι} (hx : x ∈ l) (h : ∀ (y : ι), y ∈ l → (σ (f y) = true ↔ y = x)) : eval σ (exactlyOne (List.map f l)) = true

CNF.eval_exactlyOne_of_iff for the one-hot encoding l.map f.