Graph & extensional constraints

Two families that share a shape: both describe a solution by reference to a structure given as data rather than by an arithmetic relation.

Graph constraints take a fixed graph as two parallel arrays, from and to, one entry per edge. Two Boolean arrays then select a subgraph: nodes[v] says vertex v is in it, and edges[e] says edge e is. The flow constraints are the exception: they decide a quantity per arc rather than a selection, so they take a flow array in place of the two selectors. node_offset is the number the caller’s vertices start from, since the values in from and to index nodes and a flat list cannot carry that numbering itself. The two spanning-tree constraints carry no nodes array, every vertex being covered by definition, and take a node_count in its place: a vertex in no edge is not recoverable from from and to, and without one the constraint would hold on a graph it does not span.

Extensional constraints take the permitted assignments themselves: a table of tuples, or an automaton that accepts them.

The graph constraints share a graph_ prefix rather than a type prefix, because what they constrain is the structure a subgraph takes and not the type of anything in it. A constraint over directed edges takes a _directed suffix, so graph_tree and graph_tree_directed sit together rather than being filed under t and d. The extensional constraints are named for their element type, as everything else is.

bounded_path and its relatives are absent: bounding a path’s weight is graph_path alongside a bool_lin_le over the edge selectors, which introduces nothing new. The tree constraints do carry a weight array, because their propagators filter with it; what they report is total_weight, an equality, so bounding a tree means bounding that.

Notation

The definitions below are formulas rather than sentences, and use these throughout.

$V$	$= \{\, o, \ldots, o + n - 1 \,\}$	the vertices of the given graph, where n is the length of nodes, or node_count where there is no such array
$o$	$= \mathit{node\_offset}$	the number the caller’s vertices start from
$N$	$= \{\, v \in V \mid \mathit{nodes}_{v - o + 1} \,\}$	the selected vertices
$E$	$= \{\, e \mid \mathit{edges}_e \,\}$	the selected edges
$u \sim v$	$\iff \exists e \in E : \{ \mathit{from}_e, \mathit{to}_e \} = \{ u, v \}$	a selected edge joins them
$u \to v$	$\iff \exists e \in E : \mathit{from}_e = u \wedge \mathit{to}_e = v$	a selected arc runs from one to the other
$u \rightsquigarrow v$		reachability: the reflexive-transitive closure of the adjacency above, taken over arcs in the directed constraints
$u \rightsquigarrow^{+} v$		its transitive closure, so a vertex reaching itself needs a genuine cycle
$\deg(v)$	$= \lvert \{\, e \in E \mid v \in \{ \mathit{from}_e, \mathit{to}_e \} \,\} \rvert$	the degree, how many selected edges touch it
$\deg^{-}(v)$	$= \lvert \{\, e \in E \mid \mathit{to}_e = v \,\} \rvert$	the in-degree, how many selected arcs end at it
$[P]$	$= 1 \text{ if } P,\; 0 \text{ otherwise}$	the Iverson bracket

26 constraints

bool_table

bool_table(list of var bool: xs, list of bool: tuples)

also declarable as bool_table_reif and bool_table_imp

The Boolean assignment appears as a row of the given table.

$$\exists r : \forall j : \mathit{xs}_j \leftrightarrow \mathit{tuples}_{(r-1) \cdot \lvert \mathit{xs} \rvert + j}$$

tuples is the table flattened row-major; the rows are as long as xs.

graph_acyclic_directed

graph_acyclic_directed(list of int: from, list of int: to, int: node_offset, list of var bool: nodes, list of var bool: edges)

also declarable as graph_acyclic_directed_reif and graph_acyclic_directed_imp

The selected directed subgraph contains no cycle, making it a DAG.

$$\nexists v \in N : v \rightsquigarrow^{+} v$$

graph_connected

graph_connected(list of int: from, list of int: to, int: node_offset, list of var bool: nodes, list of var bool: edges)

also declarable as graph_connected_reif and graph_connected_imp

The selected subgraph is connected.

$$\forall u, v \in N : u \rightsquigarrow v$$

graph_connected_directed

graph_connected_directed(list of int: from, list of int: to, int: node_offset, list of var bool: nodes, list of var bool: edges)

also declarable as graph_connected_directed_reif and graph_connected_directed_imp

The selected directed subgraph is strongly connected.

$$\forall u, v \in N : u \rightsquigarrow v$$

graph_network_flow

graph_network_flow(list of int: from, list of int: to, int: node_offset, list of int: balance, list of var int: flow)

also declarable as graph_network_flow_reif and graph_network_flow_imp

The flow on each arc satisfies the given supply and demand at every node.

$$\forall v : \sum_{e \,:\, \mathit{to}_e = v} \mathit{flow}_e \;-\; \sum_{e \,:\, \mathit{from}_e = v} \mathit{flow}_e \;=\; \mathit{balance}_{v - \mathit{node\_offset} + 1}$$

The graph is given as from and to, one entry per arc, the same way every other constraint here takes one. balance is numbered from node_offset: a positive value is demand, a negative one supply. Unlike the rest of the family there are no selector arrays, because every arc carries a flow rather than being in or out.

graph_network_flow_cost

graph_network_flow_cost(list of int: from, list of int: to, int: node_offset, list of int: balance, list of int: weight, list of var int: flow, var int: total_cost)

also declarable as graph_network_flow_cost_reif and graph_network_flow_cost_imp

As graph_network_flow, and the total cost is the weighted sum of the flows.

$$\mathit{total\_cost} = \sum_{e} \mathit{weight}_e \cdot \mathit{flow}_e$$

graph_path

graph_path(list of int: from, list of int: to, int: node_offset, var int: source, var int: sink, list of var bool: nodes, list of var bool: edges)

also declarable as graph_path_reif and graph_path_imp

The selected subgraph is a simple path from the source to the sink.

$$\left( \forall u, v \in N : u \rightsquigarrow v \right) \;\wedge\; \forall v \in N : \deg(v) = 2 - [\, v = \mathit{source} \,] - [\, v = \mathit{sink} \,]$$

graph_path_directed

graph_path_directed(list of int: from, list of int: to, int: node_offset, var int: source, var int: sink, list of var bool: nodes, list of var bool: edges)

also declarable as graph_path_directed_reif and graph_path_directed_imp

The selected subgraph is a simple directed path from the source to the sink.

$$\left( \mathit{source} \rightsquigarrow \mathit{sink} \right) \;\wedge\; \forall v \in N : \deg^{-}(v) = [\, v \neq \mathit{source} \,] \;\wedge\; \lvert E \rvert = \lvert N \rvert - 1$$

graph_reachable

graph_reachable(list of int: from, list of int: to, int: node_offset, var int: root, list of var bool: nodes, list of var bool: edges)

also declarable as graph_reachable_reif and graph_reachable_imp

Every selected node is reachable from the root in the selected subgraph.

$$\forall v \in N : \mathit{root} \rightsquigarrow v$$

graph_reachable_directed

graph_reachable_directed(list of int: from, list of int: to, int: node_offset, var int: root, list of var bool: nodes, list of var bool: edges)

also declarable as graph_reachable_directed_reif and graph_reachable_directed_imp

Every selected node is reachable from the root along the arcs’ direction.

$$\forall v \in N : \mathit{root} \rightsquigarrow v$$

graph_spanning_tree

graph_spanning_tree(list of int: from, list of int: to, int: node_offset, int: node_count, list of int: weight, list of var bool: edges, var int: total_weight)

also declarable as graph_spanning_tree_reif and graph_spanning_tree_imp

The selected edges span every node of the graph, reporting their total weight.

$$N = V \;\wedge\; \left( \forall u, v \in V : u \rightsquigarrow v \right) \;\wedge\; \lvert E \rvert = \lvert V \rvert - 1 \;\wedge\; \mathit{total\_weight} = \sum_{e \in E} \mathit{weight}_e$$

Unlike graph_steiner_tree, every node must be covered, so node_count stands in for the nodes array whose length gives the vertex count elsewhere.

graph_spanning_tree_directed

graph_spanning_tree_directed(list of int: from, list of int: to, int: node_offset, int: node_count, list of int: weight, var int: root, list of var bool: edges, var int: total_weight)

also declarable as graph_spanning_tree_directed_reif and graph_spanning_tree_directed_imp

The selected arcs form a spanning arborescence from the root, reporting their total weight.

$$\forall v \in V : \deg^{-}(v) = [\, v \neq \mathit{root} \,] \;\wedge\; \mathit{root} \rightsquigarrow v \;\wedge\; \mathit{total\_weight} = \sum_{e \in E} \mathit{weight}_e$$

graph_steiner_tree

graph_steiner_tree(list of int: from, list of int: to, int: node_offset, list of int: weight, list of var bool: nodes, list of var bool: edges, var int: total_weight)

also declarable as graph_steiner_tree_reif and graph_steiner_tree_imp

The selected subgraph is a tree, reporting its total edge weight.

$$\left( \forall u, v \in N : u \rightsquigarrow v \right) \;\wedge\; \lvert E \rvert = \lvert N \rvert - 1 \;\wedge\; \mathit{total\_weight} = \sum_{e \in E} \mathit{weight}_e$$

Which nodes to include is part of the decision, which is what makes it a Steiner tree rather than a spanning tree.

graph_steiner_tree_directed

graph_steiner_tree_directed(list of int: from, list of int: to, int: node_offset, list of int: weight, var int: root, list of var bool: nodes, list of var bool: edges, var int: total_weight)

also declarable as graph_steiner_tree_directed_reif and graph_steiner_tree_directed_imp

The selected subgraph is a directed tree from the root, reporting its total arc weight.

$$\left( \forall v \in N : \deg^{-}(v) = [\, v \neq \mathit{root} \,] \;\wedge\; \mathit{root} \rightsquigarrow v \right) \;\wedge\; \mathit{total\_weight} = \sum_{e \in E} \mathit{weight}_e$$

graph_subgraph

graph_subgraph(list of int: from, list of int: to, int: node_offset, list of var bool: nodes, list of var bool: edges)

also declarable as graph_subgraph_reif and graph_subgraph_imp

The selected edges and nodes form a subgraph: every selected edge has both endpoints selected.

$$\forall e \in E : \mathit{nodes}_{\mathit{from}_e - \mathit{node\_offset} + 1} \;\wedge\; \mathit{nodes}_{\mathit{to}_e - \mathit{node\_offset} + 1}$$

The well-formedness condition every other graph constraint here assumes.

graph_tree

graph_tree(list of int: from, list of int: to, int: node_offset, var int: root, list of var bool: nodes, list of var bool: edges)

also declarable as graph_tree_reif and graph_tree_imp

The selected subgraph is a tree rooted at the given node.

$$\left( \forall u, v \in N : u \rightsquigarrow v \right) \;\wedge\; \lvert E \rvert = \lvert N \rvert - 1 \;\wedge\; \mathit{root} \in N$$

graph_tree_directed

graph_tree_directed(list of int: from, list of int: to, int: node_offset, var int: root, list of var bool: nodes, list of var bool: edges)

also declarable as graph_tree_directed_reif and graph_tree_directed_imp

The selected subgraph is a directed tree with all arcs pointing away from the root.

$$\forall v \in N : \deg^{-}(v) = [\, v \neq \mathit{root} \,] \;\wedge\; \mathit{root} \rightsquigarrow v$$

int_circuit

int_circuit(list of var int: xs, int: offset)

also declarable as int_circuit_reif and int_circuit_imp

The successor array describes a single circuit visiting every node exactly once.

$$\left( \forall i \neq j : \mathit{xs}_i \neq \mathit{xs}_j \right) \;\wedge\; \lvert \{\, \sigma^{k}(v) \mid 1 \leq k \leq \lvert \mathit{xs} \rvert \,\} \rvert = \lvert \mathit{xs} \rvert \quad \text{where } \sigma(i) = \mathit{xs}_{i - \mathit{offset} + 1}$$

xs is numbered from offset, and its values name nodes in that same numbering. The Hamiltonian-circuit constraint behind most vehicle-routing models.

int_mdd

int_mdd(list of var int: xs, int: nodes, list of int: level, int: edges, list of int: from, list of set of int: label, list of int: to)

also declarable as int_mdd_reif and int_mdd_imp

The assignment corresponds to a root-to-leaf path through the given multi-valued decision diagram.

$$\exists e_1, \ldots, e_{\lvert \mathit{xs} \rvert} : \mathit{from}_{e_1} = 1 \;\wedge\; \forall j : \left( \mathit{to}_{e_j} = \mathit{from}_{e_{j+1}} \;\wedge\; \mathit{xs}_j \in \mathit{label}_{e_j} \right)$$

level gives each node’s layer, and from, label and to describe the edges. Nodes are numbered from 1, so no offset travels with them. A compact alternative to int_table when the relation factorises.

The diagram must be deterministic: no two edges leaving a node may share a label. int_mdd_nondeterministic is the form without that requirement.

int_mdd_cost

int_mdd_cost(list of var int: xs, int: nodes, list of int: level, int: edges, list of int: from, list of set of int: label, list of int: weight, list of int: to, var int: total_cost)

also declarable as int_mdd_cost_reif and int_mdd_cost_imp

As int_mdd, and the total cost sums the weight of each edge on the chosen path.

$$\exists e_1, \ldots, e_{\lvert \mathit{xs} \rvert} : \mathit{from}_{e_1} = 1 \;\wedge\; \left( \forall j : \mathit{to}_{e_j} = \mathit{from}_{e_{j+1}} \;\wedge\; \mathit{xs}_j \in \mathit{label}_{e_j} \right) \;\wedge\; \mathit{total\_cost} = \sum_{j} \mathit{weight}_{e_j}$$

int_mdd_nondeterministic

int_mdd_nondeterministic(list of var int: xs, int: nodes, list of int: level, int: edges, list of int: from, list of set of int: label, list of int: to)

also declarable as int_mdd_nondeterministic_reif and int_mdd_nondeterministic_imp

The assignment corresponds to some root-to-leaf path through the given decision diagram.

$$\exists e_1, \ldots, e_{\lvert \mathit{xs} \rvert} : \mathit{from}_{e_1} = 1 \;\wedge\; \forall j : \left( \mathit{to}_{e_j} = \mathit{from}_{e_{j+1}} \;\wedge\; \mathit{xs}_j \in \mathit{label}_{e_j} \right)$$

As int_mdd, but edges leaving a node may share a label, so an assignment may be accepted along several paths. A separate name because a propagator written for the deterministic form is wrong here.

int_regular

int_regular(list of var int: xs, int: states, int: alphabet, int: alphabet_offset, list of int: transition, int: initial, set of int: accepting)

also declarable as int_regular_reif and int_regular_imp

The array, read as a string, is accepted by the given deterministic automaton.

$$q_0 = \mathit{initial} \;\wedge\; q_j = \mathit{transition}_{q_{j-1},\, \mathit{xs}_j - \mathit{alphabet\_offset} + 1} \;\wedge\; q_{\lvert \mathit{xs} \rvert} \in \mathit{accepting}$$

transition is the state-by-symbol table flattened row-major, states rows of alphabet entries, so no row length travels with it. A transition to 0 means the string is rejected. States are numbered from 1; symbols from alphabet_offset, so xs keeps the caller’s own alphabet.

int_regular_cost

int_regular_cost(list of var int: xs, int: states, int: alphabet, int: alphabet_offset, list of int: transition, int: initial, set of int: accepting, list of int: weight, var int: total_cost)

also declarable as int_regular_cost_reif and int_regular_cost_imp

As int_regular, and the total cost sums the weight of each transition taken.

$$\mathit{total\_cost} = \sum_{j} \mathit{weight}_{q_{j-1},\, \mathit{xs}_j - \mathit{alphabet\_offset} + 1}$$

int_regular_nondeterministic

int_regular_nondeterministic(list of var int: xs, int: states, int: alphabet, int: alphabet_offset, list of set of int: transition, int: initial, set of int: accepting)

also declarable as int_regular_nondeterministic_reif and int_regular_nondeterministic_imp

The array, read as a string, is accepted by the given non-deterministic automaton.

$$\exists q : q_0 = \mathit{initial} \;\wedge\; q_j \in \mathit{transition}_{q_{j-1},\, \mathit{xs}_j - \mathit{alphabet\_offset} + 1} \;\wedge\; q_{\lvert \mathit{xs} \rvert} \in \mathit{accepting}$$

As int_regular, but each transition gives a set of possible next states.

int_subcircuit

int_subcircuit(list of var int: xs, int: offset)

also declarable as int_subcircuit_reif and int_subcircuit_imp

The successor array describes a single circuit over a subset of the nodes, with the rest as self-loops.

$$\left( \forall i \neq j : \mathit{xs}_i \neq \mathit{xs}_j \right) \;\wedge\; \lvert \{\, \sigma^{k}(v) \mid 1 \leq k \leq \lvert F \rvert \,\} \rvert = \lvert F \rvert \quad \text{where } \sigma(i) = \mathit{xs}_{i - \mathit{offset} + 1},\; F = \{\, i \mid \sigma(i) \neq i \,\},\; v \in F$$

xs is numbered from offset. A node that maps to itself is unvisited; unlike int_circuit, nodes may be left out.

int_table

int_table(list of var int: xs, list of int: tuples)

also declarable as int_table_reif and int_table_imp

The assignment to the array appears as a row of the given table.

$$\exists r : \forall j : \mathit{xs}_j = \mathit{tuples}_{(r-1) \cdot \lvert \mathit{xs} \rvert + j}$$

tuples is the table flattened row-major, one permitted assignment per row. No row length is needed: the rows are as long as xs. The most direct way to state a relation with no closed form.