Improvements to satisfiability-based boolean function bi-decomposition

Boolean function decomposition is ubiquitous in logic synthesis. Existing solutions are based on BDDs and, more recently, on Boolean Satisfiability (SAT). A widely studied special case is function bi-decomposition, where a function is decomposed into two other functions connected with a simple gate. Recent work exploited the identification of Minimally Unsatisfiable Subformulas (MUSes) for computing the sets of variables to use in Boolean function bi-decomposition. This paper develops new techniques for improving the use of MUSes in function bi-decomposition. The first technique exploits structural properties of the function being decomposed, whereas the second technique exploits group-oriented MUSes. Experimental results obtained on representative benchmarks demonstrate significant improvements in performance and in the quality of decompositions.