178
H. Riener et al.
Finding ESOP forms with a small or a minimal number of product terms is hard
and numerous exact and heuristic synthesis methods [11, 19, 22, 23, 25, 30] for
solving this problem have been proposed. Heuristic methods focus on finding small
(but not necessarily minimal) ESOP forms; they are fast, but only examine a subset
of the possible search space. Heuristic methods, e.g., the Exorcism approach [19],
usually operate in two phases. In the first phase, an ESOP form with a suboptimal number of product terms is derived from the Boolean function, e.g.,
by translating each minterm of the Boolean function into one product term or
translating the function into special cases of ESOP forms such as Pseudo-Kronecker
Expressions [6]. In the second phase, the ESOP form is iteratively optimized and
reshaped using cube transformations with the overall goal of merging as many
product terms as possible. The cube transformations are applied to each pair of
product terms that potentially lead to merging them or with other product terms
of the ESOP form. The second phase terminates when, after several iterations, no
further size reduction is achieved. Heuristic methods produce small ESOP forms in
reasonable time, but suffer from local minima that cannot easily be escaped. In
contrast, exact methods find an “exact” ESOP form, i.e., an ESOP form with a
minimal number of product terms, but either require to store large tables of precomputed information [22, 25] or suffer from long runtimes [23]. For instance,
the tabular-based methods described by Gaidukov [11] or Papakonstantinou [22]
require pre-computed tables of all exact ESOP forms for Boolean functions over
n − 1 Boolean variables to derive an exact ESOP form for a Boolean function
over n Boolean variables. Due to the exponential growth of the number of Boolean
functions in the number of Boolean variables, these methods become too time
and memory consuming when n > 6. Alternative exact synthesis approaches
such as a recent formulation of the ESOP synthesis problem using non-linear
programming [23] can take several minutes for synthesizing a single exact ESOP
form.
Until today, a large gap between the number of product terms optimized with
heuristic methods and exact methods remains. Where exact methods hardly can deal
with more than 8 Boolean variables and a few product terms, heuristic methods
nowadays, e.g., in the quantum domain, have to deal with the optimization of ESOP
forms with 10 5 or 10 6 products terms over 16 and more Boolean variables [27].
Our experiments with large-scale ESOP forms showed that heuristic optimization
method can often achieve a reduction of 50−80% in the number of ESOP terms with
respect to the size of the initial ESOP form. Due to the large combinational search
space of the ESOP synthesis problem, lower bounds on the number of required
product terms are only known for Boolean functions with a few Boolean variables,
such that the capabilities of ESOP optimization techniques remain unclear.
In this paper, we investigate the exact synthesis of ESOP forms using Boolean
satisfiability (SAT). SAT-based approaches are very successful on a variety of different verification and synthesis problems. We present an exact synthesis approach for
computing ESOP forms with a minimal number of product terms. Starting from a
specification in form of a possibly incompletely specified Boolean function, our
approach iteratively constructs a Boolean constraint satisfaction problem that is
H. Riener et al.
Finding ESOP forms with a small or a minimal number of product terms is hard
and numerous exact and heuristic synthesis methods [11, 19, 22, 23, 25, 30] for
solving this problem have been proposed. Heuristic methods focus on finding small
(but not necessarily minimal) ESOP forms; they are fast, but only examine a subset
of the possible search space. Heuristic methods, e.g., the Exorcism approach [19],
usually operate in two phases. In the first phase, an ESOP form with a suboptimal number of product terms is derived from the Boolean function, e.g.,
by translating each minterm of the Boolean function into one product term or
translating the function into special cases of ESOP forms such as Pseudo-Kronecker
Expressions [6]. In the second phase, the ESOP form is iteratively optimized and
reshaped using cube transformations with the overall goal of merging as many
product terms as possible. The cube transformations are applied to each pair of
product terms that potentially lead to merging them or with other product terms
of the ESOP form. The second phase terminates when, after several iterations, no
further size reduction is achieved. Heuristic methods produce small ESOP forms in
reasonable time, but suffer from local minima that cannot easily be escaped. In
contrast, exact methods find an “exact” ESOP form, i.e., an ESOP form with a
minimal number of product terms, but either require to store large tables of precomputed information [22, 25] or suffer from long runtimes [23]. For instance,
the tabular-based methods described by Gaidukov [11] or Papakonstantinou [22]
require pre-computed tables of all exact ESOP forms for Boolean functions over
n − 1 Boolean variables to derive an exact ESOP form for a Boolean function
over n Boolean variables. Due to the exponential growth of the number of Boolean
functions in the number of Boolean variables, these methods become too time
and memory consuming when n > 6. Alternative exact synthesis approaches
such as a recent formulation of the ESOP synthesis problem using non-linear
programming [23] can take several minutes for synthesizing a single exact ESOP
form.
Until today, a large gap between the number of product terms optimized with
heuristic methods and exact methods remains. Where exact methods hardly can deal
with more than 8 Boolean variables and a few product terms, heuristic methods
nowadays, e.g., in the quantum domain, have to deal with the optimization of ESOP
forms with 10 5 or 10 6 products terms over 16 and more Boolean variables [27].
Our experiments with large-scale ESOP forms showed that heuristic optimization
method can often achieve a reduction of 50−80% in the number of ESOP terms with
respect to the size of the initial ESOP form. Due to the large combinational search
space of the ESOP synthesis problem, lower bounds on the number of required
product terms are only known for Boolean functions with a few Boolean variables,
such that the capabilities of ESOP optimization techniques remain unclear.
In this paper, we investigate the exact synthesis of ESOP forms using Boolean
satisfiability (SAT). SAT-based approaches are very successful on a variety of different verification and synthesis problems. We present an exact synthesis approach for
computing ESOP forms with a minimal number of product terms. Starting from a
specification in form of a possibly incompletely specified Boolean function, our
approach iteratively constructs a Boolean constraint satisfaction problem that is