Exact Minimum Logic Factoring via Quantified Boolean Satisfiability

This paper presents an exact method which finds the minimum factored form of an incompletely specified Boolean function. The problem is formulated as a quantified Boolean formula (QBF) and is solved by general-purpose QBF solver. We also propose a novel graph structure, called an X-B (exchanger binary) tree, which implicitly enumerates binary trees. Using this graph structure, the factoring problem is compactly transformed into a QBF and hence the size of solvable problems is extended. Experimental results show that the proposed method successfully finds the exact minimum solutions to the problems with up to 12 literals in ten minutes.