Partition-based Decision Heuristics for Image Computation using SAT and BDDs

Methods based on Boolean satisfiability (SAT) typically use a Con-junctive Normal Form (CNF) representation of the Boolean for-mula, and exploit the structure of the given problem through use of various decision heuristics and implication methods. In this pa-per, we propose a new decision heuristic based on separator-set in-duced partitioning of the underlying CNF graph. It targets those variables whose choice generates clause partitions with disjoint variable supports. This can potentially improve performance of SAT applications by decomposing the problem dynamically within the search. In the context of a recently proposed image compu-tation method combining SAT and BDDs, this results in simpler BDD subproblems. We provide algorithms for CNF partitioning – one based on a clause-variable dependency matrix, and another based on standard hypergraph partitioning techniques, and also for the use of partitioning information in decision heuristics for SAT. We demonstrate the effectiveness of our proposed partition-based heuristic with practical results for reachability analysis of bench-mark sequential circuits. 1