Constraint networks and their branching programs #
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 edge cut of L,
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.
The branching program of a layout (Network.branchingProgram). Process the vertices in the
order of a layout. Layer t of the program is the frontier after the first t vertices, the
edge cut between them and the rest, and its states are the values on the frontier. Step t
processes the vertex v numbered t and reads the inputs read at v; its edges join the values
of an assignment on the frontier before v to its values on the frontier after v when the
constraint at v holds. One last step reads the inputs that the network does not read, so the
program reads every input exactly once.
Exactness (Network.accepted_branchingProgram). The frontier values of a satisfying
assignment form an accepting path. Conversely, along an accepting path the value on an edge
persists while the edge stays on the frontier, so the assignments witnessing the steps agree on
every edge and glue into a satisfying assignment (Network.exists_satisfies_of_isAcceptingPath).
If satisfying assignments are unique, the program is unambiguous.
Counting edges. An edge of the program at step t 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, gives a
program with at most |U| ^ (w + d + m) edges at each of its first |V| steps. Its final step
has at most |U| ^ #(unread inputs) edges (Network.size_branchingProgram_le), and the rectangle
bound for read-once programs bounds the accepted set (Network.ncard_accepted_le); peeling bounds
the bias of a set on it (Network.abs_signedCount_accepted_le).
Sweeps with extra messages (Network.frontierSweep). Any values val x on the edges, not
necessarily satisfying, together with an extra message at each time, form a sweep as soon as
the inputs sending the same messages splice. This is how a global register, such as a ledger,
travels along a layout next to the values on the frontier.
Main definitions #
Cslib.Circuits.Frontier.Network U ι V E: a constraint network.Cslib.Circuits.Frontier.Network.accepted: its accepted inputs.Cslib.Circuits.Frontier.Network.branchingProgram: the read-once branching program of a layout.Cslib.Circuits.Frontier.Network.frontierSweep: frontier values and extra messages along a layout, as a sweep.
Main results #
Cslib.Circuits.Frontier.Network.Satisfies.splice: the separator lemma.Cslib.Circuits.Frontier.Network.dependsOn_read: acceptance depends only on the inputs read.Cslib.Circuits.Frontier.Network.readIn_insert_subset: inserting one vertex adds only its reads.Cslib.Circuits.Frontier.Network.exists_ncard_readIn_initial_eq: read counts reach every intermediate value when each vertex reads at most one input.Cslib.Circuits.Frontier.Network.ncard_image_path_le: states at a layer are bounded by the number of assignments on its frontier.Cslib.Circuits.Frontier.Network.accepted_branchingProgram: the branching program of a layout accepts exactly the accepted inputs.Cslib.Circuits.Frontier.Network.unambiguous_branchingProgram: it is unambiguous when satisfying assignments are unique.Cslib.Circuits.Frontier.Network.size_branchingProgram_le: its size, by the width.Cslib.Circuits.Frontier.Network.ncard_accepted_le: the frontier counting lemma for networks.Cslib.Circuits.Frontier.Network.abs_signedCount_accepted_le: its peeling form, for biased sets.
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 values on 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.
- Constraint : V → (ι → U) → (E → U) → Prop
The constraint at a vertex, on the input and the values on the edges.
- constraint_congr (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.Constraint v x α → self.Constraint v x' α'
Constraints are local: the constraint at
vsees only the inputs read atvand the values on the edges incident tov.
Instances For
The separator lemma. Let α satisfy the network on the input x and β on the input
y, and suppose that they agree on the edge 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.
Frontier values and revealed inputs along a layout #
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.
Instances For
The inputs revealed while processing the vertex numbered t are read at that vertex.
Reads grow one at a time. If each vertex reads at most one input, then along every layout,
for every k up to the number of inputs read, the first t vertices read exactly k inputs for
some t, by the discrete intermediate value theorem.
The branching program of a layout #
The branching program of a layout. Its layers are the frontiers of the layout, and its
states are the values on a frontier. Step t < |V| processes the vertex v numbered t and
reads the inputs read at v: an edge joins the values of an assignment α on the frontier
before v to its values on the frontier after v when the constraint at v holds for α.
The last step reads the inputs that the network does not read.
Instances For
Exactness #
The frontier values of a satisfying assignment form an accepting path.
Gluing. An accepting path of the branching program lists the frontier values of a satisfying assignment. An edge is on the frontier strictly after its earlier end and up to its later end, and along the path it keeps the value given to it by the step that processes its earlier end. Reading each edge off that step gives an assignment that agrees with the witness of every step on the edges at its vertex, so it satisfies every constraint.
If every input has at most one satisfying assignment, the branching program of every layout is unambiguous: an accepting path lists the frontier values of a satisfying assignment.
Counting edges #
Edges by width. At a step that processes a vertex, an edge of the program is determined by the values of an assignment on the two frontiers and the inputs read at the vertex.
The states of the branching program of a layout. At a layer t ≤ |V|, the chosen
accepting paths of the accepted inputs pass through at most |U| ^ |frontier t| states: each is
the list of the values of a satisfying assignment on the frontier.
The size of the program. If a layout has width at most w, and every vertex has degree
at most d and reads at most m inputs, then the branching program has at most
|V| · |U| ^ (w + d + m) + |U| ^ #(unread inputs) edges.
The frontier counting lemma for networks. Let the accepted inputs of a network be
K-rectangle-free. If a layout has width at most w, and 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)).
This is the rectangle bound for the branching program of the layout.
Peeling for networks. Let S have bias at most b ≥ 0 on rectangles with both sides
of size at least K, and let every input have at most one satisfying assignment. If a layout
has width at most w, and every vertex has degree at most d and reads at most m inputs, then
the accepted inputs in S and those outside S differ in number by at most
2 b |accepted| + (K - 1) ^ 2 · (|V| · |U| ^ (w + d + m) + |U| ^ #(unread inputs)).
Sweeps with extra messages #
Sweeping along a layout with extra messages. 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 messages splice, and the last extra message is the same for all inputs of S.
Instances For
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.
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.