Propositional theorem proving by semantic tree trimming for hardware verification
David A. Plaisted, William John Yakowenko · 1999
The present work describes a new algorithm for testing the satisfiability of statements in propositional logic. It was designed to efficiently handle the most obvious kinds of pathological cases for the Davis-Putnam algorithm. Its performance is compared with a very efficient implementation of Davis-Putnam on a large number of problems, and it is shown to be superior. A recently-developed version of DavisPutnam with a related algorithmic enhancement is better still, but it is conjectured that the same enhancement can apply to the present work, with a similar boost in performance.