Documentation

Complexity.Logics.Propositional.Tseitin

Tseitin formulas #

A finite multigraph on the vertices V with edges E, parallel edges and self-loops allowed, is given by the map ends : E → Sym2 V sending each edge to its ends (Cslib.Multigraph). Given a charge χ v for every vertex v, the Tseitin formula CNF.tseitinFormula ends χ Tseitin Urquhart has a variable for each edge and says, for every vertex v, that the parity of the edges at v is the charge of v. A self-loop at v would count twice towards the parity of v, so it does not count at all; the parity of v is that of the edges at v that are not self-loops (Multigraph.incidence), and the constraint is expressed by the formula CNF.parityOnEq with a clause per assignment to those edges of the wrong parity. A vertex with d edges other than self-loops thus contributes at most 2 ^ d clauses of d literals each.

Every edge other than a self-loop is at exactly two vertices, so summing the constraints of all vertices gives 0 = ∑ χ: if the total charge is odd, the Tseitin formula is unsatisfiable (CNF.not_satisfiable_tseitinFormula). On a connected multigraph the converse holds, and more: the constraints of all vertices but one are satisfiable, whatever the charges (Tseitin.exists_forall_mem_parityOn_incidence_eq). Flipping the value of an edge flips the parities of its two ends, so flipping the edges of a path flips the parities of its two ends only; combining such flips moves the parities to any target, up to the vertex left out.

These facts underlie the resolution lower bounds for Tseitin formulas (Cslib.Logic.PL.Tseitin.minBalancedCut_le_of_refutableInWidth, Cslib.Logic.PL.Tseitin.exp_le_of_refutableInSize).

Main definitions #

Main results #

References #

Parities at the vertices #

source
theorem Cslib.Logic.PL.Tseitin.parityOn_incidence_update_not {V : Type u_1} {E : Type u_2} {ends : E → Sym2 V} [Fintype E] [DecidableEq V] [DecidableEq E] (σ : E → Bool) (e : E) (v : V) :
parityOn (Multigraph.incidence ends v) (Function.update σ e !σ e) = (decide (e ∈ Multigraph.incidence ends v) ^^ parityOn (Multigraph.incidence ends v) σ)

Flipping the value of an edge flips the parities at its ends, and only there.

source
theorem Cslib.Logic.PL.Tseitin.exists_forall_parityOn_incidence_eq_xor {V : Type u_1} {E : Type u_2} {ends : E → Sym2 V} [Fintype E] [DecidableEq V] [Finite V] (hG : (Multigraph.toSimpleGraph ends).Connected) (u w : V) :
∃ (τ : E → Bool), ∀ (v : V), parityOn (Multigraph.incidence ends v) τ = (decide (v = u) ^^ decide (v = w))

On a connected multigraph, the parities at any two vertices u and w, and nowhere else, can be flipped: some assignment has parity 1 exactly at u and w (and nowhere if u = w).

source
theorem Cslib.Logic.PL.Tseitin.parityOn_univ_parityOn_incidence_eq_false {V : Type u_1} {E : Type u_2} {ends : E → Sym2 V} [Fintype E] [DecidableEq V] [Fintype V] (σ : E → Bool) :
(parityOn Finset.univ fun (v : V) => parityOn (Multigraph.incidence ends v) σ) = false

The handshake argument: the parities at all vertices of an assignment to the edges add up to 0, since every edge other than a self-loop is at exactly two vertices.

source
theorem Cslib.Logic.PL.Tseitin.parityOn_univ_eq_false_of_forall {V : Type u_1} {E : Type u_2} {ends : E → Sym2 V} [Fintype E] [DecidableEq V] [Fintype V] {σ : E → Bool} {χ : V → Bool} (h : ∀ (v : V), parityOn (Multigraph.incidence ends v) σ = χ v) :
parityOn Finset.univ χ = false

An assignment satisfying the constraints of all vertices has even total charge.

source
theorem Cslib.Logic.PL.Tseitin.exists_forall_parityOn_incidence_eq {V : Type u_1} {E : Type u_2} {ends : E → Sym2 V} [Fintype E] [DecidableEq V] [Fintype V] (hG : (Multigraph.toSimpleGraph ends).Connected) (χ : V → Bool) (u : V) :
∃ (σ : E → Bool), ∀ (v : V), parityOn (Multigraph.incidence ends v) σ = (parityOn Finset.univ χ && decide (v = u) ^^ χ v)

On a connected multigraph, for every vertex u some assignment satisfies the constraints of all vertices except possibly u: its parity at v is χ v, flipped at u when the total charge is odd.

source
theorem Cslib.Logic.PL.Tseitin.exists_forall_mem_parityOn_incidence_eq {V : Type u_1} {E : Type u_2} {ends : E → Sym2 V} [Fintype E] [DecidableEq V] [Fintype V] (hG : (Multigraph.toSimpleGraph ends).Connected) (χ : V → Bool) {S : Finset V} (hS : S ≠ Finset.univ) :
∃ (σ : E → Bool), ∀ v ∈ S, parityOn (Multigraph.incidence ends v) σ = χ v

Satisfiable subsystems: on a connected multigraph, the constraints of the vertices of any set other than the set of all vertices are satisfiable, whatever the charges.

Tseitin formulas #

source
noncomputable def Cslib.Logic.PL.CNF.tseitinFormula {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [Fintype E] [DecidableEq E] (ends : E → Sym2 V) (χ : V → Bool) :
CNF E

The Tseitin formula of the multigraph ends with charges χ Tseitin Urquhart: a variable for each edge, and for each vertex v the clauses of CNF.parityOnEq saying that the parity of the edges at v other than self-loops is χ v.

Instances For
    source
    theorem Cslib.Logic.PL.CNF.mem_tseitinFormula {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [Fintype E] [DecidableEq E] {ends : E → Sym2 V} {χ : V → Bool} {c : Clause E} :
    c ∈ tseitinFormula ends χ ↔ ∃ (v : V), c ∈ parityOnEq (Multigraph.incidence ends v) (χ v)

    A clause belongs to tseitinFormula ends χ iff it belongs to the parity constraint parityOnEq (Multigraph.incidence ends v) (χ v) of some vertex v.

    source
    theorem Cslib.Logic.PL.CNF.eval_tseitinFormula_eq_true_iff {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [Fintype E] [DecidableEq E] {ends : E → Sym2 V} {χ : V → Bool} (σ : E → Bool) :
    eval σ (tseitinFormula ends χ) = true ↔ ∀ (v : V), parityOn (Multigraph.incidence ends v) σ = χ v

    An assignment satisfies the Tseitin formula when its parity at every vertex is the charge.

    source
    theorem Cslib.Logic.PL.CNF.not_satisfiable_tseitinFormula {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [Fintype E] [DecidableEq E] {ends : E → Sym2 V} {χ : V → Bool} (h : parityOn Finset.univ χ = true) :
    ¬(tseitinFormula ends χ).Satisfiable

    Tseitin formulas with odd total charge are unsatisfiable Urquhart.

    source
    theorem Cslib.Logic.PL.CNF.satisfiable_tseitinFormula_iff {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [Fintype E] [DecidableEq E] {ends : E → Sym2 V} {χ : V → Bool} (hG : (Multigraph.toSimpleGraph ends).Connected) :
    (tseitinFormula ends χ).Satisfiable ↔ parityOn Finset.univ χ = false

    On a connected multigraph, the Tseitin formula is satisfiable exactly when the total charge is even Urquhart.

    source
    theorem Cslib.Logic.PL.CNF.length_le_of_mem_tseitinFormula {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [Fintype E] [DecidableEq E] {ends : E → Sym2 V} {χ : V → Bool} {k : ℕ} (hk : ∀ (v : V), (Multigraph.incidence ends v).card ≤ k) {c : Clause E} (hc : c ∈ tseitinFormula ends χ) :
    List.length c ≤ k

    If every vertex has at most k edges other than self-loops, the clauses of the Tseitin formula have at most k literals.

    source
    theorem Cslib.Logic.PL.CNF.length_tseitinFormula_le {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [Fintype E] [DecidableEq E] {ends : E → Sym2 V} {χ : V → Bool} {k : ℕ} (hk : ∀ (v : V), (Multigraph.incidence ends v).card ≤ k) :
    List.length (tseitinFormula ends χ) ≤ Fintype.card V * 2 ^ k

    If every vertex has at most k edges other than self-loops, the Tseitin formula has at most |V| 2 ^ k clauses.

    source
    theorem Cslib.Logic.PL.CNF.card_toFinset_vars_tseitinFormula_le {V : Type u_1} {E : Type u_2} [Fintype V] [DecidableEq V] [Fintype E] [DecidableEq E] {ends : E → Sym2 V} {χ : V → Bool} :
    (tseitinFormula ends χ).vars.toFinset.card ≤ Fintype.card E

    The variables of a Tseitin formula are edges.