90
7 Designing Application-Specific Architectures
7.4 Symbolic Formulation
In this section, the details of the corresponding symbolic formulation are provided.
To this end, this section describes the implementation of all steps of the decision
problem reviewed in Sect. 7.3.2.
7.4.1 Symbolic Formulation of All Architectures
In order to symbolically formulate all possible architectures to be considered, an
encoding of all possible graphs with nodes V ⊆ ˆ
V and edges E ⊆ ˆ
E is created. To
this end, a symbolic one-hot encoding is applied where a single Boolean variable
represents whether an edge possible according to ˆ
E is indeed present in E. More
formally:
Definition 7.3 Let ˆ
G = ( ˆ
V , ˆ
E) be the superset architecture out of which a subgraph G representing the desired architecture shall be derived. Then, for each
edge (u, v) ∈ ˆ
E, a free Boolean variable e (u,v) with u, v ∈ ˆ
V is introduced. These
variables represent whether (e (u,v) = 1) or not (e (u,v) = 0) there is an edge from
node u to node v.
Note that, by this, also the presence of nodes in G is implicitly represented:
If an assignment is applied representing no incoming edge to a node v ∈ ˆ
V
(i.e., e (u,v) = 0 for all u ∈ ˆ
V \ {v}), then v is not present in G.
Example 7.4 Consider again the setting as given in Example 7.3. Figure 7.2a
sketches the resulting graph ˆ
G = ( ˆ
V , ˆ
E) together with the introduced e (u,v) -
variables. A possible assignment to these variables is given in Fig. 7.2b leading
to a graph G as shown in Fig. 7.2c (which is equal to the architecture shown in
Fig. 7.1b).
Passing this symbolic formulation to an SMT-solver would yield an arbitrary
assignment to the e (u,v) -variables and, hence, an arbitrary sub-graph G of ˆ
G. Since
the graph has to satisfy the experiments and constraints, the possible assignments to
all e (u,v) -variables have to be restricted.
7.4.2 Realization of Experiments
First, restrictions are enforced which only allow for e (u,v) -assignments that represent
graphs realizing the desired set of experiments . Recall that an experiment φ ∈
is given as a sequence of operations and these operations have to be executed by
respective modules. Hence, the graph G has to contain a path of nodes realizing the
7 Designing Application-Specific Architectures
7.4 Symbolic Formulation
In this section, the details of the corresponding symbolic formulation are provided.
To this end, this section describes the implementation of all steps of the decision
problem reviewed in Sect. 7.3.2.
7.4.1 Symbolic Formulation of All Architectures
In order to symbolically formulate all possible architectures to be considered, an
encoding of all possible graphs with nodes V ⊆ ˆ
V and edges E ⊆ ˆ
E is created. To
this end, a symbolic one-hot encoding is applied where a single Boolean variable
represents whether an edge possible according to ˆ
E is indeed present in E. More
formally:
Definition 7.3 Let ˆ
G = ( ˆ
V , ˆ
E) be the superset architecture out of which a subgraph G representing the desired architecture shall be derived. Then, for each
edge (u, v) ∈ ˆ
E, a free Boolean variable e (u,v) with u, v ∈ ˆ
V is introduced. These
variables represent whether (e (u,v) = 1) or not (e (u,v) = 0) there is an edge from
node u to node v.
Note that, by this, also the presence of nodes in G is implicitly represented:
If an assignment is applied representing no incoming edge to a node v ∈ ˆ
V
(i.e., e (u,v) = 0 for all u ∈ ˆ
V \ {v}), then v is not present in G.
Example 7.4 Consider again the setting as given in Example 7.3. Figure 7.2a
sketches the resulting graph ˆ
G = ( ˆ
V , ˆ
E) together with the introduced e (u,v) -
variables. A possible assignment to these variables is given in Fig. 7.2b leading
to a graph G as shown in Fig. 7.2c (which is equal to the architecture shown in
Fig. 7.1b).
Passing this symbolic formulation to an SMT-solver would yield an arbitrary
assignment to the e (u,v) -variables and, hence, an arbitrary sub-graph G of ˆ
G. Since
the graph has to satisfy the experiments and constraints, the possible assignments to
all e (u,v) -variables have to be restricted.
7.4.2 Realization of Experiments
First, restrictions are enforced which only allow for e (u,v) -assignments that represent
graphs realizing the desired set of experiments . Recall that an experiment φ ∈
is given as a sequence of operations and these operations have to be executed by
respective modules. Hence, the graph G has to contain a path of nodes realizing the