{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,25]],"date-time":"2026-04-25T14:04:58Z","timestamp":1777125898688,"version":"3.51.4"},"reference-count":11,"publisher":"Springer Science and Business Media LLC","issue":"8","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2009,12]]},"DOI":"10.1007\/s00153-009-0152-4","type":"journal-article","created":{"date-parts":[[2009,9,23]],"date-time":"2009-09-23T13:02:38Z","timestamp":1253710958000},"page":"793-798","source":"Crossref","is-referenced-by-count":2,"title":["Pool resolution is NP-hard to recognize"],"prefix":"10.1007","volume":"48","author":[{"given":"Samuel R.","family":"Buss","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,9,24]]},"reference":[{"key":"152_CR1","unstructured":"Alekhnovich, M., Buss, S., Moran, S., Pitassi, T.: Minimum propositional proof length is NP-hard to linearly approximate, J. Symb. Log. 66, 171\u2013191 (2001). A shorter extended abstract appeared in Mathematical Foundations of Computer Science (MFCS\u201998). Lecture Notes in Computer Science, vol. 1450, pp. 176\u2013184. Springer (1998)"},{"key":"152_CR2","doi-asserted-by":"crossref","unstructured":"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\u2013219 (2001)","DOI":"10.1109\/SFCS.2001.959895"},{"key":"152_CR3","unstructured":"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\u2013290. AAAI Press (2008)"},{"key":"152_CR4","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1613\/jair.1410","volume":"22","author":"P. Beame","year":"2004","unstructured":"Beame P., Kautz H.A., Sabharwal A.: Towards understanding and harnessing the potential of clause learning. J. Artif. Intell. Res. 22, 319\u2013351 (2004)","journal-title":"J. Artif. Intell. Res."},{"key":"152_CR5","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/j.tcs.2008.01.039","volume":"396","author":"S.R. Buss","year":"2008","unstructured":"Buss S.R., Hoffmann J.: The NP-hardness of finding a directed acyclic graph for regular resolution. Theor. Comput. Sci. 396, 271\u2013276 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"152_CR6","doi-asserted-by":"crossref","unstructured":"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)","DOI":"10.2168\/LMCS-4(4:13)2008"},{"key":"152_CR7","doi-asserted-by":"crossref","first-page":"2295","DOI":"10.1016\/j.tcs.2009.02.018","volume":"410","author":"J. Hoffmann","year":"2009","unstructured":"Hoffmann J.: Finding a tree structure in a resolution proof is NP-complete. Theor. Comput. Sci. 410, 2295\u20132300 (2009)","journal-title":"Theor. Comput. Sci."},{"key":"152_CR8","doi-asserted-by":"crossref","unstructured":"Iwama, K.: Complexity of finding short resolution proofs. In: Pr\u00edvara I., Ruzicka P. (eds) Mathematical Foundations of Computer Science 1997, Lecture Notes in Computer Science, vol. 1295, pp. 309\u2013318. Springer (1997)","DOI":"10.1007\/BFb0029974"},{"key":"152_CR9","doi-asserted-by":"crossref","unstructured":"Iwama, K., Miyano, E.: Intractibility of read-once resolution, In: Proceedings of the 10th Annual Conference on Structure in Complexity Theory, pp. 29\u201336. IEEE Computer Society, Los Alamitos (1995)","DOI":"10.1109\/SCT.1995.514725"},{"key":"152_CR10","doi-asserted-by":"crossref","unstructured":"Szeider, S.: NP-completeness of refutability by literal-once resolution. In: Automated Reasoning: 1st International Joint Conference (IJCAR), pp. 168\u2013181. Springer (2001)","DOI":"10.1007\/3-540-45744-5_13"},{"key":"152_CR11","doi-asserted-by":"crossref","unstructured":"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\u2013594. Springer (2005)","DOI":"10.1007\/11591191_40"}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-009-0152-4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T09:13:03Z","timestamp":1739351583000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00153-009-0152-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,9,24]]},"references-count":11,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2009,12]]}},"alternative-id":["152"],"URL":"https:\/\/doi.org\/10.1007\/s00153-009-0152-4","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"value":"0933-5846","type":"print"},{"value":"1432-0665","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,9,24]]}}}