Resolution cannot polynomially simulate compressed-BFS
dc.contributor.author | Motter, DoRon B. | en_US |
dc.contributor.author | Roy, Jarrod Alexander | en_US |
dc.contributor.author | Markov, Igor L. | en_US |
dc.date.accessioned | 2006-09-08T19:37:23Z | |
dc.date.available | 2006-09-08T19:37:23Z | |
dc.date.issued | 2005-05 | en_US |
dc.identifier.citation | Motter, DoRon B.; Roy, Jarrod A.; Markov, Igor L.; (2005). "Resolution cannot polynomially simulate compressed-BFS." Annals of Mathematics and Artificial Intelligence 44 (1-2): 121-156. <http://hdl.handle.net/2027.42/41774> | en_US |
dc.identifier.issn | 1012-2443 | en_US |
dc.identifier.issn | 1573-7470 | en_US |
dc.identifier.uri | https://hdl.handle.net/2027.42/41774 | |
dc.description.abstract | 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 (PHP n m ), suitably encoded as a CNF instance, includes exponentially many steps [18]. Therefore SAT solvers based upon the DLL procedure [12] or the DP procedure [13] 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 [27], an implementation of a Compressed-BFS algorithm empirically solved instances in Θ( n 4 ) time. Here, we add to this claim, and show analytically that these instances are solvable in polynomial time by Compressed-BFS. Thus the class of tautologies efficiently provable by Compressed-BFS is different than that of any resolution-based procedure. We hope that the details of our complexity analysis shed some light on the proof system implied by Compressed-BFS. Our proof focuses on structural invariants within the compressed data structure that stores collections of sets of open clauses during the Compressed-BFS algorithm. We bound the size of this data structure, as well as the overall memory, by a polynomial. We then use this to show that the overall runtime is bounded by a polynomial. | en_US |
dc.format.extent | 645747 bytes | |
dc.format.extent | 3115 bytes | |
dc.format.mimetype | application/pdf | |
dc.format.mimetype | text/plain | |
dc.language.iso | en_US | |
dc.publisher | Kluwer Academic Publishers; Springer | en_US |
dc.subject.other | Computer Science | en_US |
dc.subject.other | Computer Science, General | en_US |
dc.subject.other | Artificial Intelligence (Incl. Robotics) | en_US |
dc.subject.other | Mathematics, General | en_US |
dc.subject.other | Nonlinear Dynamics, Complex Systems, Chaos, Neural Networks | en_US |
dc.title | Resolution cannot polynomially simulate compressed-BFS | en_US |
dc.type | Article | en_US |
dc.subject.hlbsecondlevel | Science (General) | en_US |
dc.subject.hlbsecondlevel | Computer Science | en_US |
dc.subject.hlbtoplevel | Science | en_US |
dc.subject.hlbtoplevel | Engineering | en_US |
dc.description.peerreviewed | Peer Reviewed | en_US |
dc.contributor.affiliationum | EECS, University of Michigan, 1301, Beal Ave, Ann Arbor, MI 48109-2122, USA | en_US |
dc.contributor.affiliationum | EECS, University of Michigan, 1301, Beal Ave, Ann Arbor, MI 48109-2122, USA | en_US |
dc.contributor.affiliationum | EECS, University of Michigan, 1301, Beal Ave, Ann Arbor, MI 48109-2122, USA | en_US |
dc.contributor.affiliationumcampus | Ann Arbor | en_US |
dc.description.bitstreamurl | http://deepblue.lib.umich.edu/bitstream/2027.42/41774/1/10472_2004_Article_5379427.pdf | en_US |
dc.identifier.doi | http://dx.doi.org/10.1007/s10472-004-8427-2 | en_US |
dc.identifier.source | Annals of Mathematics and Artificial Intelligence | en_US |
dc.owningcollname | Interdisciplinary and Peer-Reviewed |
Files in this item
Remediation of Harmful Language
The University of Michigan Library aims to describe library materials in a way that respects the people and communities who create, use, and are represented in our collections. Report harmful or offensive language in catalog records, finding aids, or elsewhere in our collections anonymously through our metadata feedback form. More information at Remediation of Harmful Language.
Accessibility
If you are unable to use this file in its current format, please select the Contact Us link and we can modify it to make it more accessible to you.