7.3 Design of Application-Specific Architectures
89
7.3.2 General Idea
Satisfiability Modulo Theories (SMT) is the field considering the satisfiability of
formulas with respect to some background theory. The background theory thereby
fixes the interpretation of predicate and function symbols [5]. For checking the
satisfiability, corresponding SMT-solvers implement intelligent decision heuristics,
powerful learning schemes, and fast implication methods. These highly optimized
solvers allow to efficiently traverse large search spaces and have been proven to
be effective for many practically relevant design problems. For example, SMTsolvers have been proven effective for design automation tasks for other microfluidic
platforms, e.g., for digital microfluidics using electrowetting [71–73] and for
microfluidics based on the large-scale integration using valves [45, 51].
However, SMT solvers are specialized for solving decision problems. Hence,
in order to utilize SMT-solvers, the design problem of generating an optimized
application-specific architecture is re-phrased as a decision problem, i.e.
Is there an architecture which
(i) realizes all experiments,
(ii) satisfies all physical constraints, and
(iii) is optimized with respect to one or more of the quality criteria?
Then, this decision problem is formalized in a fashion that can be handled by the
utilized SMT-solvers. To this end, the following steps are conducted:
• A symbolic formulation representing all possible architectures ˆ
G to be considered is created. This is done by encoding these architectures in terms of Boolean
variables.
• The possible assignments are restricted (by additional Boolean constraints) so
that only assignments result which represent architectures realizing all experiments and satisfying all physical constraints (employing issue (i) and (ii) of the
decision problem).
• An objective function is added which enforces the SMT-solver to determine that
particular assignment (out of the remaining ones) which is optimized or even
optimal with respect to one or more of the quality criteria (employing issue (iii)
of the decision problem).
Passing the resulting symbolic formulation to the SMT-solver either yields an
assignment (which is optimized with respect to the objective function) or proves
that no assignment satisfying all constraints exists. In the former case, the desired
architecture can be derived from the obtained variable assignments. In the latter
case, it has been proven that no architecture exists which realizes all experiments
under the given constraints. In the next section, details to all these steps are
provided.
89
7.3.2 General Idea
Satisfiability Modulo Theories (SMT) is the field considering the satisfiability of
formulas with respect to some background theory. The background theory thereby
fixes the interpretation of predicate and function symbols [5]. For checking the
satisfiability, corresponding SMT-solvers implement intelligent decision heuristics,
powerful learning schemes, and fast implication methods. These highly optimized
solvers allow to efficiently traverse large search spaces and have been proven to
be effective for many practically relevant design problems. For example, SMTsolvers have been proven effective for design automation tasks for other microfluidic
platforms, e.g., for digital microfluidics using electrowetting [71–73] and for
microfluidics based on the large-scale integration using valves [45, 51].
However, SMT solvers are specialized for solving decision problems. Hence,
in order to utilize SMT-solvers, the design problem of generating an optimized
application-specific architecture is re-phrased as a decision problem, i.e.
Is there an architecture which
(i) realizes all experiments,
(ii) satisfies all physical constraints, and
(iii) is optimized with respect to one or more of the quality criteria?
Then, this decision problem is formalized in a fashion that can be handled by the
utilized SMT-solvers. To this end, the following steps are conducted:
• A symbolic formulation representing all possible architectures ˆ
G to be considered is created. This is done by encoding these architectures in terms of Boolean
variables.
• The possible assignments are restricted (by additional Boolean constraints) so
that only assignments result which represent architectures realizing all experiments and satisfying all physical constraints (employing issue (i) and (ii) of the
decision problem).
• An objective function is added which enforces the SMT-solver to determine that
particular assignment (out of the remaining ones) which is optimized or even
optimal with respect to one or more of the quality criteria (employing issue (iii)
of the decision problem).
Passing the resulting symbolic formulation to the SMT-solver either yields an
assignment (which is optimized with respect to the objective function) or proves
that no assignment satisfying all constraints exists. In the former case, the desired
architecture can be derived from the obtained variable assignments. In the latter
case, it has been proven that no architecture exists which realizes all experiments
under the given constraints. In the next section, details to all these steps are
provided.