Strategies for solving the Boolean satisfiability problem using binary decision diagrams

The Boolean satisfiability (SAT) problem is the problem of finding a soluti on to the equation f = 1, where f is a Boolean formula to be satisfied. Bin ary decision diagrams (BDDs) have been widely used to solve this problem; e ach of the individual output requirements of a multiple-output function is represented as a BDD and the conjunction of these requirements (product BDD ) provides all satisfying solutions. However, these techniques suffer from BDD size explosion problems. This paper presents two BDD-based algorithms t o solve the SAT problem that attempt to contain the growth of BDD size whil e identifying solutions quickly. The first algorithm, called BSAT, is a recursive, backtracking algorithm th at uses an exhaustive search to find a SAT solution. It exploits the well-k nown unate recursive paradigm to reduce the effective size of search space for the SAT problem. We recursively apply orthonormal expansion on highly b inate functions that may eventually lead to unate cofactors. The second alg orithm, called IS-USAT (for INCOMPLETE-SEARCH-USAT), incorporates an incomp lete search to find a solution. The search is incomplete inasmuch as it is restricted to only those regions that have a high likelihood of containing the solution, discarding the rest. Using our techniques we were able to fin d SAT solutions not only for all MCNC and ISCAS benchmarks, but also for a variety of industry standard designs, solutions for many of which could not be found by contemporary BDD-based SAT techniques. (C) 2001 Elsevier Scien ce B.V. All rights reserved.