Exact sat-based toffoli network synthesis

Abstract

Compact realizations of reversible logic functions are of interest in the design of quantum computers. Such reversible functions are realized as a cascade of Toffoli gates. In this paper, we present the first exact synthesis algorithm for reversible functions using generalized Toffoligates. Our iterative algorithm formulates the synthesis problem with d Toffoli gates as a sequence of Boolean Satisfiability (SAT) instances. Such an instance is satisfiable if there exists a network representation with d gates. Thus, we can guarantee minimality. In addition to fully specified reversible functions, the algorithm can be applied to incompletely specified functions. For a set of benchmarks experimental results are given.