Algorithms for Satisfiability in Combinational Circuits Based on Backtrack Search and Recursive Learning
João P. Marques-Silva · 1999
Boolean Satisfiability is a ubiquitous modeling tool in Electronic Design Automation (EDA). It finds application in test pattern generation, delay-fault testing, combinational equivalence checking and circuit delay computation, among many other problems. Moreover, Boolean Satisfiability is also in the core of algorithms for solving Binate Covering Problems. This paper starts by describing how Boolean Satisfiability algorithms can take circuit structure into account when solving instances derived from combinational circuits. Afterwards, it shows how recursive learning techniques can be incorporated into Boolean Satisfiability algorithms. The proposed algorithmic framework has several natural applications in EDA. Moreover, potential advantages include smaller run times, the utilization of circuit -specific search pruning techniques, avoiding the overspecification problem that characterizes Boolean Satisfiability testers, and reducing the time for iteratively generating instances of SAT f...