Pigeonhole formulas

The pigeonhole formula PHP^m_n (CNF.pigeonhole m n) has a variable (i, j) for every pigeon i : Fin m and hole j : Fin n, read as "pigeon i sits in hole j". Its pigeon clauses (CNF.pigeonClause) say that every pigeon sits in some hole, and its hole clauses (CNF.holeClause) that no two pigeons sit in the same hole. By the pigeonhole principle it is satisfiable exactly when m ≤ n (CNF.satisfiable_pigeonhole_iff); for m > n it is the classical family of unsatisfiable formulas that are hard for resolution Haken.

Main definitions

• Cslib.Logic.PL.CNF.pigeonClause, Cslib.Logic.PL.CNF.holeClause: the two kinds of clauses.
• Cslib.Logic.PL.CNF.pigeonhole: the pigeonhole formula PHP^m_n.

Main results

• Cslib.Logic.PL.CNF.eval_pigeonhole_eq_true_iff: the semantics of the pigeonhole formula.
• Cslib.Logic.PL.CNF.satisfiable_pigeonhole_iff: PHP^m_n is satisfiable exactly when m ≤ n.
• Cslib.Logic.PL.CNF.length_le_of_mem_pigeonhole, Cslib.Logic.PL.CNF.length_pigeonhole_le: clause-length and formula-size bounds for PHP^m_n.

References

• A. Haken, The intractability of resolution
• S. Jukna, Boolean Function Complexity: Advances and Frontiers, Chapter 18

def Cslib.Logic.PL.CNF.pigeonClause {m : ℕ} (n : ℕ) (i : Fin m) : Clause (Fin m × Fin n)

The pigeon clause of pigeon i: it sits in one of the holes Fin n.

def Cslib.Logic.PL.CNF.holeClause {m n : ℕ} (i i' : Fin m) (j : Fin n) : Clause (Fin m × Fin n)

The hole clause of pigeons i, i' and hole j: i and i' do not both sit in j.

def Cslib.Logic.PL.CNF.pigeonhole (m n : ℕ) : CNF (Fin m × Fin n)

The pigeonhole formula PHP^m_n: every pigeon i : Fin m sits in a hole j : Fin n, and no two pigeons i < i' sit in the same hole.

theorem Cslib.Logic.PL.CNF.mem_pigeonhole {m n : ℕ} {c : Clause (Fin m × Fin n)} : c ∈ pigeonhole m n ↔ (∃ (i : Fin m), c = pigeonClause n i) ∨ ∃ (i : Fin m) (i' : Fin m) (j : Fin n), i < i' ∧ c = holeClause i i' j

The clauses of PHP^m_n are its pigeon clauses and its hole clauses.

@[simp]

theorem Cslib.Logic.PL.CNF.eval_pigeonClause {m n : ℕ} (σ : Fin m × Fin n → Bool) (i : Fin m) : Clause.eval σ (pigeonClause n i) = true ↔ ∃ (j : Fin n), σ (i, j) = true

pigeonClause n i evaluates to true under σ iff σ (i, j) = true for some hole j.

@[simp]

theorem Cslib.Logic.PL.CNF.eval_holeClause {m n : ℕ} (σ : Fin m × Fin n → Bool) (i i' : Fin m) (j : Fin n) : Clause.eval σ (holeClause i i' j) = true ↔ σ (i, j) = false ∨ σ (i', j) = false

holeClause i i' j evaluates to true under σ iff at least one of (i, j) or (i', j) is false.

theorem Cslib.Logic.PL.CNF.eval_pigeonhole_eq_true_iff {m n : ℕ} (σ : Fin m × Fin n → Bool) : eval σ (pigeonhole m n) = true ↔ (∀ (i : Fin m), ∃ (j : Fin n), σ (i, j) = true) ∧ ∀ (i i' : Fin m) (j : Fin n), σ (i, j) = true → σ (i', j) = true → i = i'

The semantics of the pigeonhole formula: an assignment satisfies PHP^m_n when it puts every pigeon in some hole and no two pigeons in the same hole.

theorem Cslib.Logic.PL.CNF.satisfiable_pigeonhole_iff {m n : ℕ} : (pigeonhole m n).Satisfiable ↔ m ≤ n

The pigeonhole principle: PHP^m_n is satisfiable exactly when there are at most as many pigeons as holes.

theorem Cslib.Logic.PL.CNF.not_satisfiable_pigeonhole {m n : ℕ} (h : n < m) : ¬(pigeonhole m n).Satisfiable

PHP^m_n is unsatisfiable when there are more pigeons than holes.

@[simp]

theorem Cslib.Logic.PL.CNF.length_pigeonClause {m : ℕ} (n : ℕ) (i : Fin m) : List.length (pigeonClause n i) = n

The pigeon clause for n holes has length n.

@[simp]

theorem Cslib.Logic.PL.CNF.length_holeClause {m n : ℕ} (i i' : Fin m) (j : Fin n) : List.length (holeClause i i' j) = 2

Every hole clause has length 2.

theorem Cslib.Logic.PL.CNF.length_le_of_mem_pigeonhole {m n : ℕ} {c : Clause (Fin m × Fin n)} (hc : c ∈ pigeonhole m n) : List.length c ≤ max n 2

Every clause of PHP^m_n has at most max n 2 literals.

theorem Cslib.Logic.PL.CNF.length_pigeonhole_le (m n : ℕ) : List.length (pigeonhole m n) ≤ m + n * m ^ 2

PHP^m_n has at most m + n m² clauses.

theorem Cslib.Logic.PL.CNF.card_toFinset_vars_pigeonhole_le (m n : ℕ) : (pigeonhole m n).vars.toFinset.card ≤ m * n

PHP^m_n has at most m n variables.