New and improved models for SAT-based bi-decomposition

Boolean function bi-decomposition is pervasive in logic synthesis. Bi-decomposition entails the decomposition of a Boolean function into two other simpler functions connected by a simple two-input gate. Existing solutions are based either on Binary Decision Diagrams (BDDs) or Boolean Satisfiability (SAT). Furthermore, the partition of the input set of variables is either assumed, or an automatic derivation is required. Most recent work on bi-decomposition proposed the use of Minimally Unsatisfiable Subformulas (MUSes) or Quantified Boolean Formulas (QBF) for computing, respectively, variable partitions of either approximate or optimum quality. This paper develops new grouporiented MUS-based models for addressing both the performance and the quality of bi-decompositions. The paper shows that approximate MUS search can be guided by the quality of well-known metrics. In addition, the paper improves on recent high-performance approximate models and versatile exact models, to address the practical requirements of bi-decomposition in logic synthesis. Experimental results obtained on representative benchmarks demonstrate significant improvement in performance as well as in the quality of decompositions.