Dynamic detection and removal of inactive clauses in SAT with application in image computation

Aarti Gupta, Anubhav Gupta, Zijiang Yang, Pranav Ashar

Research output: Contribution to journalArticle

36 Scopus citations

Abstract

In this paper, we present a new technique for the efficient dynamic detection and removal of inactive clauses, i.e. clauses that do not affect the solutions of interest of a Boolean Satisfiability (SAT) problem. The algorithm is based on the extraction of gate connectivity information during generation of the Boolean formula from the circuit, and its use in the inner loop of a branch-and-bound SAT algorithm. The motivation for this optimization is to exploit the circuit structure information, which can be used to find unobservable gates at circuit outputs under dynamic conditions. It has the potential to speed up all applications of SAT in which the SAT formula is derived from a logic circuit. In particular, we find that it has considerable impact on an image computation algorithm based on SAT. We present practical results for benchmark circuits which show that the use of this optimization consistently improves the performance for reachability analysis, in some cases enabling the prototype tool to reach more states than otherwise possible.

Original languageEnglish (US)
Pages (from-to)536-541
Number of pages6
JournalProceedings - Design Automation Conference
DOIs
StatePublished - Jan 1 2001
Externally publishedYes

All Science Journal Classification (ASJC) codes

  • Hardware and Architecture
  • Control and Systems Engineering

Fingerprint Dive into the research topics of 'Dynamic detection and removal of inactive clauses in SAT with application in image computation'. Together they form a unique fingerprint.

Cite this