4.2.2.11. Graph constraints
Many of these constraints operate on graphs that are represented as lists of edges.
The constraints take a given (fixed) graph as arguments, which is represented
using two arrays, from and to, representing the graph with edges
(from[i],to[i]), where from[i] and to[i] are nodes of the graph.
In this section: bounded_dpath, bounded_path, circuit, connected, d_weighted_spanning_tree, dag, dconnected, dpath, dreachable, dsteiner, dtree, network_flow, network_flow_cost, path, reachable, steiner, subcircuit, subgraph, tree, weighted_spanning_tree.
bounded_dpath
1. predicate bounded_dpath(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of int: w,
var int: s,
var int: t,
array [int] of var bool: ns,
array [int] of var bool: es,
var int: K)
2. predicate bounded_dpath(array [int] of $$N: from,
array [int] of $$N: to,
array [int] of int: w,
var $$N: s,
var $$N: t,
array [$$N] of var bool: ns,
array [int] of var bool: es,
var int: K)
|
Constrains the subgraph ns and es of a given directed graph to be a path from s to t of weight K.
Parameters:
N: the number of nodes in the given graph
E: the number of edges in the given graph
from: the leaving node 1..N for each edge
to: the entering node 1..N for each edge
w: the weight of each edge
s: the source node (which may be variable)
t: the dest node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
K: the cost of the path
Constrains the subgraph ns and es of a given directed graph to be a path from s to t of weight K.
Parameters:
from: the leaving node for each edge
to: the entering node for each edge
w: the weight of each edge
s: the source node (which may be variable)
t: the dest node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
K: the cost of the path
|
bounded_path
1. predicate bounded_path(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of int: w,
var int: s,
var int: t,
array [int] of var bool: ns,
array [int] of var bool: es,
var int: K)
2. predicate bounded_path(array [int] of $$N: from,
array [int] of $$N: to,
array [int] of int: w,
var $$N: s,
var $$N: t,
array [$$N] of var bool: ns,
array [int] of var bool: es,
var int: K)
|
Constrains the subgraph ns and es of a given undirected graph to be a path from s to t of weight K.
Parameters:
N: the number of nodes in the given graph
E: the number of edges in the given graph
from: the leaving node 1..N for each edge
to: the entering node 1..N for each edge
w: the weight of each edge
s: the source node (which may be variable)
t: the dest node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
K: the cost of the path
Constrains the subgraph ns and es of a given undirected graph to be a path from s to t of weight K.
Parameters:
from: the leaving node for each edge
to: the entering node for each edge
w: the weight of each edge
s: the source node (which may be variable)
t: the dest node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
K: the cost of the path
|
circuit
1. predicate circuit(array [$$E] of var $$E: x)
2. predicate circuit(array [$$E] of var opt $$E: x)
|
Constrains the elements of x to define a circuit where x[i] = j means
that j is the successor of i.
Constrains the elements of x to define a circuit where x[i] = j means
that j is the successor of i. Absent elements do not take part in the circuit.
|
connected
predicate connected(array [$$E] of $$N: from,
array [$$E] of $$N: to,
array [$$N] of var bool: ns,
array [$$E] of var bool: es)
|
Constrains the subgraph ns and es of a given undirected graph to be connected.
Parameters:
from: is the leaving node for each edge
to: is the entering node for each edge
ns: is a Boolean for each node whether it is in the subgraph
es: is a Boolean for each edge whether it is in the subgraph
|
d_weighted_spanning_tree
1. predicate d_weighted_spanning_tree(array [$$E] of $$N: from,
array [$$E] of $$N: to,
array [$$E] of int: w,
var $$N: r,
array [$$E] of var bool: es,
var int: K)
2. predicate d_weighted_spanning_tree(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of int: w,
var int: r,
array [int] of var bool: es,
var int: K)
|
Constrains the set of edges es of a given directed graph to be a weighted spanning tree rooted at r of weight W.
Parameters:
from: the leaving node for each edge
to: the entering node each edge
w: the weight of each edge
r: the root node (which may be variable)
es: a Boolean for each edge whether it is in the subgraph
K: the weight of the tree
Constrains the set of edges es of a given directed graph to be a weighted spanning tree rooted at r of weight W.
Parameters:
N: the number of nodes in the given graph
E: the number of edges in the given graph
from: the leaving node 1..N for each edge
to: the entering node 1..N for each edge
w: the weight of each edge
r: the root node (which may be variable)
es: a Boolean for each edge whether it is in the subgraph
K: the weight of the tree
|
dag
predicate dag(array [$$E] of $$N: from,
array [$$E] of $$N: to,
array [$$N] of var bool: ns,
array [$$E] of var bool: es)
|
Constrains the subgraph ns and es of a given directed graph to be a DAG.
Parameters:
from: the leaving node for each edge
to: the entering node for each edge
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
|
dconnected
predicate dconnected(array [$$E] of $$N: from,
array [$$E] of $$N: to,
array [$$N] of var bool: ns,
array [$$E] of var bool: es)
|
Constrains the subgraph ns and es of a given directed graph to be connected.
Parameters:
from: the leaving node for each edge
to: the entering node for each edge
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
|
dpath
1. predicate dpath(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: s,
var int: t,
array [int] of var bool: ns,
array [int] of var bool: es)
2. predicate dpath(array [int] of $$N: from,
array [int] of $$N: to,
var $$N: s,
var $$N: t,
array [$$N] of var bool: ns,
array [int] of var bool: es)
|
Constrains the subgraph ns and es of a given directed graph to be a path from s to t.
Parameters:
N: the number of nodes in the given graph
E: the number of edges in the given graph
from: the leaving node 1..N for each edge
to: the entering node 1..N for each edge
s: the source node (which may be variable)
t: the dest node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
Constrains the subgraph ns and es of a given directed graph to be a path from s to t.
Parameters:
from: the leaving node for each edge
to: the entering node for each edge
s: the source node (which may be variable)
t: the dest node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
|
dreachable
1. predicate dreachable(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: r,
array [int] of var bool: ns,
array [int] of var bool: es)
2. predicate dreachable(array [$$E] of $$N: from,
array [$$E] of $$N: to,
var $$N: r,
array [$$N] of var bool: ns,
array [$$E] of var bool: es)
|
Constrains the subgraph ns and es of a given directed graph to be reachable from r.
Parameters:
N: the number of nodes in the given graph
E: the number of edges in the given graph
from: the leaving node 1..N for each edge
to: the entering node 1..N for each edge
r: the root node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
Constrains the subgraph ns and es of a given directed graph to be reachable from r.
Parameters:
from: the leaving node for each edge
to: the entering node for each edge
r: the root node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
|
dsteiner
predicate dsteiner(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of int: w,
var int: r,
array [int] of var bool: ns,
array [int] of var bool: es,
var int: K)
|
Constrains the subgraph ns and es of a given directed graph to be a weighted spanning tree rooted at r of weight W.
Parameters:
N: the number of nodes in the given graph
E: the number of edges in the given graph
from: the leaving node 1..N for each edge
to: the entering node 1..N for each edge
w: the weight of each edge
r: the root node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
K: the weight of the tree
|
dtree
1. predicate dtree(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: r,
array [int] of var bool: ns,
array [int] of var bool: es)
2. predicate dtree(array [$$E] of $$N: from,
array [$$E] of $$N: to,
var $$N: r,
array [$$N] of var bool: ns,
array [$$E] of var bool: es)
|
Constrains the subgraph ns and es of a given directed graph to be a tree rooted at r.
Parameters:
N: the number of nodes in the given graph
E: the number of edges in the given graph
from: the leaving node 1..N for each edge
to: the entering node 1..N for each edge
r: the root node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
Constrains the subgraph ns and es of a given directed graph to be at tree rooted at r.
Parameters:
from: the leaving node for each edge
to: the entering node for each edge
r: the root node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
|
network_flow
predicate network_flow(array [$$E,1..2] of $$N: arc,
array [$$N] of int: balance,
array [$$E] of var int: flow)
|
Defines a network flow constraint.
Parameters:
arc: a directed arc of the flow network. Arc i connects node arc[i,1] to node arc[i,2].
balance: the amount of flow added or removed by each node. If the balance is positive then flow is added by the node, and it is removed when it is negative, i.e., balance = output - input.
flow: the flow going through each arc.
|
network_flow_cost
predicate network_flow_cost(array [$$E,1..2] of $$N: arc,
array [$$N] of int: balance,
array [$$E] of int: weight,
array [$$E] of var int: flow,
var int: cost)
|
Defines a network flow constraint with cost.
Parameters:
arc: a directed arc of the flow network. Arc i connects node arc[i,1] to node arc[i,2].
balance: the amount of flow added or removed by each node. If the balance is positive then flow is added by the node, and it is removed when it is negative, i.e., balance = output - input.
weight: the unit cost of the flow through the arc.
flow: the flow going through each arc.
cost: the overall cost of the flow.
|
path
1. predicate path(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: s,
var int: t,
array [int] of var bool: ns,
array [int] of var bool: es)
2. predicate path(array [int] of $$N: from,
array [int] of $$N: to,
var $$N: s,
var $$N: t,
array [$$N] of var bool: ns,
array [int] of var bool: es)
|
Constrains the subgraph ns and es of a given undirected graph to be a path from s to t.
Parameters:
N: the number of nodes in the given graph
E: the number of edges in the given graph
from: the leaving node 1..N for each edge
to: the entering node 1..N for each edge
s: the source node (which may be variable)
t: the dest node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
Constrains the subgraph ns and es of a given undirected graph to be a path from s to t.
Parameters:
from: the leaving node for each edge
to: the entering node for each edge
s: the source node (which may be variable)
t: the dest node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
|
reachable
1. predicate reachable(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: r,
array [int] of var bool: ns,
array [int] of var bool: es)
2. predicate reachable(array [$$E] of $$N: from,
array [$$E] of $$N: to,
var $$N: r,
array [$$N] of var bool: ns,
array [$$E] of var bool: es)
|
Constrains the subgraph ns and es of a given undirected graph to be reachable from r.
Parameters:
N: the number of nodes in the given graph
E: the number of edges in the given graph
from: the leaving node 1..N for each edge
to: the entering node 1..N for each edge
r: the root node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
Constrains the subgraph ns and es of a given undirected graph to be reachable from r.
Parameters:
from: the leaving node for each edge
to: the entering node for each edge
r: the root node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
|
steiner
predicate steiner(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of int: w,
array [int] of var bool: ns,
array [int] of var bool: es,
var int: K)
|
Constrains the set of edges es of a given undirected graph to be a weighted spanning tree of weight W.
Parameters:
N: the number of nodes in the given graph
E: the number of edges in the given graph
from: the leaving node 1..N for each edge
to: the entering node 1..N for each edge
w: the weight of each edge
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
K: the weight of the tree
|
subcircuit
predicate subcircuit(array [$$E] of var $$E: x)
|
Constrains the elements of x to define a subcircuit where x[i] = j
means that j is the successor of i and x[i] = i means that i
is not in the circuit. |
subgraph
1. predicate subgraph(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of var bool: ns,
array [int] of var bool: es)
2. predicate subgraph(array [$$E] of $$N: from,
array [$$E] of $$N: to,
array [$$N] of var bool: ns,
array [$$E] of var bool: es)
|
Constrains that ns and es is a subgraph of a given directed graph.
Parameters:
N: the number of nodes in the given graph
E: the number of edges in the given graph
from: the leaving node 1..N for each edge
to: the entering node 1..N for each edge
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
Constrains that ns and es is a subgraph of a given directed graph.
Parameters:
from: the leaving node for each edge
to: the entering node for each edge
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
|
tree
1. predicate tree(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
var int: r,
array [int] of var bool: ns,
array [int] of var bool: es)
2. predicate tree(array [$$E] of $$N: from,
array [$$E] of $$N: to,
var $$N: r,
array [$$N] of var bool: ns,
array [$$E] of var bool: es)
|
Constrains the subgraph ns and es of a given undirected graph to be a tree rooted at r.
Parameters:
N: the number of nodes in the given graph
E: the number of edges in the given graph
from: the leaving node 1..N for each edge
to: the entering node 1..N for each edge
r: the root node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
Constrains the subgraph ns and es of a given undirected graph to be at tree rooted at r.
Parameters:
from: the leaving node for each edge
to: the entering node for each edge
r: the root node (which may be variable)
ns: a Boolean for each node whether it is in the subgraph
es: a Boolean for each edge whether it is in the subgraph
|
weighted_spanning_tree
predicate weighted_spanning_tree(array [$$E] of int: from,
array [$$E] of int: to,
array [$$E] of int: w,
array [$$E] of var bool: es,
var int: K)
predicate weighted_spanning_tree(int: N,
int: E,
array [int] of int: from,
array [int] of int: to,
array [int] of int: w,
array [int] of var bool: es,
var int: K)
|
Constrains the set of edges es of a given undirected graph to be a weighted spanning tree of weight W.
Parameters:
N: the number of nodes in the given graph
E: the number of edges in the given graph
from: the leaving node 1..N for each edge
to: the entering node 1..N for each edge
w: the weight of each edge
es: a Boolean for each edge whether it is in the subgraph
K: the weight of the tree
|