A method for concurrent decomposition and factorization of Boolean expressions

Efficient algorithms are described for decomposition and factorization of Boolean expressions. The method uses only two-literal single-cube divisors and double-cube divisors considered concurrently with their complementary expressions. It is demonstrated that these objects, despite their simplicity, provide a very good framework to reason about common algebraic divisors and the duality relations between expressions. The algorithm was implemented and excellent results on several benchmark circuits illustrate its efficiency and effectiveness.<>