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_of_realized bounds the number of
accepted inputs of a K-rectangle-free function by |V| · P · (K - 1) ^ 2,
where P bounds the number of bit patterns that satisfying assignments
realize on the cut before a vertex together with its incident edges
(realized). A subset of those edges that determines the rest under every
satisfying assignment (Determines) bounds the patterns by a power of two
(card_realized_le_of_determines). Taking all edges, the classical form
card_accepting_le charges 2 ^ (w + 3), where w bounds every prefix cut
and each vertex has at most three incident edges.
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
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.
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.
Instances For
The accepted inputs are those with a satisfying edge assignment.
Instances For
A computed function depends only on the variables the network reads.
T determines C: two satisfying assignments that agree on T agree on C.
Equations
Instances For
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
Instances For
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
Instances For
A consistent past and future together form an accepted input: the past and future sets of a cut assignment form a one-rectangle.
Every accepted input restricts into a fixed past set of the whole vertex set, so a small final past set forces few accepted inputs.
Realized patterns #
A determining subset of C bounds the patterns realized on C: restriction
to T is injective on them.
The vertices strictly before v.
Equations
- Algebraic.Cutwidth.Network.below v = {u : V | u < v}
Instances For
The vertices up to and including v.
Equations
- Algebraic.Cutwidth.Network.upto v = {u : V | u ≤ v}
Instances For
The prefix through the last vertex is everything.
The edges charged at a vertex: the cut before it and its incident edges.
Instances For
With prefix cuts of size at most w and degrees at most three, at most
w + 3 edges are charged at any vertex.
The cut-counting lemma, charged by realized patterns. For a network
computing a K-rectangle-free function and a vertex ordering, suppose that
satisfying assignments realize at most P bit patterns on the cut before any
vertex together with that vertex's incident edges. Then either the final past
set is small, so that fewer than K · 2 ^ (n - |read|) inputs are accepted, or
at most |V| · P · (K - 1) ^ 2 inputs are accepted.
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.