Resolution cannot polynomially simulate compressed-BFS

13 years 4 months ago

Download www.eecs.umich.edu

Many algorithms for Boolean satisfiability (SAT) work within the framework of resolution as a proof system, and thus on unsatisfiable instances they can be viewed as attempting to find proofs by resolution. However it has been known since the 1980s that every resolution proof of the pigeonhole principle (PHPm n ), suitably encoded as a CNF instance, includes exponentially many steps [1]. Therefore SAT solvers based upon the DLL procedure [2] or the DP procedure [3] must take exponential time. Polynomial-sized proofs of the pigeonhole principle exist for different proof systems, but general-purpose SAT solvers often remain confined to resolution. This result is in correlation with empirical evidence. Previously, we introduced the Compressed-BFS algorithm to solve the SAT decision problem. In an earlier work [4], an implementation of a Compressed-BFS algorithm empirically solved PHPn

DoRon B. Motter, Jarrod A. Roy, Igor L. Markov

Real-time Traffic