Problems in propositional logic, such as Boolean satisfiability, are studied from the point of view of developing practical algorithms, although the problems are often NP-complete or co-NP-complete. Such problems are of practical importance in VLSI design verification, test generation, related CAD applications, as well as automated verification. Many other applications also occur naturally. E.g., higher order theorem provers require a satisfiability checker as a module. Recent hardware advances bring solution of some of these problems within reach. Algorithms are being implemented and tested for performance in typical applications, such as test pattern generation, sequential circuit verification, and program verification. Model search (usually called the Davis-Putnam method) and resolution are two well known, but somewhat conflicting, strategies for solving propositional satisfiability. Model search ``succeeds'' by discovering a satisfying assignment, whereas resolution ``succeeds'' by detecting that no such assignment exists. Some work on combining the two ideas in one algorithm has recently appeared. This project investigates more powerful combinations of these methods. Besides resolution, recognition can be valuable. The goal is to identify contexts in which resolution, equality recognition, and other inferences can be beneficial in reducing the search space. Equally important is to find implementations, usually requiring advanced data structures. Another goal is the development of application-independent methods. Heuristics described in the literature for particular applications are examined to determine whether the application content can be abstracted away, making the heuristic applicable to a logic problem without knowing its origin.
