Quantified synthesis of reversible logic

In the last years synthesis of reversible logic functions has emerged as an important research area. Other fields such as low-power design, optical computing and quantum computing benefit directly from achieved improvements. Recently, several approaches for exact synthesis of Toffoli networks have been proposed. They all use Boolean satisfiability to solve the underlying synthesis problem. In this paper a new exact synthesis approach based on Quantified Boolean Formula (QBF) satisfiability - a generalization of Boolean satisfiability - is presented. Besides the application of QBF solvers, we propose Binary Decision Diagrams to solve the quantified problem formulation. This allows to easily support different gate libraries during synthesis. In addition, all minimal networks are found in a single step and the best one with respect to quantum costs can be chosen. Experimental results confirm that the new technique is faster than the best previously known approach and leads to cheaper realizations in terms of quantum costs.