Constraint networks and their sweeps

A constraint network is a multigraph whose edges carry values in an alphabet U and whose vertices impose local constraints: the constraint at v sees only the values on the edges at v and the inputs read at v. Each input is read at no more than one vertex. An input is accepted when some assignment of values to the edges satisfies every constraint.

Networks are a semantics-free form of computation. Nothing in them is directed: a gate z = g(x, y) becomes the relation {(x, y, z) | z = g(x, y)} between three edge values, and the network never needs to invert g.

The separator lemma (Network.Satisfies.splice). Cut the vertices into a set L and its complement. If two satisfying assignments, for inputs x and y, agree on the cut, then taking the first assignment near L and the second away from it satisfies the network for the input that reads like x at L and like y elsewhere. Once the values on the cut are fixed, the two sides of the network are independent.

Sweeping a network. Process the vertices in the order of a layout. At time t the inputs read by the first t vertices are revealed, and the message is the list of values on the frontier, the cut after the first t vertices (Network.sweep). By the separator lemma this is a sweep of the accepted set. A transition is determined by the values on two consecutive frontiers and the inputs read at the vertex processed in between, so a layout of width w in a network of degree at most d, reading at most m inputs per vertex, yields at most |U| ^ (w + d + m) transitions per step (Network.ncard_accepted_le). One last step reveals the inputs that the network does not read.

Main definitions

• Frontier.Network U ι V E: a constraint network.
• Frontier.Network.accepted: its accepted inputs.
• Frontier.Network.sweep: the sweep of the accepted set along a layout.

Main results

• Frontier.Network.Satisfies.splice: the separator lemma.
• Frontier.Network.dependsOn_read: acceptance depends only on the inputs read.
• Frontier.Network.ncard_accepted_le: the frontier counting lemma for networks.

structure Complexity.Frontier.Network (U : Type u_1) (ι : Type u_2) (V : Type u_3) (E : Type u_4) extends Complexity.Frontier.Multigraph V E : Type (max (max (max u_1 u_2) u_3) u_4)

A constraint network over the alphabet U with inputs indexed by ι: a multigraph on vertices V and edges E, the vertex at which each input is read (if any), and a constraint at each vertex that sees only the edges at that vertex and the inputs read there.

• src : E → V
• tgt : E → V
• site : ι → Option V

  The vertex at which each input is read, if it is read at all.

• Check : V → (ι → U) → (E → U) → Prop

  The constraint at a vertex, on the input and the values on the edges.

• check_local (v : V) (x x' : ι → U) (α α' : E → U) : (∀ (i : ι), self.site i = some v → x i = x' i) → (∀ (e : E), self.src e = v ∨ self.tgt e = v → α e = α' e) → self.Check v x α → self.Check v x' α'

  Constraints are local: the constraint at v sees only the inputs read at v and the values on the edges incident to v.

def Complexity.Frontier.Network.Satisfies {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) (x : ι → U) (α : E → U) : Prop

An assignment of values to the edges satisfies every constraint on the input x.

Equations

• N.Satisfies x α = ∀ (v : V), N.Check v x α

def Complexity.Frontier.Network.accepted {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) : Set (ι → U)

The accepted inputs: those with a satisfying assignment.

Equations

• N.accepted = {x : ι → U | ∃ (α : E → U), N.Satisfies x α}

def Complexity.Frontier.Network.readAt {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) (v : V) : Set ι

The inputs read at a vertex.

Equations

• N.readAt v = {i : ι | N.site i = some v}

def Complexity.Frontier.Network.readIn {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) (L : Set V) : Set ι

The inputs read at the vertices of L.

Equations

• N.readIn L = {i : ι | ∃ v ∈ L, N.site i = some v}

def Complexity.Frontier.Network.read {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) : Set ι

The inputs read by the network.

Equations

• N.read = N.readIn Set.univ

@[simp]

theorem Complexity.Frontier.Network.readIn_empty {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) : N.readIn ∅ = ∅

theorem Complexity.Frontier.Network.Satisfies.splice {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} {N : Network U ι V E} {L : Set V} {x y z : ι → U} {α β : E → U} (hx : N.Satisfies x α) (hy : N.Satisfies y β) (hcut : Set.EqOn α β (N.cut L)) (hzx : Set.EqOn z x (N.readIn L)) (hzy : Set.EqOn z y (N.readIn L)ᶜ) : ∃ (γ : E → U), N.Satisfies z γ ∧ Set.EqOn γ α (N.touching L) ∧ Set.EqOn γ β (N.touching L)ᶜ

The separator lemma. Let α satisfy the network on the input x and β on the input y, and suppose that they agree on the cut of L. Then the network is satisfied on any input z that agrees with x on the inputs read in L and with y on the others, by an assignment that agrees with α on the edges touching L and with β on the remaining edges.

theorem Complexity.Frontier.Network.dependsOn_read {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) : DependsOn (fun (x : ι → U) => x ∈ N.accepted) N.read

Acceptance depends only on the inputs that the network reads.

Sweeping along a layout

def Complexity.Frontier.Network.frontier {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) (π : Layout V) (t : ℕ) : Set E

The frontier at time t: the cut after the first t vertices of the layout.

Equations

• N.frontier π t = N.cut (π.initial t)

noncomputable def Complexity.Frontier.Network.frontierValues {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) (π : Layout V) (t : ℕ) (α : E → U) : E → Option U

The values of an assignment on the frontier at time t, and nothing elsewhere.

Equations

• N.frontierValues π t α e = if e ∈ N.frontier π t then some (α e) else none

theorem Complexity.Frontier.Network.frontierValues_eq_iff {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) (π : Layout V) {t : ℕ} {α β : E → U} : N.frontierValues π t α = N.frontierValues π t β ↔ Set.EqOn α β (N.frontier π t)

def Complexity.Frontier.Network.revealedBy {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) (π : Layout V) (t : ℕ) : Set ι

The inputs revealed by time t: those read by the first t vertices, and after the last vertex, all inputs, including those the network does not read.

Equations

• N.revealedBy π t = if t ≤ Nat.card V then N.readIn (π.initial t) else Set.univ

noncomputable def Complexity.Frontier.Network.frontierSweep {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) (π : Layout V) {S : Set (ι → U)} {R : Type u_5} (val : (ι → U) → E → U) (extra : ℕ → (ι → U) → R) (hlast : ∀ x ∈ S, ∀ y ∈ S, extra (Nat.card V + 1) x = extra (Nat.card V + 1) y) (hsplice : ∀ t ≤ Nat.card V, ∀ x ∈ S, ∀ y ∈ S, extra t x = extra t y → Set.EqOn (val x) (val y) (N.frontier π t) → ∀ (z : ι → U), Set.EqOn z x (N.readIn (π.initial t)) → Set.EqOn z y (N.readIn (π.initial t))ᶜ → z ∈ S) : Sweep S (R × (E → Option U))

Sweeping along a layout. Fix values val x on the edges for every input x, and an extra message extra t x at every time. The messages (extra t x, val x on the frontier at time t) form a sweep of S as soon as inputs of S with the same message splice.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.Frontier.Network.newly_subset_readAt {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) {π : Layout V} {S : Set (ι → U)} {R : Type u_5} {val : (ι → U) → E → U} {extra : ℕ → (ι → U) → R} {hlast : ∀ x ∈ S, ∀ y ∈ S, extra (Nat.card V + 1) x = extra (Nat.card V + 1) y} {hsplice : ∀ t ≤ Nat.card V, ∀ x ∈ S, ∀ y ∈ S, extra t x = extra t y → Set.EqOn (val x) (val y) (N.frontier π t) → ∀ (z : ι → U), Set.EqOn z x (N.readIn (π.initial t)) → Set.EqOn z y (N.readIn (π.initial t))ᶜ → z ∈ S} {t : ℕ} (ht : t < Nat.card V) : (N.frontierSweep π val extra hlast hsplice).newly t ⊆ N.readAt ((Equiv.symm π) ⟨t, ht⟩)

The inputs revealed while processing the vertex numbered t are read at that vertex.

theorem Complexity.Frontier.Network.ncard_transition_le {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) {π : Layout V} {S : Set (ι → U)} {R : Type u_5} {val : (ι → U) → E → U} {extra : ℕ → (ι → U) → R} {hlast : ∀ x ∈ S, ∀ y ∈ S, extra (Nat.card V + 1) x = extra (Nat.card V + 1) y} {hsplice : ∀ t ≤ Nat.card V, ∀ x ∈ S, ∀ y ∈ S, extra t x = extra t y → Set.EqOn (val x) (val y) (N.frontier π t) → ∀ (z : ι → U), Set.EqOn z x (N.readIn (π.initial t)) → Set.EqOn z y (N.readIn (π.initial t))ᶜ → z ∈ S} [Finite ι] [Finite U] [Finite E] {t : ℕ} (ht : t < Nat.card V) : ((N.frontierSweep π val extra hlast hsplice).transition t '' S).ncard ≤ ((fun (x : ι → U) => (extra t x, extra (t + 1) x)) '' S).ncard * Nat.card U ^ ((N.frontier π t ∪ N.frontier π (t + 1)).ncard + (N.readAt ((Equiv.symm π) ⟨t, ht⟩)).ncard)

Transitions by width. At a step that processes a vertex, the transition is determined by the extra messages, the values on the two frontiers, and the inputs read at the vertex.

theorem Complexity.Frontier.Network.ncard_transition_le_labels {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) {π : Layout V} {S : Set (ι → U)} {R : Type u_5} {val : (ι → U) → E → U} {extra : ℕ → (ι → U) → R} {hlast : ∀ x ∈ S, ∀ y ∈ S, extra (Nat.card V + 1) x = extra (Nat.card V + 1) y} {hsplice : ∀ t ≤ Nat.card V, ∀ x ∈ S, ∀ y ∈ S, extra t x = extra t y → Set.EqOn (val x) (val y) (N.frontier π t) → ∀ (z : ι → U), Set.EqOn z x (N.readIn (π.initial t)) → Set.EqOn z y (N.readIn (π.initial t))ᶜ → z ∈ S} [Finite ι] [Finite U] {Λ : Type u_6} [Finite Λ] (label : E → Λ) (value : (ι → U) → Λ → U) (hval : ∀ x ∈ S, ∀ (e : E), val x e = value x (label e)) {t : ℕ} (ht : t < Nat.card V) : ((N.frontierSweep π val extra hlast hsplice).transition t '' S).ncard ≤ ((fun (x : ι → U) => (extra t x, extra (t + 1) x)) '' S).ncard * Nat.card U ^ ((label '' (N.frontier π t ∪ N.frontier π (t + 1))).ncard + (N.readAt ((Equiv.symm π) ⟨t, ht⟩)).ncard)

Transitions by distinct labels. If edges with the same label carry the same value, charge a label only once across the union of the adjacent frontiers.

theorem Complexity.Frontier.Network.ncard_transition_le_of_touching {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) {π : Layout V} {S : Set (ι → U)} {R : Type u_5} {val : (ι → U) → E → U} {extra : ℕ → (ι → U) → R} {hlast : ∀ x ∈ S, ∀ y ∈ S, extra (Nat.card V + 1) x = extra (Nat.card V + 1) y} {hsplice : ∀ t ≤ Nat.card V, ∀ x ∈ S, ∀ y ∈ S, extra t x = extra t y → Set.EqOn (val x) (val y) (N.frontier π t) → ∀ (z : ι → U), Set.EqOn z x (N.readIn (π.initial t)) → Set.EqOn z y (N.readIn (π.initial t))ᶜ → z ∈ S} [Finite ι] [Finite U] {t : ℕ} (ht : t < Nat.card V) {W : Set V} (hv : (Equiv.symm π) ⟨t, ht⟩ ∈ W) (hC : N.frontier π t ∪ N.frontier π (t + 1) ⊆ N.touching W) (hdet : ∀ x ∈ S, ∀ y ∈ S, extra t x = extra t y → extra (t + 1) x = extra (t + 1) y → Set.EqOn x y (N.readIn W) → Set.EqOn (val x) (val y) (N.touching W)) : ((N.frontierSweep π val extra hlast hsplice).transition t '' S).ncard ≤ ((fun (x : ι → U) => (extra t x, extra (t + 1) x)) '' S).ncard * Nat.card U ^ (N.readIn W).ncard

Transitions inside a closed set. If the vertex processed lies in W, both frontiers lie among the edges at W, and the values on the edges at W are determined by the extra messages and the inputs read in W, then so is the transition.

theorem Complexity.Frontier.Network.ncard_transition_last_le {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) {π : Layout V} {S : Set (ι → U)} {R : Type u_5} {val : (ι → U) → E → U} {extra : ℕ → (ι → U) → R} {hlast : ∀ x ∈ S, ∀ y ∈ S, extra (Nat.card V + 1) x = extra (Nat.card V + 1) y} {hsplice : ∀ t ≤ Nat.card V, ∀ x ∈ S, ∀ y ∈ S, extra t x = extra t y → Set.EqOn (val x) (val y) (N.frontier π t) → ∀ (z : ι → U), Set.EqOn z x (N.readIn (π.initial t)) → Set.EqOn z y (N.readIn (π.initial t))ᶜ → z ∈ S} [Finite ι] [Finite U] : ((N.frontierSweep π val extra hlast hsplice).transition (Nat.card V) '' S).ncard ≤ ((fun (x : ι → U) => (extra (Nat.card V) x, extra (Nat.card V + 1) x)) '' S).ncard * Nat.card U ^ N.readᶜ.ncard

At the last step nothing is left on the frontier, and the transition is determined by the extra messages and the inputs that the network does not read.

The sweep of a network

noncomputable def Complexity.Frontier.Network.witness {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) [Nonempty U] (x : ι → U) : E → U

A satisfying assignment for an accepted input, chosen once and for all.

Equations

• N.witness x = Classical.epsilon (N.Satisfies x)

theorem Complexity.Frontier.Network.satisfies_witness {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) [Nonempty U] {x : ι → U} (hx : x ∈ N.accepted) : N.Satisfies x (N.witness x)

noncomputable def Complexity.Frontier.Network.sweep {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) (π : Layout V) [Nonempty U] : Sweep N.accepted (Unit × (E → Option U))

The sweep of a network along a layout: the messages are the values of a satisfying assignment on the frontier, and splicing is the separator lemma.

Equations

• N.sweep π = N.frontierSweep π N.witness (fun (x : ℕ) (x_1 : ι → U) => ()) ⋯ ⋯

theorem Complexity.Frontier.Network.ncard_accepted_le {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) (π : Layout V) [Nonempty U] [Finite ι] [Finite U] [Finite E] {K : ℕ} (hfree : RectangleFree N.accepted K) (hK : K ≤ N.accepted.ncard) {w d m : ℕ} (hw : ∀ (t : ℕ), (N.frontier π t).ncard ≤ w) (hd : N.MaxDegreeLE d) (hm : ∀ (v : V), (N.readAt v).ncard ≤ m) : N.accepted.ncard ≤ (K - 1) ^ 2 * (Nat.card V * Nat.card U ^ (w + d + m) + Nat.card U ^ N.readᶜ.ncard)

The frontier counting lemma for networks. Let the accepted inputs of a network be K-rectangle-free, with at least K of them. If a layout has all frontiers of size at most w, every vertex has degree at most d and reads at most m inputs, then

|accepted| ≤ (K - 1) ^ 2 · (|V| · |U| ^ (w + d + m) + |U| ^ #(unread inputs)).

theorem Complexity.Frontier.Network.ncard_accepted_le_labels {U : Type u_1} {ι : Type u_2} {V : Type u_3} {E : Type u_4} (N : Network U ι V E) (π : Layout V) [Nonempty U] [Finite ι] [Finite U] {Λ : Type u_6} [Finite Λ] (label : E → Λ) (value : (ι → U) → Λ → U) (hval : ∀ x ∈ N.accepted, ∀ (e : E), N.witness x e = value x (label e)) {K b : ℕ} (hfree : RectangleFree N.accepted K) (hK : K ≤ N.accepted.ncard) (hb : ∀ (t : ℕ) (ht : t < Nat.card V), (label '' (N.frontier π t ∪ N.frontier π (t + 1))).ncard + (N.readAt ((Equiv.symm π) ⟨t, ht⟩)).ncard ≤ b) : N.accepted.ncard ≤ (K - 1) ^ 2 * (Nat.card V * Nat.card U ^ b + Nat.card U ^ N.readᶜ.ncard)

A label budget on adjacent frontiers bounds the accepted set without charging repeated copies of a label. This includes the inputs read during the step in the budget b.