Abstract
A pool resolution proof is a dag-like resolution proof which admits a depth-first traversal tree in which no variable is used as a resolution variable twice on any branch. The problem of determining whether a given dag-like resolution proof is a valid pool resolution proof is shown to be NP-complete.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Alekhnovich, M., Buss, S., Moran, S., Pitassi, T.: Minimum propositional proof length is NP-hard to linearly approximate, J. Symb. Log. 66, 171–191 (2001). A shorter extended abstract appeared in Mathematical Foundations of Computer Science (MFCS’98). Lecture Notes in Computer Science, vol. 1450, pp. 176–184. Springer (1998)
Alekhnovich, M., Razborov, A.A.: Resolution is not automatizable unless W[P] is tractable. In: Proceedings of the 42nd IEEE Conference on Foundations of Computer Science (FOCS), pp. 210–219 (2001)
Bacchus, F., Hertel, P., Pitassi, T., Van Gelder, A.: Clause learning can effectively p-simulate general propositional resolution. In: Proceedings of 23rd AAAI Conference on Artificial Intelligence (AAAI 2008), pp. 283–290. AAAI Press (2008)
Beame P., Kautz H.A., Sabharwal A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. 22, 319–351 (2004)
Buss S.R., Hoffmann J.: The NP-hardness of finding a directed acyclic graph for regular resolution. Theor. Comput. Sci. 396, 271–276 (2008)
Buss, S.R., Hoffmann, J., Johannsen, J.: Resolution trees with lemmas: resolution refinements that characterize DLL-algorithms with clause learning. Log. Methods Comput. Sci. 4(4), Article 13 (2008)
Hoffmann J.: Finding a tree structure in a resolution proof is NP-complete. Theor. Comput. Sci. 410, 2295–2300 (2009)
Iwama, K.: Complexity of finding short resolution proofs. In: Prívara I., Ruzicka P. (eds) Mathematical Foundations of Computer Science 1997, Lecture Notes in Computer Science, vol. 1295, pp. 309–318. Springer (1997)
Iwama, K., Miyano, E.: Intractibility of read-once resolution, In: Proceedings of the 10th Annual Conference on Structure in Complexity Theory, pp. 29–36. IEEE Computer Society, Los Alamitos (1995)
Szeider, S.: NP-completeness of refutability by literal-once resolution. In: Automated Reasoning: 1st International Joint Conference (IJCAR), pp. 168–181. Springer (2001)
Van Gelder, A.: Pool resolution and its relation to regular resolution and DPLL with clause learning. In: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Lecture Notes in Computer Science Intelligence, vol. 3835, pp. 580–594. Springer (2005)
Acknowledgments
I thank Philip Hertel, Jan Hoffmann, Toni Pitassi, and Allen Van Gelder for useful discussions on this problem, and the referee for further comments.
Open Access
This article is distributed under the terms of the Creative Commons Attribution Noncommercial License which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.
Author information
Authors and Affiliations
Corresponding author
Additional information
Supported in part by NSF grant DMS-0700533.
Rights and permissions
Open Access This is an open access article distributed under the terms of the Creative Commons Attribution Noncommercial License (https://creativecommons.org/licenses/by-nc/2.0), which permits any noncommercial use, distribution, and reproduction in any medium, provided the original author(s) and source are credited.
About this article
Cite this article
Buss, S.R. Pool resolution is NP-hard to recognize. Arch. Math. Logic 48, 793–798 (2009). https://doi.org/10.1007/s00153-009-0152-4
Received:
Revised:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00153-009-0152-4