Exact Multiple-Control Toffoli Network Synthesis With SAT Techniques

Synthesis of reversible logic has become a very important research area in recent years. Applications can be found in the domain of low-power design, optical computing, and quantum computing. In the past, several approaches have been introduced that synthesize reversible networks with respect to a given function. Most of these methods only approximate a minimal network representation. In this paper, exact algorithms for the synthesis of multiple-control Toffoli networks are presented, i.e., algorithms that guarantee to find a network with the minimal number of gates. Our iterative algorithms formulate the synthesis problem as a sequence of decision problems. The decision problems are encoded as Boolean satisfiability (SAT) or SAT modulo theory (SMT) instances, respectively. As soon as one of these instances becomes satisfiable, a Toffoli network representation for the given function has been found. We show that choosing the encoding for synthesis is crucial for the resulting runtimes. Furthermore, we discuss the principal limits of the SAT and SMT approaches. To overcome these limits, we propose a method using problem-specific knowledge during synthesis. In addition, better embeddings to make irreversible functions reversible are considered. For the resulting synthesis problems, an improvement is presented that reduces the overall runtime by automatically setting the constant inputs to their optimal values. Experimental results on a large set of benchmarks demonstrate the differences between three exact synthesis algorithms. In addition, a comparison with the best-known heuristic results is provided. In summary, the results show that, for some benchmarks, the heuristic approaches have already found the minimal network, while for other benchmarks, significantly smaller networks exist.