Methods based on Boolean satisfiability (SAT) typically use a Conjunctive Normal Form (CNF) representation of the Boolean formula, and exploit the structure of the given problem through use of various decision heuristics and implication methods. In this paper, we propose a new decision heuristic based on separator-set induced 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 computation 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 benchmark sequential circuits.
|Original language||English (US)|
|Number of pages||7|
|Journal||IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers|
|State||Published - 2001|
All Science Journal Classification (ASJC) codes
- Computer Science Applications
- Computer Graphics and Computer-Aided Design