{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,16]],"date-time":"2025-10-16T06:47:06Z","timestamp":1760597226114,"version":"3.41.0"},"reference-count":31,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2006,1]]},"abstract":"<jats:p>\n            DPLL and resolution are two popular methods for solving the problem of propositional satisfiability. Rather than algorithms, they are families of algorithms, as their behavior depends on some choices they face during execution: DPLL depends on the choice of the literal to branch on; resolution depends on the choice of the pair of clauses to resolve at each step. The complexity of making the optimal choice is analyzed in this article. Extending previous results, we prove that choosing the optimal literal to branch on in DPLL is \u0394\n            <jats:sup>\n              <jats:italic>p<\/jats:italic>\n            <\/jats:sup>\n            <jats:sub>2<\/jats:sub>\n            [log\n            <jats:italic>n<\/jats:italic>\n            ]-hard, and becomes NP\n            <jats:sup>PP<\/jats:sup>\n            -hard if branching is only allowed on a subset of variables. Optimal choice in regular resolution is both NP-hard and coNP-hard. The problem of determining the size of the optimal proofs is also analyzed: it is coNP-hard for DPLL, and \u0394\n            <jats:sup>\n              <jats:italic>p<\/jats:italic>\n            <\/jats:sup>\n            <jats:sub>2<\/jats:sub>\n            [log\n            <jats:italic>n<\/jats:italic>\n            ]-hard if a conjecture we make is true. This problem is coNP-hard for regular resolution.\n          <\/jats:p>","DOI":"10.1145\/1119439.1119442","type":"journal-article","created":{"date-parts":[[2006,5,8]],"date-time":"2006-05-08T16:09:20Z","timestamp":1147104560000},"page":"84-107","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Complexity results on DPLL and resolution"],"prefix":"10.1145","volume":"7","author":[{"given":"Paolo","family":"Liberatore","sequence":"first","affiliation":[{"name":"Universit\u00e0 di Roma \u201cLa Sapienza\u201d, Rome, Italy"}]}],"member":"320","published-online":{"date-parts":[[2006,1]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.2307\/2694916"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the Forty-Second Annual Symposium on the Foundations of Computer Science (FOCS","author":"Alekhnovich M.","year":"2001","unstructured":"Alekhnovich , M. and Razborov , A . 2001. Resolution is not automatizable unless W{P} is tractable . In Proceedings of the Forty-Second Annual Symposium on the Foundations of Computer Science (FOCS 2001 ). 210--219.]] Alekhnovich, M. and Razborov, A. 2001. Resolution is not automatizable unless W{P} is tractable. In Proceedings of the Forty-Second Annual Symposium on the Foundations of Computer Science (FOCS 2001). 210--219.]]"},{"key":"e_1_2_1_3_1","volume-title":"Proceedings of the Forty-Third Annual Symposium on the Foundations of Computer Science (FOCS","author":"Alekhnovich M.","year":"2002","unstructured":"Alekhnovich , M. and Razborov , A . 2002. Satisfiability, branch-width and Tseitin tautologies . In Proceedings of the Forty-Third Annual Symposium on the Foundations of Computer Science (FOCS 2002 ). 593--603.]] Alekhnovich, M. and Razborov, A. 2002. Satisfiability, branch-width and Tseitin tautologies. In Proceedings of the Forty-Third Annual Symposium on the Foundations of Computer Science (FOCS 2002). 593--603.]]"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700369156"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00493-004-0036-5"},{"key":"e_1_2_1_6_1","first-page":"1","article-title":"Non-automatizability of bounded-depth Frege proofs","volume":"13","author":"Bonet M.","year":"2004","unstructured":"Bonet , M. , Domingo , C. , Gavald\u00e0 , R. , Maciel , A. , and Pitassi , T. 2004 . Non-automatizability of bounded-depth Frege proofs . In Proceedings of the Computational Complexity 13 , 1 -- 2 , 47--68.]] Bonet, M., Domingo, C., Gavald\u00e0, R., Maciel, A., and Pitassi, T. 2004. Non-automatizability of bounded-depth Frege proofs. In Proceedings of the Computational Complexity 13, 1--2, 47--68.]]","journal-title":"Proceedings of the Computational Complexity"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539799352474"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539798353230"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2566-9_4"},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the Thirteenth International Conference on Computer Aided Verification (CAV","author":"Copty F.","year":"2001","unstructured":"Copty , F. , Fix , L. , Fraer , R. , Giunchiglia , E. , Kamhi , G. , Tacchella , A. , and Vardi , M . 2001. Benefits of bounded model checking at an industrial setting . In Proceedings of the Thirteenth International Conference on Computer Aided Verification (CAV 2001 ). 436--453.]] Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., and Vardi, M. 2001. Benefits of bounded model checking at an industrial setting. In Proceedings of the Thirteenth International Conference on Computer Aided Verification (CAV 2001). 436--453.]]"},{"volume-title":"Proceedings of the Twelfth National Conference on Artificial Intelligence (AAAI'94)","author":"Crawford J.","key":"e_1_2_1_11_1","unstructured":"Crawford , J. and Baker , A . 1994. Experimental results on the application of satisfiability algorithms to scheduling problems . In Proceedings of the Twelfth National Conference on Artificial Intelligence (AAAI'94) . 1092--1097.]] Crawford, J. and Baker, A. 1994. Experimental results on the application of satisfiability algorithms to scheduling problems. In Proceedings of the Twelfth National Conference on Artificial Intelligence (AAAI'94). 1092--1097.]]"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/368273.368557"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/321033.321034"},{"volume-title":"Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97)","author":"Ernst M.","key":"e_1_2_1_14_1","unstructured":"Ernst , M. , Millstein , T. , and Weld , D . 1997. Automatic SAT-compilation of planning problems . In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97) . 1169--1176.]] Ernst, M., Millstein, T., and Weld, D. 1997. Automatic SAT-compilation of planning problems. In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97). 1169--1176.]]"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/646333.687785"},{"volume-title":"Proceedings of the Fifteenth National Conference on Artificial Intelligence (AAAI'98)","author":"Giunchiglia E.","key":"e_1_2_1_16_1","unstructured":"Giunchiglia , E. , Massarotto , A. , and Sebastiani , R . 1998. Act, and the rest will follow: Exploiting determinism in planning as satisfiability . In Proceedings of the Fifteenth National Conference on Artificial Intelligence (AAAI'98) . 948--953.]] Giunchiglia, E., Massarotto, A., and Sebastiani, R. 1998. Act, and the rest will follow: Exploiting determinism in planning as satisfiability. In Proceedings of the Fifteenth National Conference on Artificial Intelligence (AAAI'98). 948--953.]]"},{"volume-title":"Proceedings of the Sixth Conference of the Italian Association for Artificial Intelligence (AI&ast;IA'99)","author":"Giunchiglia E.","key":"e_1_2_1_17_1","unstructured":"Giunchiglia , E. and Sebastiani , R . 1999. Applying the Davis-Putnam procedure to non-clausal formulas . In Proceedings of the Sixth Conference of the Italian Association for Artificial Intelligence (AI&ast;IA'99) . 84--94.]] Giunchiglia, E. and Sebastiani, R. 1999. Applying the Davis-Putnam procedure to non-clausal formulas. In Proceedings of the Sixth Conference of the Italian Association for Artificial Intelligence (AI&ast;IA'99). 84--94.]]"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(85)90144-6"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/645726.667214"},{"volume-title":"Proceedings of the Tenth Annual Structure in Complexity Theory Conference (CoCo'95)","author":"Iwama K.","key":"e_1_2_1_20_1","unstructured":"Iwama , K. and Miyano , E . 1995. Intractability of read-once resolution . In Proceedings of the Tenth Annual Structure in Complexity Theory Conference (CoCo'95) . 29--36.]] Iwama, K. and Miyano, E. 1995. Intractability of read-once resolution. In Proceedings of the Tenth Annual Structure in Complexity Theory Conference (CoCo'95). 29--36.]]"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(99)00097-1"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622797.1622798"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1006326723002"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97)","author":"Min Li C.","year":"1997","unstructured":"Min Li , C. and Anbulagan . 1997 . Heuristics based on unit propagation for satisfiability problems . In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97) . 366--371.]] Min Li, C. and Anbulagan. 1997. Heuristics based on unit propagation for satisfiability problems. In Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI'97). 366--371.]]"},{"key":"e_1_2_1_25_1","volume-title":"Proceedings of the Fourteenth European Conference on Artificial Intelligence (ECAI","author":"Min Li C.","year":"2000","unstructured":"Min Li , C. and G\u00e9rard , S . 2000. On the limit of branching rules for hard random unsatisfiable 3-SAT . In Proceedings of the Fourteenth European Conference on Artificial Intelligence (ECAI 2000 ). 98--102.]] Min Li, C. and G\u00e9rard, S. 2000. On the limit of branching rules for hard random unsatisfiable 3-SAT. In Proceedings of the Fourteenth European Conference on Artificial Intelligence (ECAI 2000). 98--102.]]"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/321250.321253"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/647769.734091"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1137\/0220053"},{"volume-title":"Studies in Constructive Mathematics and Mathematical Logic","author":"Tseitin G.","key":"e_1_2_1_29_1","unstructured":"Tseitin , G. 1970. On the complexity of derivation in propositional calculus . In Studies in Constructive Mathematics and Mathematical Logic , A. Slisenko, Ed. Vol. II. Consultants Bureau , New York, NY , 115--125.]] Tseitin, G. 1970. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, A. Slisenko, Ed. Vol. II. Consultants Bureau, New York, NY, 115--125.]]"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/7531.8928"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1137\/0219058"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1119439.1119442","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1119439.1119442","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T16:08:18Z","timestamp":1750262898000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1119439.1119442"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,1]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2006,1]]}},"alternative-id":["10.1145\/1119439.1119442"],"URL":"https:\/\/doi.org\/10.1145\/1119439.1119442","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2006,1]]},"assertion":[{"value":"2006-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}