Constraint networks and the cut-counting lemma

A Network is a multigraph whose vertices carry local checks on the bits written on their incident edges, together with a port for each input variable read by the network: a vertex and an incident edge that must carry the variable's value. The network computes f when the accepted inputs are exactly those for which some edge assignment satisfies every check and every port.

For a vertex ordering, the bits on a prefix cut summarize what the processed part of the network remembers. The past assignments consistent with a cut assignment and the future assignments consistent with it form a one-rectangle of f (accepted_of_mem_pastSet_of_mem_futureSet). Charging every accepted input to the first vertex at which its past set becomes large, the cut-counting lemma card_accepting_le bounds the number of accepted inputs of a K-rectangle-free function by |V| · 2 ^ (w + 3) · (K - 1) ^ 2, where w bounds every prefix cut and each vertex has at most three incident edges.

structure Algebraic.Cutwidth.Network (n : ℕ) (V E : Type) extends Algebraic.Cutwidth.Multigraph V E : Type

A constraint network over n input variables: a multigraph with a local check at every vertex and a port for every variable it reads.

• fst : E → V
• snd : E → V
• Check : V → (E → Bool) → Prop

  The local check of a vertex on an assignment of bits to edges.

• check_local (v : V) (α β : E → Bool) : (∀ (e : E), self.fst e = v ∨ self.snd e = v → α e = β e) → self.Check v α → self.Check v β

  A check depends only on the bits of the incident edges.

• read : Finset (Fin n)

  The variables read by the network.

• portVertex : Fin n → V

  The vertex at which a variable is read. Irrelevant outside read.

• portEdge : Fin n → E

  The edge carrying a variable's value. Irrelevant outside read.

• port_incident (j : Fin n) : j ∈ self.read → self.fst (self.portEdge j) = self.portVertex j ∨ self.snd (self.portEdge j) = self.portVertex j

  The port edge of a read variable is incident to its port vertex.

def Algebraic.Cutwidth.Network.Satisfies {n : ℕ} {V E : Type} (N : Network n V E) (x : Fin n → Bool) (α : E → Bool) : Prop

An edge assignment satisfies every check and carries the input on every port.

Equations

• N.Satisfies x α = ((∀ (v : V), N.Check v α) ∧ ∀ j ∈ N.read, α (N.portEdge j) = x j)

def Algebraic.Cutwidth.Network.Computes {n : ℕ} {V E : Type} (N : Network n V E) (f : Cslib.BooleanFunction n) : Prop

The accepted inputs are those with a satisfying edge assignment.

Equations

• N.Computes f = ∀ (x : Cslib.BitString n), f x = true ↔ ∃ (α : E → Bool), N.Satisfies x α

theorem Algebraic.Cutwidth.Network.Computes.dependsOnlyOn {n : ℕ} {V E : Type} (N : Network n V E) {f : Cslib.BooleanFunction n} (h : N.Computes f) : DependsOnlyOn f N.read

A computed function depends only on the variables the network reads.

noncomputable def Algebraic.Cutwidth.Network.past {n : ℕ} {V E : Type} (N : Network n V E) (L : Finset V) : Finset (Fin n)

The variables read at a vertex of L.

Equations

• N.past L = {j ∈ N.read | N.portVertex j ∈ L}

theorem Algebraic.Cutwidth.Network.mem_past {n : ℕ} {V E : Type} (N : Network n V E) {L : Finset V} {j : Fin n} : j ∈ N.past L ↔ j ∈ N.read ∧ N.portVertex j ∈ L

@[simp]

theorem Algebraic.Cutwidth.Network.past_empty {n : ℕ} {V E : Type} (N : Network n V E) : N.past ∅ = ∅

@[simp]

theorem Algebraic.Cutwidth.Network.past_univ {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] : N.past Finset.univ = N.read

noncomputable def Algebraic.Cutwidth.Network.pastSet {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] (L : Finset V) (σ : E → Bool) : Finset (↥(N.past L) → Bool)

The past assignments consistent with a cut assignment: assignments to the variables read in L extended by an edge assignment satisfying the checks of L and agreeing with σ on the cut.

Equations

• N.pastSet L σ = {p : ↥(N.past L) → Bool | ∃ (α : E → Bool), (∀ v ∈ L, N.Check v α) ∧ (∀ e ∈ N.cut L, α e = σ e) ∧ ∀ (j : ↥(N.past L)), α (N.portEdge ↑j) = p j}

noncomputable def Algebraic.Cutwidth.Network.futureSet {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] (L : Finset V) (σ : E → Bool) : Finset (↥(N.past L)ᶜ → Bool)

The future assignments consistent with a cut assignment: assignments to the remaining variables extended by an edge assignment satisfying the checks outside L, agreeing with σ on the cut, and carrying the read variables.

Equations

• N.futureSet L σ = {q : ↥(N.past L)ᶜ → Bool | ∃ (β : E → Bool), (∀ v ∉ L, N.Check v β) ∧ (∀ e ∈ N.cut L, β e = σ e) ∧ ∀ (j : ↥(N.past L)ᶜ), ↑j ∈ N.read → β (N.portEdge ↑j) = q j}

theorem Algebraic.Cutwidth.Network.mem_pastSet {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] {L : Finset V} {σ : E → Bool} {p : ↥(N.past L) → Bool} : p ∈ N.pastSet L σ ↔ ∃ (α : E → Bool), (∀ v ∈ L, N.Check v α) ∧ (∀ e ∈ N.cut L, α e = σ e) ∧ ∀ (j : ↥(N.past L)), α (N.portEdge ↑j) = p j

theorem Algebraic.Cutwidth.Network.mem_futureSet {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] {L : Finset V} {σ : E → Bool} {q : ↥(N.past L)ᶜ → Bool} : q ∈ N.futureSet L σ ↔ ∃ (β : E → Bool), (∀ v ∉ L, N.Check v β) ∧ (∀ e ∈ N.cut L, β e = σ e) ∧ ∀ (j : ↥(N.past L)ᶜ), ↑j ∈ N.read → β (N.portEdge ↑j) = q j

theorem Algebraic.Cutwidth.Network.pastSet_congr {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] {L : Finset V} {σ σ' : E → Bool} (h : ∀ e ∈ N.cut L, σ e = σ' e) : N.pastSet L σ = N.pastSet L σ'

The past set depends on the cut assignment only through the cut.

theorem Algebraic.Cutwidth.Network.futureSet_congr {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] {L : Finset V} {σ σ' : E → Bool} (h : ∀ e ∈ N.cut L, σ e = σ' e) : N.futureSet L σ = N.futureSet L σ'

The future set depends on the cut assignment only through the cut.

theorem Algebraic.Cutwidth.Network.restrict_mem_pastSet {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] {x : Fin n → Bool} {α : E → Bool} (h : N.Satisfies x α) (L : Finset V) : (fun (j : ↥(N.past L)) => x ↑j) ∈ N.pastSet L α

The past of an accepted input lies in the past set of its own assignment.

theorem Algebraic.Cutwidth.Network.restrict_mem_futureSet {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] {x : Fin n → Bool} {α : E → Bool} (h : N.Satisfies x α) (L : Finset V) : (fun (j : ↥(N.past L)ᶜ) => x ↑j) ∈ N.futureSet L α

The future of an accepted input lies in the future set of its own assignment.

theorem Algebraic.Cutwidth.Network.card_pastSet_empty_le {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] (σ : E → Bool) : (N.pastSet ∅ σ).card ≤ 1

Before any vertex is processed, only the empty past assignment exists.

theorem Algebraic.Cutwidth.Network.accepted_of_mem_pastSet_of_mem_futureSet {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] {f : Cslib.BooleanFunction n} (hf : N.Computes f) {L : Finset V} {σ : E → Bool} {p : ↥(N.past L) → Bool} (hp : p ∈ N.pastSet L σ) {q : ↥(N.past L)ᶜ → Bool} (hq : q ∈ N.futureSet L σ) : f (glue (N.past L) p q) = true

A consistent past and future together form an accepted input: the past and future sets of a cut assignment form a one-rectangle.

theorem Algebraic.Cutwidth.Network.card_accepting_lt_of_card_pastSet_univ_lt {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] {f : Cslib.BooleanFunction n} (hf : N.Computes f) {K : ℕ} (small : (N.pastSet Finset.univ fun (x : E) => false).card < K) : (accepting f).card < K * 2 ^ (n - N.read.card)

Every accepted input restricts into a fixed past set of the whole vertex set, so a small final past set forces few accepted inputs.

noncomputable def Algebraic.Cutwidth.Network.below {V : Type} [Fintype V] [LinearOrder V] (v : V) : Finset V

The vertices strictly before v.

Equations

• Algebraic.Cutwidth.Network.below v = {u : V | u < v}

noncomputable def Algebraic.Cutwidth.Network.upto {V : Type} [Fintype V] [LinearOrder V] (v : V) : Finset V

The vertices up to and including v.

Equations

• Algebraic.Cutwidth.Network.upto v = {u : V | u ≤ v}

theorem Algebraic.Cutwidth.Network.mem_below {V : Type} [Fintype V] [LinearOrder V] {u v : V} : u ∈ below v ↔ u < v

theorem Algebraic.Cutwidth.Network.mem_upto {V : Type} [Fintype V] [LinearOrder V] {u v : V} : u ∈ upto v ↔ u ≤ v

theorem Algebraic.Cutwidth.Network.isLowerSet_below {V : Type} [Fintype V] [LinearOrder V] (v : V) : IsLowerSet ↑(below v)

theorem Algebraic.Cutwidth.Network.isLowerSet_upto {V : Type} [Fintype V] [LinearOrder V] (v : V) : IsLowerSet ↑(upto v)

theorem Algebraic.Cutwidth.Network.upto_max' {V : Type} [Fintype V] [LinearOrder V] (h : Finset.univ.Nonempty) : upto (Finset.univ.max' h) = Finset.univ

The prefix through the last vertex is everything.

theorem Algebraic.Cutwidth.Network.below_eq_empty_or_exists_upto {V : Type} [Fintype V] [LinearOrder V] (v : V) : below v = ∅ ∨ ∃ u < v, below v = upto u

The vertices before v are empty or the prefix through an earlier vertex.

theorem Algebraic.Cutwidth.Network.cut_upto_subset {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] [LinearOrder V] (v : V) : N.cut (upto v) ⊆ N.cut (below v) ∪ N.edgesAt v

Processing one vertex changes the cut only among its incident edges.

theorem Algebraic.Cutwidth.Network.card_accepting_le {n : ℕ} {V E : Type} (N : Network n V E) [Fintype V] [Fintype E] [LinearOrder V] [Nonempty V] {f : Cslib.BooleanFunction n} (hf : N.Computes f) (hdeg : N.MaxDegreeLE 3) {w : ℕ} (hw : ∀ (v : V), (N.cut (below v)).card ≤ w) {K : ℕ} (hK : 1 < K) (hrect : RectangleFree f K) : (accepting f).card < K * 2 ^ (n - N.read.card) ∨ (accepting f).card ≤ Fintype.card V * 2 ^ (w + 3) * (K - 1) ^ 2

The cut-counting lemma. For a network computing a K-rectangle-free function, with every vertex of degree at most three and every prefix cut of the ordering of size at most w, either the final past set is small, so that fewer than K · 2 ^ (n - |read|) inputs are accepted, or at most |V| · 2 ^ (w + 3) · (K - 1) ^ 2 inputs are accepted.