Search algorithms for satisfiability problems in combinational switching circuits.
Joao Paulo Marques Da Silva · ePrints Soton (University of Southampton) · 1995
A number of tasks in computer-aided analysis of combinational circuits, including test pattern generation, timing analysis, delay fault testing and logic verification, can be viewed as particular formulations of the satisfiability problem (SAT).The first purpose of this dissertation is to describe a configurable search-based algorithm for SAT that can be used for implementing different circuit analysis tools.Several methods for reducing the amount of search are detailed and integrated into a general algorithmic framework for solving SAT.Special emphasis is given to the description of methods for diagnosing the causes of conflicts that may be identified while searching for a solution to each instance of SAT.These methods allow the implementation of nonchronological backtracking, conflict identification based on equivalence relations and logic value assertions derived from conflicts.