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

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

doi:https://doi.org/10.1109/ICCAD.2001.968635

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

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

Princeton University

Research output: Contribution to journal › Article › peer-review

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 language	American English
Article number	43
Pages (from-to)	286-292
Number of pages	7
Journal	IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers
DOIs	https://doi.org/10.1109/ICCAD.2001.968635
State	Published - 2001

ASJC Scopus subject areas

Software
Computer Science Applications
Computer Graphics and Computer-Aided Design

Access to Document

https://doi.org/10.1109/ICCAD.2001.968635

Cite this

@article{6b689cf6bd2f4429a590fb7da359e5ba,

title = "Partition-based decision heuristics for image computation using SAT and BDDs",

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.",

author = "Aarti Gupta and Zijiang Yang and Pranav Ashar and Lintao Zhang and Sharad Malik",

year = "2001",

doi = "https://doi.org/10.1109/ICCAD.2001.968635",

language = "American English",

pages = "286--292",

journal = "IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD",

issn = "1092-3152",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

}

TY - JOUR

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

AU - Gupta, Aarti

AU - Yang, Zijiang

AU - Ashar, Pranav

AU - Zhang, Lintao

AU - Malik, Sharad

PY - 2001

Y1 - 2001

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0035215350&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0035215350&partnerID=8YFLogxK

U2 - https://doi.org/10.1109/ICCAD.2001.968635

DO - https://doi.org/10.1109/ICCAD.2001.968635

M3 - Article

SN - 1092-3152

SP - 286

EP - 292

JO - IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD

JF - IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD

M1 - 43

ER -

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

Abstract

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this