Incremental Boolean satisfiability and its application to electronic design automation.

Abstract

Boolean satisfiability has been successfully applied to various problems in electronic design automation. These applications typically involve targeting and solving a set of related satisfiability problems. However, there has been no attempt to take advantage of the similarity among the resulting satisfiability problems. In this thesis, we introduce the concept of incremental satisfiability and classify its manifestations in different problem domains into three classes. For each class, we present a method to efficiently solve the problem, followed by extensive experimental validation. We then apply the proposed incremental satisfiability engine to a number of applications in electronic design automation: timing analysis, delay fault testing, testing for stuck-at faults. For each of these applications, we identify the class of incremental satisfiability to which the resulting satisfiability problems belong and present a procedure to enhance performance by taking advantage of the problem structure. The practicality of the proposed approach is supported by experimental results on all of the problem domains.