Keywords

8.1 Introduction

In the design of Very Large-Scale Integration (VLSI) systems, two-level logic representations are classically used to represent and manipulate Boolean functions. Exclusive-or Sum-of-Products (ESOP) is a two-level normal form representation of a Boolean function that consists of one level of multi-input AND gates followed on the next level by one multi-input XOR gate. ESOP forms play an important role in logic synthesis due to their improved compactness for arithmetic or communication circuits with respect to other two-level representations [26] and their excellent testability properties [13]. The inherent reversibility of the XOR operation, moreover, makes ESOP forms particularly suitable in applications such as security [16, 21] or quantum computation [8].

The ESOP representation of a Boolean function is not unique, i.e., the same Boolean function can be expressed as multiple structurally different, but semantically equivalent ESOP forms. In practice, it is important to find a small representation of an ESOP form to reduce the overall costs for realizing it in hardware or implementing it in software. The problem of synthesizing an ESOP form for a given Boolean function is to identify a set of product terms over the Boolean variables of the function such that each minterm in the OFF-set of the function is covered by the product terms an even number of times and each minterm in the ON-set of the Boolean function is covered an odd number of times.

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 sub-optimal 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 pre-computed 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 105 or 106 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 satisfiable if and only if an ESOP form with k (initially k = 1) product terms that implements the specification exists. The problem is then solved utilizing a SAT-solver and, if satisfiable, an ESOP form with k product terms is returned. Otherwise, if unsatisfiable, k is increased and the synthesis process is restarted. The synthesis approach is hardly affected by the number of Boolean variables and particularly fast if the Boolean function can be expressed by using only a few product terms. We argue that such a SAT-based exact synthesis procedure can be a backbone of a new generation of heuristic ESOP optimization methods that, instead of relying on cube transformations applied to a pair of product terms, are capable of optimizing small subsets (windows) of product terms.

The proposed approach is the first ESOP synthesis technique based on Boolean satisfiability. We further present a relaxation of the technique to compute ESOP forms with size close to minimal leveraging the SAT-solver’s conflict limit. We have implemented SAT-based exact synthesis for ESOPs and the relaxation of the approach using an off-the-shelf SAT-solver and show in the experiments that SAT-based ESOP synthesis can be readily used to synthesize ESOP forms with up to 8 Boolean variables and up to 100 terms. As benchmarks, we use completely specified Boolean functions that are used as representatives of the NPN4 equivalence classes [12] as well as completely specified Boolean functions that appeared in technology mapping using look-up tables (LUTs) with at most 8 inputs (8-LUT mapping). Moreover, we use a set of randomly generated incompletely specified Boolean functions with up to 8 Boolean variables.

8.2 Background

Exclusive-or Sum-of-Products (ESOP)

Let \(\mathbb {B} = \{0,1\}\) and \(\mathbb {B}_{3} = \{0,1,-\}\) with the third element “−” which denotes don’t care. An ESOP form in n Boolean variables x 1, …, x n is a Boolean expression

$$\displaystyle \begin{aligned} \bigoplus_{j=1}^k \left( \bigwedge_{i=1}^n x_i^{l_{i,j}} \right), \end{aligned} $$
(8.1)

where the operators ⊕ and ∧ denote standard addition (XOR) and multiplication (AND) in the Galois field with two-elements, respectively, each \(l_{i,j} \in \mathbb {B}_{3}\) is a constant and each expression

$$\displaystyle \begin{aligned} x_i^{l_{i,j}} = \begin{cases}\bar{x}_i,&\text{if}\ l_{i,j} = 0\\x_i,&\text{if}\ l_{i,j} = 1\\1,&\text{if}\ l_{i,j} = -\end{cases} \end{aligned} $$
(8.2)

for 1 ≤ i ≤ n and 1 ≤ j ≤ k. We say that k is the size of the ESOP form and call each conjunction \(x_1^{l_{1,j}} \cdots x_n^{l_{n,j}}\), 1 ≤ j ≤ k, that appears in the ESOP form a product term. The Boolean expression in (8.1) is often compactly notated as a list of words

$$\displaystyle \begin{aligned} l_{1,1} \cdots l_{n,1} \quad l_{1,2} \cdots l_{n,2} \qquad \dots \qquad l_{1,k} \cdots l_{n,k}, \end{aligned} $$
(8.3)

where each word l 1,j⋯l n,j is of fixed length n.

Distance of Product Terms

Suppose that

$$\displaystyle \begin{aligned} u = x_1^{l_{1,p}} \cdots x_n^{l_{n,p}}\qquad {}\text{ and }\qquad {}v = x_1^{l_{1,q}} \cdots x_n^{l_{n,q}} \end{aligned} $$
(8.4)

are two product terms in n Boolean variables. We define the distance d(u, v) of u and v as the number of different l i,j for 1 ≤ i ≤ n and j ∈{p, q}, i.e.,

$$\displaystyle \begin{aligned} d(u,v) = \sum_{i=1}^n [ l_{i,p} \neq l_{i,q} ], \end{aligned} $$
(8.5)

where [.] denote the Iverson brackets. We say if d(u, v) = m, then u and v have distance m or are m-distant.

ESOPs Describing Boolean Functions

An ESOP form semantically describes a (single-output) Boolean function \(f : \mathbb {B}^n \rightarrow \mathbb {B}\), which maps assignments of the Boolean variables \(x_1, \dots , x_n \in \mathbb {B}\) to truth values \(f(x_1, \dots , x_n) \in \mathbb {B}\). Each assignment to all Boolean variables x 1, …, x n is called a minterm and can be interpreted as the decimal number \(\sum _{i=1}^n x_i 2^{i-1}\) when read as (x n⋯x 1)2.

A completely specified Boolean function \(f : \mathbb {B}^n \rightarrow \mathbb {B}\) over n Boolean variables can be uniquely represented as a truth table, i.e., a word \(b_{2^nS} \cdots b_1\) of length 2n, where b j = f(j − 1) for 1 ≤ j ≤ 2n. An incompletely specified Boolean function \(g : \mathbb {B}^n \rightarrow \mathbb {B}_3\) can be represented by two completely specified Boolean functions \(f : \mathbb {B}^n \rightarrow \mathbb {B}\) and \(c : \mathbb {B}^n \rightarrow \mathbb {B}\), where f(x) = [g(x) = 1] and c(x) = [g(x) ≠ −]. We call c the care function of g.

Two ESOP forms are semantically equivalent if they describe the same Boolean function. An ESOP form with size k is minimal if and only if no semantically equivalent ESOP form with fewer product terms exists. Minimal ESOP forms are in general not unique.

8.3 SAT-Based Exact ESOP Synthesis

8.3.1 Exact Synthesis of ESOP Forms

Objective

We aim for synthesizing minimal ESOP forms in n Boolean variables when a completely specified Boolean function or incompletely specified Boolean function is provided as specification. In case of completely specified Boolean functions, this objective can be formally described as follows: given a single-output Boolean function \(f : \mathbb {B}^n \rightarrow \mathbb {B}\) over n Boolean variables x 1, …, x n, find an integer k and constants \(l_{i,j} \in \mathbb {B}_3\) for 1 ≤ i ≤ n and 1 ≤ j ≤ k such that

$$\displaystyle \begin{aligned} \bigoplus_{j=1}^k \left( \bigwedge_{i=1}^n x_i^{l_{i,j}} \right) = f(x_1,\dots,x_n)\ \text{for}\ \text{all}\ x_1, \dots, x_n \in \mathbb{B}^{n} \end{aligned} $$
(8.6)

and k is minimal. The case of incompletely specified Boolean functions can be addressed similarly to (8.6).

Example 8.1

As an introductory example, consider the incompletely specified Boolean function described by the truth table 0x688C802028222222 Footnote 1 over 6 Boolean variables with care function 0x6AAEFF3FFEBFEAA6. A minimal ESOP form, for instance, is

$$\displaystyle \begin{aligned} \bar{x}_1 x_3 \bar{x}_4 \bar{x}_5 x_6 \oplus \bar{x}_1 x_2 \bar{x}_3 x_5 \bar{x}_6 \oplus \bar{x}_1 \bar{x}_3 \bar{x}_4 \bar{x}_6 \oplus \bar{x}_2 \bar{x}_5 \bar{x}_6 \oplus \bar{x}_1 x_2 x_6, \end{aligned} $$
(8.7)

which requires 5 product terms and can be equivalently written as

(8.8)

In general, minimal ESOPs are not unique. The same Boolean function may also be represented as the ESOP form

(8.9)

or

(8.10)

Finding minimal ESOP forms is, due to the large combinational search space, a challenging problem. In [23], a minimal ESOP form for the Boolean function in the previous example was found on average in roughly 668.22 s using integer non-linear programming using different starting points and Matlab as a solving engine. The authors, moreover, point out that decomposition-based ESOP synthesis approaches, e.g., [25], require up to 4 h for synthesizing minimal ESOP forms for incompletely specified Boolean functions over 6 Boolean variables.

8.3.2 SAT-Based Exact Synthesis Procedure

In this section, we propose a SAT-based exact synthesis approach for ESOP forms. The approach is based on ideas from Knuth [15] (originally proposed by Kamath et al. [14]) and our previous work on learning two-level patches to correct combinational Boolean circuits [24]. Our approach synthesizes an ESOP form for the Boolean function in Example 8.1 in less than a second. We formalize the search problem as a series of Boolean constraint satisfaction problems—one for each possible ESOP size k (starting with k = 1) and employ a decision procedure for Boolean satisfiability to decide the satisfiability of the constraints. The constraints are constructed in such a way that they are satisfiable if and only if an ESOP form with k product terms exists and each satisfying assignment corresponds to an ESOP form with k product terms. If the constraints are unsatisfiable, then no ESOP form restricted to k product terms, that is equivalent to the provided Boolean function, exists. By systematically solving the constraint satisfaction problem for increasing values of the size parameter k, a minimal ESOP form is guaranteed to be found.

Formulation of the Constraint Satisfaction Problem

Suppose that \(f : \mathbb {B}_3^n \rightarrow \mathbb {B}\) is a (single-output) Boolean function over n Boolean variables. We formulate the problem of finding an ESOP form equivalent to f with k product terms as a constraint satisfaction problem in propositional logic using 2nk Boolean variables, p = p 1,1, …, p k,n and q = q 1,1, …, q k,n, where n is the number of Boolean variables of f, k is the size of the ESOP form, and

$$\displaystyle \begin{aligned} p_{j,l} = [x_l\ \text{in}\ \text{product}\ \text{term}\ j] \quad \ \text{and}\ \quad q_{j,l} = [\bar{x}_l\ \text{in}\ \text{product}\ \text{term}\ j] \end{aligned} $$
(8.11)

for 1 ≤ j ≤ k and 1 ≤ l ≤ n.

For each assignment \(x_1 \cdots x_n \in \mathbb {B}_3^n\) of the Boolean function f with the corresponding output value f(x 1, …, x n) = b, we introduce k auxiliary Boolean variables z = z 1, …, z k and add k ⋅ n + k clauses

$$\displaystyle \begin{aligned} \bigwedge_{j=1}^k \bigwedge_{l=1}^{n} \big( \bar{z}_j \vee \mathrm{ITE}(x_i,\bar{q}_{j,l}, \bar{p}_{j,l}) \big)\quad \ \text{and}\ \quad \bigwedge_{j=1}^k \left( z_j \vee \bigvee_{l=1}^{n} \mathrm{ITE}(x_i, q_{j,l}, p_{j,l}) \right), \end{aligned} $$
(8.12)

which ensure that if and only if z j = 1, then the j-th product term evaluates to 1 for assignment x 1⋯x n. The if-then-else-operator is defined as

$$\displaystyle \begin{aligned} \mathrm{ITE}(x_i, v_{j,l}, u_{j,l}) = \begin{cases}v_{j,l}, &\ \text{if}\ x_i = 1\\u_{j,l}, &\ \text{if}\ x_i = 0\\false, &\ \text{otherwise}\end{cases} \end{aligned} $$
(8.13)

with \(v_{j,l} \in \{q_{j,l}, \bar {q}_{j,l}\}\) and \(u_{j,l} \in \{p_{j,l}, \bar {p}_{j,l}\}\), respectively. One additional XOR-constraint

$$\displaystyle \begin{aligned} \left( \bigoplus_{j=1}^k z_j \right) = b \end{aligned} $$
(8.14)

per assignment guarantees that an odd number of z js evaluates to 1 if b = 1 and an even number if b = 0.

This constraint satisfaction problem is satisfiable if and only if an ESOP form of size k exists and each satisfying assignment \(\hat p_{1,1}, \dots , \hat p_{k,n}\) and \(\hat q_{1,1}, \dots , \hat q_{k,n}\) corresponds to one possible implementation.

Translating XOR-Constraints to CNF

All XOR-constraints in the constraint satisfaction problem are, by construction, formulated over disjoint sets of Boolean variables such that techniques like Gaussian elimination are not effective. Instead, we translate each XOR-constraint first into an equivalent XOR-clause by flipping one of the Boolean variables if and only if b = 0, i.e.,

$$\displaystyle \begin{aligned} (z_1 \oplus \dots \oplus z_k) = b \quad \Longrightarrow\quad \begin{cases}z_1 \oplus \dots \oplus z_k,&\text{if}\ b = 1\\z_1 \oplus \dots \oplus \bar{z}_k,&\text{if}\ b = 0.\end{cases} \end{aligned} $$
(8.15)

Then, we select two literals l a, l b from the XOR-clause and apply the Tseitin transformation to generate four clauses \((\bar {z}_a \vee \bar {z}_b \vee \bar {u})\), \((z_a \vee z_b \vee \bar {u})\), \((z_a \vee \bar {z}_b \vee u)\), \((\bar {z}_a \vee z_b \vee u)\) with the newly introduced Boolean variable u and repeat this process until only one literal is left which is added as a unit clause.

Algorithm 3 SAT-based exact ESOP synthesis

SAT-Based Exact ESOP Synthesis

The overall exact synthesis procedure is sketched in Algorithm 3. The function MakeCSP constructs the constraint satisfaction problem φ in the Boolean variables p, q, z for a given Boolean function f and size parameter k as described above. The function SAT refers to the invocation of a decision procedure for the Boolean satisfiability problem, usually called a SAT-solver, and is assumed to decide the satisfiability of φ and, if satisfiable, to also provide a satisfying assignment \(\hat p\) and \(\hat q\) for variables p and q. The assignment to the intermediate Boolean variables z is for the construction of no further interest and not returned. Finally, the function MakeESOP constructs an ESOP form from the assignment \(\hat p\) and \(\hat q\) according to the rules described in (8.11). Note that Algorithm 3 always terminates, but may run out of resources (memory or time) if the minimal ESOP requires many product terms. Thus in practice usually an additional termination criterion in form of an upper bound for the size parameter k or maximum number of conflicts examined by the SAT-solver is provided.

Algorithm 4 SAT-based exact synthesis guided by counterexamples

Counterexample-Guided Abstraction-Refinement

Algorithm 3 synthesizes an ESOP form in one step. Alternatively, counterexample-guided abstraction-refinement can be employed as shown in Algorithm 4. The idea of the abstraction-refinement loop is to iteratively update a candidate ESOP form r (starting from the empty ESOP form 𝜖) until it eventually becomes semantically equivalent to the Boolean function f to be synthesized. In each iteration, the constraints of one assignment x = x 1⋯x n for which r and f evaluate differently (r(x) ≠ f(x)) are added (AddConstraints) to the constraint satisfaction problem and r is resynthesized. If φ becomes unsatisfiable, then the constraints cannot be solved within the current restriction to k product terms and k needs to be relaxed. If f and r are equivalent, i.e., no counterexample x = x 1⋯x n is found by NotEquivalent, then r is returned as an ESOP form semantically equivalent to f. The main advantage of Algorithms 4 over 3 lies in its ability to abstract from unnecessary constraints which keeps the constraint satisfaction problem as small as possible. The algorithm is fast mainly because modern backtrack search-based SAT-solvers support incremental solving [7] and are able to maintain learned information when new constraints are added to a satisfiability problem. The oracle NotEquivalent has to be capable of verifying whether a candidate ESOP form r is functionally equivalent to the Boolean function f. For Boolean functions with up to 16 Boolean variables, simulation using explicit representations such as truth 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 \(\hat 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 \(\hat 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 outputs (often called ancillæ) and, consequently, can be realized with fewer qubits—a highly critical resource on today’s quantum computers.

In this section, we survey ESOP-based synthesis for quantum circuits. We describe how an ESOP form can be mapped to a quantum circuit and show by example that optimizing ESOP forms has a positive effect on the cost functions for realizing them.

Reversible Logic Synthesis for Quantum Computing

Figure 8.1 illustrates an ESOP-based synthesis flow that stepwisely transforms a Boolean function into a quantum circuit leveraging ESOP forms and reversible logic circuits as intermediate representations. The so-called ESOP-based reversible logic synthesis [20] has proven effective while keeping the number of extra qubits required for transforming the ESOP form as low as possible. In fact, for translating an ESOP form with n Boolean variables, we present a construction that requires at most n + 2 qubits.

Fig. 8.1
figure 1

ESOP-based synthesis flow from a Boolean function to a quantum circuit

Full size image

We describe reversible logic circuits in terms of reversible gates using a formalism introduced by Toffoli and Fredkin [10]. Given a fixed set X  =  x 1, …, x n of Boolean variables, a (mixed-polarity multiple-controlled) Toffoli gate is a pair (C, x t) of control lines \(C \subset \{x,\bar x~|~x \in X\}\) and a target line x t ∈ X with

$$\displaystyle \begin{aligned} \{x,\bar x\} \not\subset C\ \text{for}\ \text{all}\ x \in X\qquad {}\ \text{and}\ \qquad {}\{x_t, \bar x_t\} \cup C = \emptyset. \end{aligned} $$
(8.16)

Each Toffoli gate defines a bijective Boolean function \(g : \mathbb {B}^n \rightarrow \mathbb {B}^n\)

$$\displaystyle \begin{aligned} (x_1, \dots, x_n) \mapsto (x_1, \dots, x_{t-1}, x_t \oplus f(x_1, \dots, x_n), x_{t+1}, \dots, x_n), \end{aligned} $$
(8.17)

with control function \(f : \mathbb {B}^{n-1} \rightarrow \mathbb {B}\)

$$\displaystyle \begin{aligned} (x_1, \dots, x_{t-1}, x_{t+1}, \dots, x_n) \mapsto \bigwedge_{c \in C} c. \end{aligned} $$
(8.18)

The reversible gate flips the Boolean value on the target line if the control function f evaluates to true for the values observed on the control lines.

A reversible logic circuit is a cascade of Toffoli gates and the function defined by the reversible logic circuit is the composition function of the individual functions defined by its reversible gates. We use a graphical notation based on Feynman [9] to denote reversible circuits as diagrams. Figure 8.2 illustrates the graphical notation: on the top-left, the figure shows one reversible single-target gate with an arbitrary control function f; on the top-right, a concrete example of a reversible circuit is given consisting of the cascade of the two Toffoli gates \((\{x_1, \bar x_2\}, x_5)\) and ({x 2, x 3}, x 5), where the composition function \(h(x_1,x_2,x_3) = x_1 \bar x_2 \oplus x_2 x_3\) of the two gates can be observed on line y. In this notation, the line with the ⊕ denotes the target line, whereas black and white dots denote positive and negative control lines, respectively. On the bottom, a quantum circuit is shown for the same example. We show this example for completeness, but will not discuss the graphical notation of quantum circuits (see, e.g., Soeken et al. [27] for details).

Fig. 8.2
figure 2

Graphical notation of reversible logic circuits and quantum circuits. (a) Toffoli gate. (b) Reversible circuit. (c) Quantum circuit

Full size image

Mapping ESOP forms into reversible circuits is straightforward. An ESOP form c 1 ⊕⋯ ⊕ c k with k product terms and n Boolean variables is functionally equivalent to a reversible circuit with at most n + 2 lines and k Toffoli gates, where the control function of each gate is exactly one c i for 1 ≤ i ≤ k. Since each Toffoli gate is reversible, the concrete order of the Toffoli gates does not matter.

Next, Toffoli gates are mapped into a quantum gate library [18]. In this paper, we focus on the universal fault-tolerant quantum gate library Clifford+T [17] and use the number of T-gates as cost function. This simple cost model is based on the assumption that T-gates are far more expensive to realize than all other gates in the Clifford+T library [1]. Based on concrete mappings for Toffoli gates with small number of control lines [18] and a decomposition schemata [3] for larger Toffoli gates, an overapproximation for the number of T-gates necessary to realize an ESOP form c 1 ⊕⋯ ⊕ c k can be computed as

$$\displaystyle \begin{aligned} T(c_1 \oplus \dots \oplus c_k) = \sum_{i=1}^{k} T_{\mathrm{cube}}(|c_i|) \end{aligned} $$
(8.19)

with

$$\displaystyle \begin{aligned} T_{\mathrm{cube}}(l) = \begin{cases} 0, & l \leq 1 \\ 7, & l = 2 \\ 16, & l = 3 \\ 8(l-1), & l > 3 \wedge n \geq \frac{3l + 1}{2}\\ 16(l-1), & \text{else}.\\ \end{cases} \end{aligned} $$
(8.20)

8.5 Experimental Evaluation

We have implemented Algorithm 4 in easy, an open-source toolkit for manipulating ESOP formsFootnote 2 using the prominent state-of-the-art SAT-solver Glucose 4.1 [2] as decision procedure for Boolean satisfiability.

We have evaluated the SAT-based synthesis approach in four experimentsFootnote 3:

  1. 1.

    NPN4: We synthesized all ESOP forms of minimal size for the representatives of the NPN4 equivalence class.

  2. 2.

    LUT mapping: We synthesized one ESOP form of fixed-size and one of minimal size for each of the Boolean functions that occurred during LUT mapping of Boolean networks.

  3. 3.

    Random: We synthesized one ESOP form of fixed-size and one of minimal size for randomly generated Boolean functions.

  4. 4.

    Reversible logic synthesis: We generate Pseudo-Kronecker Expressions (PKRMs)—a special case of ESOPs—and ESOP using our exact method and analyze the effect of ESOP size minimization on the size of the corresponding quantum circuits. For evaluation, we use the T-metric presented in Sect. 8.4.

All experiments have been conducted on an Intel® Core™ i7-7567U CPU @ 3.50 GHz with 16 GB RAM.

Correctness

All computed ESOP forms have been verified against their specifications, i.e., we simulated all ESOP forms for all possible values and compared the results of simulation with the initial truth tables of the provided Boolean functions. Note that it is not possible to verify the minimality of the ESOP forms.

NPN4

We synthesized all ESOP forms of minimum size for all 222 representatives of the NPN4 equivalence classes [12]. Computing one minimal ESOP form for each representatives takes 1.6 s, computing all minimal ESOP forms for each representatives takes 9.2 s. Figure 8.3 shows the histogram of the size of the minimal ESOP forms for the representatives (on the left) and the number of ESOP forms of minimal size per representative (on the right). On average a representative has 12 structurally different minimal ESOP forms. Some representatives can have 100 or more ESOP forms of minimal size. The Boolean function 0x166A (shown in Fig. 8.4) has the most minimal ESOP forms (in total 126) within the NPN4 classes.

Fig. 8.3
figure 3

Synthesis of minimal ESOP forms for NPN4

Full size image
Fig. 8.4
figure 4

Karnaugh map of 0x166A

Full size image

LUT Mapping

We synthesized one ESOP form for a fixed number of ESOP terms and one ESOP form of minimal size using downward and upward search, respectively, for each Boolean function that occurred in LUT mapping of the EPFL benchmark suite. For LUT mapping, we used the ABC command if -K 8 [4]. After LUT mapping, we applied exactmine [28] to extract all Boolean functions from the benchmarks. We obtained 4001 different Boolean functions with up to 8 Boolean variables and used SAT-based ESOP synthesis to compute ESOP forms. For this experiment, we consider a fixed conflict limit of 10, 000. The synthesis results are presented in Table 8.1: the first column (Terms) is a user-specified upper limit on the number of terms. The rest of the table is organized in three parts. The first part (fixed-size) is dedicated to synthesis of an ESOP form for the given term limit (without minimizing the number of terms). In this case, the SAT-solver’s heuristics decides whether unnecessary terms are canceled or kept. The second part (downward search) is dedicated to a synthesis procedure that iteratively synthesizes ESOP forms starting from the upper term limit and decreases the number of terms until the constraint system becomes unsatisfiable (as described in Algorithm 4). The satisfying assignment with the smallest number of terms is used for deriving an ESOP form. The last part (upward search) is similar to the second part, but starts with 1 term and increases the number if the constraint system is unsatisfiable. The satisfying assignment with the largest number of terms is used to derive an ESOP form. For each part, we list the number of Boolean functions successfully realized (R), the number of Boolean functions that could not be synthesized because the SAT-solver’s conflict limit (C) was exceeded, the average number of terms (k) for all realizable Boolean functions, and the total runtime (T) for synthesizing all Boolean functions. The runtime includes the time for synthesizing the realizable Boolean function and the time spent in unsuccessful synthesis attempts.

Table 8.1 Synthesis of ESOP forms for LUT mapping
Full size table

Example 8.2

We illustrate the effect of the conflict limit on upward and downward search with a simple example. Consider the completely specified Boolean function 0xF550311031100000. We attempt to synthesize an ESOP form of minimal size with at most 16 terms and a conflict limit of 10,000 using the upward and downward search procedures, respectively. Figure 8.5 shows the number of conflicts explored by the SAT-solver in logarithmic scale parameterized by the number of terms (k). The colors encode the decision results: green denotes satisfiable, blue denotes unsatisfiable, and gray denotes unknown. For those k for which the conflict limit of 10,000 was reached, we repeated synthesis with a much higher conflict limit of 500,000 to understand what conflict limit would allow us to conclude the correct result. The results for k = 7 and k = 8, however, remain unknown, i.e., we do not know whether the constraints are satisfiable, because the conflict limit of 500,000 was also exceeded.

Fig. 8.5
figure 5

SAT-solver results for different k for 0xF550311031100000

Full size image

The downward search starts with 16 terms and systematically decreases the number of terms. During the search, the conflict limit is reached with k = 13 for the first; the search procedure interprets this as potentially satisfiable, such that the procedure proceeds until finally k = 4 is reached. For k = 4, the procedure concludes unsatisfiability, terminates, and returns the smallest constructed ESOP form with 9 terms determined during the search process.

The upward search procedure solves the constraint system with increasing number of terms starting with 1. For k ≤ 4, the SAT-solver proves unsatisfiability of the constraint system. For 5 ≤ k ≤ 8, the SAT-solver reaches the conflict limit, which is interpreted as potentially unsatisfiable by our search procedure, such that the search proceeds until k = 9. For k = 9 terms, the constraint system becomes for the first time satisfiable and the corresponding ESOP form with 9 terms is returned.

Random

We synthesized ESOP forms for randomly generated, incompletely specified Boolean functions over 5, 6, 7, and 8 Boolean variables. Each bit in the Boolean function and its care function was chosen by flipping a fair coin. In total, we generated 100 Boolean functions for each number of Boolean variables. Table 8.2 summarizes the results for synthesizing ESOP forms. The first two columns list the number of Boolean variables (Var.) and a fixed bound on the number of terms (Terms). The rest of the table is organized as Table 8.1. Due to the symmetric design of downward and upward search, they reached exactly the same minimal ESOP forms. Overall downward search is slower due to the fact that unsatisfiability is typically harder to prove and can only be concluded by the SAT-solver for sufficiently small k. Consequently, the downward search procedure on average analyzes many more cases before unsatisfiability is reached. In contrast, upward search keeps searching until satisfiability is reached for the first time, which can occur early in the search process.

Table 8.2 Synthesis of ESOP forms for randomly generated Boolean functions
Full size table

Reversible Logic Synthesis

We synthesized ESOP forms for Boolean functions obtained from decomposition-based synthesis (DBS), a recent approach to map permutations into quantum circuits [5, 29]. We extracted the Boolean functions from the DBS approach and synthesized for each Boolean function, a Pseudo-Kronecker Expressions (PKRM)—a special case of ESOP forms—using the approach proposed by Drechsler [6], and an exact ESOP form using our proposed method with downward search.

Table 8.3 shows experimental results for 10 Boolean functions; each of them corresponds to one Toffoli gate in the quantum circuit. For both synthesis techniques, the table lists the number of product terms (k), the required runtime (Time), and the number of T-gates computed using Eq. (8.19). The example illustrates the positive effect of ESOP optimization for reducing the cost of realizing a quantum circuits. By using our exact ESOP synthesis method, the over-approximated number of T-gates could be reduced by 48.44%, while the additional runtime can be almost neglected.

Table 8.3 Synthesis of ESOP forms for Boolean functions from DBS
Full size table

8.6 Conclusion

We have presented an exact synthesis approach for computing ESOP forms using Boolean satisfiability. The approach needs no pre-computed information, synthesizes one or multiple ESOP forms of minimal size, and can take completely specified or incompletely specified Boolean functions as specifications. We have implemented the approach using an off-the-shelf SAT-solver and have further presented a relaxation that leverages the SAT-solver’s conflict limit to find ESOP forms with almost minimal size. We have also presented evidence that the synthesis procedure can deal with small-scale ESOP forms with up to 8 Boolean variables and up to 100 terms. As benchmarks, we have used Boolean functions in the NPN4 equivalence class, Boolean functions that appeared during 8-LUT mapping, and randomly generated Boolean functions. Moreover, we show how the proposed techniques can be used to reduce the costs for implemented quantum circuits. We envision that the proposed SAT-based synthesis technique can be integrated with large-scale ESOP optimization procedures, e.g., by selecting windows of terms and resynthesizing them.