7.4 Symbolic Formulation
93
Passing this (extended) formulation to an SMT-solver would yield an assignment
to the e (u,v) -variables which will represent a sub-graph G of ˆ
G realizing all given
experiments.
7.4.3 Satisfying Physical Constraints
After the realization of the experiments is guaranteed, the physical constraints have
to be satisfied, i.e. that the maximal number of successor edges of a node are limited
(e.g., a bifurcation for passive droplet routing limits the successor edges to two) and
that resulting architectures do not contain cycles, which do not include the pump.
In order to restrict the maximal number of successor edges of each node except
the MPU (i.e., u ∈ ˆ
V \ {MP U }) to two, the number of successor edges (i.e., the
number of variables e (u,v) set to 1) have to be less than or equal to 2, i.e.
u∈ ˆ
V \{MP U}
⎛
⎝
v∈ ˆ
V
e (u,v)
⎞
⎠ ≤ 2.
Next, it has to be ensured that the resulting architectures do not contain cycles,
which do not include the MPU. Therefore, all edges which do not have the MPU as
source or destination (i.e., (u, v) where u, v ∈ ˆ
V \ {MP U }) must not build a path,
which allows to start at some node u and follow a sequence of edges that eventually
loops back to u again. To this end, again new Boolean variables are introduced—this
time for representing all paths possible in the graph G.
Definition 7.5 Let (u, v) ∈ ( ˆ
V \ {MP U }) × ( ˆ
V \ {MP U }) be all tuples of
nodes excluding the MPU. Then, for every tuple a new Boolean variable pth (u,v)
is introduced, which represents the existence (pth (u,v) = 1) or non-existence
(pth (u,v) = 0) of a path from node u to v. A path is a sequence of edges starting at
node u which, eventually, ends in node v.
Obviously, these pth (u,v) -variables depend on the respective assignment of the
e (u,v) -variables. If there exists an edge between u ∈ ˆ
V and v ∈ ˆ
V (i.e., if e (u,v) is
set to 1), then there also exists a path between these nodes. This is accomplished by
the constraint
u∈ ˆ
V \{MP U}
v∈ ˆ
V \{MP U}
e (u,v) ⇒ pth (u,v) .
Similarly, also the transitive relations of paths are enforced, i.e. if there is a path
between the nodes u and v and a path between the nodes v and w (all in ˆ
V \{MP U }),
then there is also a path between the nodes u and w. This motivates the constraint
u∈ ˆ
V \{MP U}
v∈ ˆ
V \{MP U}
w∈ ˆ
V \{MP U}
pth (u,v) ∧ pth (v,w) ⇒ pth (u,w) .
93
Passing this (extended) formulation to an SMT-solver would yield an assignment
to the e (u,v) -variables which will represent a sub-graph G of ˆ
G realizing all given
experiments.
7.4.3 Satisfying Physical Constraints
After the realization of the experiments is guaranteed, the physical constraints have
to be satisfied, i.e. that the maximal number of successor edges of a node are limited
(e.g., a bifurcation for passive droplet routing limits the successor edges to two) and
that resulting architectures do not contain cycles, which do not include the pump.
In order to restrict the maximal number of successor edges of each node except
the MPU (i.e., u ∈ ˆ
V \ {MP U }) to two, the number of successor edges (i.e., the
number of variables e (u,v) set to 1) have to be less than or equal to 2, i.e.
u∈ ˆ
V \{MP U}
⎛
⎝
v∈ ˆ
V
e (u,v)
⎞
⎠ ≤ 2.
Next, it has to be ensured that the resulting architectures do not contain cycles,
which do not include the MPU. Therefore, all edges which do not have the MPU as
source or destination (i.e., (u, v) where u, v ∈ ˆ
V \ {MP U }) must not build a path,
which allows to start at some node u and follow a sequence of edges that eventually
loops back to u again. To this end, again new Boolean variables are introduced—this
time for representing all paths possible in the graph G.
Definition 7.5 Let (u, v) ∈ ( ˆ
V \ {MP U }) × ( ˆ
V \ {MP U }) be all tuples of
nodes excluding the MPU. Then, for every tuple a new Boolean variable pth (u,v)
is introduced, which represents the existence (pth (u,v) = 1) or non-existence
(pth (u,v) = 0) of a path from node u to v. A path is a sequence of edges starting at
node u which, eventually, ends in node v.
Obviously, these pth (u,v) -variables depend on the respective assignment of the
e (u,v) -variables. If there exists an edge between u ∈ ˆ
V and v ∈ ˆ
V (i.e., if e (u,v) is
set to 1), then there also exists a path between these nodes. This is accomplished by
the constraint
u∈ ˆ
V \{MP U}
v∈ ˆ
V \{MP U}
e (u,v) ⇒ pth (u,v) .
Similarly, also the transitive relations of paths are enforced, i.e. if there is a path
between the nodes u and v and a path between the nodes v and w (all in ˆ
V \{MP U }),
then there is also a path between the nodes u and w. This motivates the constraint
u∈ ˆ
V \{MP U}
v∈ ˆ
V \{MP U}
w∈ ˆ
V \{MP U}
pth (u,v) ∧ pth (v,w) ⇒ pth (u,w) .