Soeken, MathiasDueck, Gerhard W.Miller, D. Michael2017-01-242017-01-242017-01-24201610.1007/978-3-319-40578-0_22https://infoscience.epfl.ch/handle/20.500.14299/133387WOS:000387765200022We present a more concise formulation of the transformation based synthesis approach for reversible logic synthesis, which is one of the most prominent explicit ancilla-free synthesis approaches. Based on this formulation we devise a symbolic variant of the approach that allows one to find a circuit in shorter time using less memory for the function representation. We present both a BDD based and a SAT based implementation of the symbolic variant. Experimental results show that both approaches are significantly faster than the state-of-the-art method. We were able to find ancilla-free circuit realizations for large optimally embedded reversible functions for the first time.Reversible circuit synthesisSymbolic methodsBinary decision diagramsBoolean satisfiabilitytext::conference output::conference proceedings::conference paper