8 Exact Synthesis of ESOP Forms
185
tables can be done very quickly. For Boolean functions with more than 16 Boolean
variables, a BDD- or SAT-based procedure can be employed.
8.3.3 Extensions and Variations
Downward vs. Upward Search Algorithm 4 describes an upward search procedure to find a minimal ESOP form starting with 1 term. This approach can be easily
modified into a downward search by starting from a maximum number of terms ˆ
k
and iteratively decreasing the number of terms by 1 as long as the constraint system
is satisfiable. If the constraint system becomes unsatisfiable for a certain number k
of terms, the previous k + 1 terms correspond to a minimal ESOP form. In practice
downward and upward search procedures are useful. An upward search procedure
is fast if the expected minimal k is small. Otherwise, proving unsatisfiability with a
SAT-solver becomes too time consuming. A downward search procedure is fast if
the expected minimal k is close to the initially provided term limit ˆ
k.
Conflict Limit For a SAT-solver proving unsatisfiability of a set of constraints,
i.e., showing that no assignment exists that satisfies the constraints, often requires
labor-intensive analysis. If the search space is sufficiently large, these proofs are
often not completed within reasonable time. Most modern SAT-solver provides a
conflict limit to allow a user to specify a maximum number of possible solving
attempts. If the SAT-solver is unable to find a satisfying assignment within the given
conflict limit, the solver reports “unknown” as solution. In this case, the synthesis
algorithm can choose to increase or decrease the current k, hoping that the next
k is easier to solve because the corresponding constraint system is less or more
constrained, respectively. When a conflict limit is employed in Algorithm 4, due
to the possible “unknown” solutions, a minimal ESOP form may not be found.
However, in case of a downward search, which systematically decreases k, an
intermediate “unknown” solution for k 1 can be safely ignored if the constraint
system is later proved satisfiable for k 2 < k 1 , whereas in case of an upward search,
an intermediate “unknown” solution for k 1 can be ignored if the constraint system
is proved unsatisfiable for a later k 2 > k 1 .
8.4 ESOP Synthesis for Quantum Computation
ESOP-based logic synthesis and optimization techniques have recently attracted
interest due to their application for quantum computing, where ESOP forms are
used as an intermediate representation to map Boolean functions into quantum
circuits [20]. The appeal of the idea stems from the fact that, in contrast to other
mapping approaches, ESOP-based synthesis does not introduce additional garbage
185
tables can be done very quickly. For Boolean functions with more than 16 Boolean
variables, a BDD- or SAT-based procedure can be employed.
8.3.3 Extensions and Variations
Downward vs. Upward Search Algorithm 4 describes an upward search procedure to find a minimal ESOP form starting with 1 term. This approach can be easily
modified into a downward search by starting from a maximum number of terms ˆ
k
and iteratively decreasing the number of terms by 1 as long as the constraint system
is satisfiable. If the constraint system becomes unsatisfiable for a certain number k
of terms, the previous k + 1 terms correspond to a minimal ESOP form. In practice
downward and upward search procedures are useful. An upward search procedure
is fast if the expected minimal k is small. Otherwise, proving unsatisfiability with a
SAT-solver becomes too time consuming. A downward search procedure is fast if
the expected minimal k is close to the initially provided term limit ˆ
k.
Conflict Limit For a SAT-solver proving unsatisfiability of a set of constraints,
i.e., showing that no assignment exists that satisfies the constraints, often requires
labor-intensive analysis. If the search space is sufficiently large, these proofs are
often not completed within reasonable time. Most modern SAT-solver provides a
conflict limit to allow a user to specify a maximum number of possible solving
attempts. If the SAT-solver is unable to find a satisfying assignment within the given
conflict limit, the solver reports “unknown” as solution. In this case, the synthesis
algorithm can choose to increase or decrease the current k, hoping that the next
k is easier to solve because the corresponding constraint system is less or more
constrained, respectively. When a conflict limit is employed in Algorithm 4, due
to the possible “unknown” solutions, a minimal ESOP form may not be found.
However, in case of a downward search, which systematically decreases k, an
intermediate “unknown” solution for k 1 can be safely ignored if the constraint
system is later proved satisfiable for k 2 < k 1 , whereas in case of an upward search,
an intermediate “unknown” solution for k 1 can be ignored if the constraint system
is proved unsatisfiable for a later k 2 > k 1 .
8.4 ESOP Synthesis for Quantum Computation
ESOP-based logic synthesis and optimization techniques have recently attracted
interest due to their application for quantum computing, where ESOP forms are
used as an intermediate representation to map Boolean functions into quantum
circuits [20]. The appeal of the idea stems from the fact that, in contrast to other
mapping approaches, ESOP-based synthesis does not introduce additional garbage