出版社：Information and Media Technologies Editorial Board
摘要：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 compactly and implicitly enumerates binary trees. Leveraged by this graph structure, the factoring problem is transformed into a QBF. Using three sets of benchmark functions: artificially-created, randomly-generated and ISCAS 85 benchmark functions, we empirically demonstrate the quality of the solutions and the runtime complexity of the proposed method.
