Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation

In this paper, we present a new technique for the e cient dynamic detection and removal of inactive clauses, i.e. clauses that do not a ect the solutions of interest of a Boolean Satis ability 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 nd 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 nd 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...

• Type: Conference
• Year: 2001
• Where: DAC
• Authors: Aarti Gupta, Anubhav Gupta, Zijiang Yang, Pranav Ashar
• Keywords: Ability Sat Problem, Branch-and-bound Sat Algorithm, DAC 2001, Design Automation, SAT Formula