Complete synthesis of identity templates for quantum and reversible logic MCT circuits using SAT-solvers and proposal of suboptimality witness notion

In this study, we introduce a procedural generation technique for Identity Templates applicable to quantum and reversible logic circuits. These templates are recognized for their significant role in enhancing the efficiency of quantum and reversible logic optimization. Our approach enables the exhaustive synthesis of all potential templates up to a specified size. Leveraging the power of SAT-solver technology, we have verified the comprehensiveness of our template collections by confirming the full exploration of the search space. Additionally, we propose an innovative concept of Suboptimality Witnesses, which we anticipate will be instrumental in streamlining the search process in formal methods, akin to SAT-solvers, for the synthesis of reversible logic circuits.