Parity constraints in conjunctive normal form

The constraint that the parity of the variables in a finite set B is c has a formula in conjunctive normal form with one clause for each assignment to B of the other parity, excluding that assignment (CNF.parityOnEq); assignments to B are indexed by the subsets of B on which they are true. Its clauses have #B literals each, and there are at most 2 ^ #B of them (CNF.length_parityOnEq_le).

Main definitions

• Cslib.Logic.PL.Clause.exclude: the clause excluding the values of an assignment on a set of variables.
• Cslib.Logic.PL.CNF.parityOnEq: the parity constraint on a finite set of variables.

Main results

• Cslib.Logic.PL.CNF.eval_parityOnEq_eq_true_iff: CNF.parityOnEq B c holds exactly when the parity of the variables in B is c.
• Cslib.Logic.PL.CNF.length_parityOnEq_le: it has at most 2 ^ #B clauses.

References

• A. Urquhart, Hard examples for resolution, for parity constraints in conjunctive normal form as the clauses of Tseitin formulas

noncomputable def Cslib.Logic.PL.Clause.exclude {ι : Type u_1} (B : Finset ι) (y : ι → Bool) : Clause ι

The clause excluding the values of y on B: it holds when the assignment differs from y at some variable in B.

theorem Cslib.Logic.PL.Clause.eval_exclude_eq_true_iff {ι : Type u_1} (B : Finset ι) (y x : ι → Bool) : eval x (exclude B y) = true ↔ ∃ i ∈ B, x i ≠ y i

@[simp]

theorem Cslib.Logic.PL.Clause.length_exclude {ι : Type u_1} (B : Finset ι) (y : ι → Bool) : List.length (exclude B y) = B.card

theorem Cslib.Logic.PL.Clause.mem_exclude {ι : Type u_1} {B : Finset ι} {y : ι → Bool} {l : Literal ι} : l ∈ exclude B y ↔ l.1 ∈ B ∧ l.2 = !y l.1

The literals of Clause.exclude B y are the variables of B, with the polarity opposite to their values in y.

noncomputable def Cslib.Logic.PL.CNF.parityOnEq {ι : Type u_1} [DecidableEq ι] (B : Finset ι) (c : Bool) : CNF ι

A formula in conjunctive normal form saying that the parity of the variables in B is c: for each subset A of B such that the assignment true on A and false on the rest of B has the other parity, a clause excludes that assignment.

theorem Cslib.Logic.PL.CNF.eval_parityOnEq_eq_true_iff {ι : Type u_1} [DecidableEq ι] (B : Finset ι) (c : Bool) (x : ι → Bool) : eval x (parityOnEq B c) = true ↔ parityOn B x = c

The semantics of parity constraints: CNF.parityOnEq B c holds exactly when the parity of the variables in B is c.

theorem Cslib.Logic.PL.CNF.exists_eq_exclude_of_mem_parityOnEq {ι : Type u_1} [DecidableEq ι] {B : Finset ι} {c : Bool} {d : Clause ι} (hd : d ∈ parityOnEq B c) : ∃ (y : ι → Bool), d = Clause.exclude B y

A clause of CNF.parityOnEq B c excludes an assignment to B.

theorem Cslib.Logic.PL.CNF.length_of_mem_parityOnEq {ι : Type u_1} [DecidableEq ι] {B : Finset ι} {c : Bool} {d : Clause ι} (hd : d ∈ parityOnEq B c) : List.length d = B.card

The clauses of CNF.parityOnEq B c have #B literals.

theorem Cslib.Logic.PL.CNF.length_parityOnEq_le {ι : Type u_1} [DecidableEq ι] (B : Finset ι) (c : Bool) : List.length (parityOnEq B c) ≤ 2 ^ B.card

CNF.parityOnEq B c has at most 2 ^ #B clauses: one per subset of B.