Partition-based decision heuristics for image computation using SAT and BDDs

Aarti Gupta, Zijiang Yang, Pranav Ashar, Lintao Zhang, Sharad Malik

Research output: Contribution to journalArticle

33 Scopus citations

Abstract

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 languageEnglish (US)
Article number43
Pages (from-to)286-292
Number of pages7
JournalIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers
DOIs
StatePublished - 2001

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design

Fingerprint Dive into the research topics of 'Partition-based decision heuristics for image computation using SAT and BDDs'. Together they form a unique fingerprint.

  • Cite this