{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T04:45:47Z","timestamp":1773809147494,"version":"3.50.1"},"reference-count":37,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T00:00:00Z","timestamp":1624924800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000181","name":"Air Force Office of Scientific Research","doi-asserted-by":"crossref","award":["FA9550-19-1-017"],"award-info":[{"award-number":["FA9550-19-1-017"]}],"id":[{"id":"10.13039\/100000181","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2022,1]]},"DOI":"10.1007\/s10472-021-09762-2","type":"journal-article","created":{"date-parts":[[2021,6,29]],"date-time":"2021-06-29T08:02:40Z","timestamp":1624953760000},"page":"3-29","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas"],"prefix":"10.1007","volume":"90","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5821-5117","authenticated-orcid":false,"given":"K.","family":"Subramani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Piotr","family":"Wojciechowski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,6,29]]},"reference":[{"issue":"3","key":"9762_CR1","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"B Aspvall","year":"1979","unstructured":"Aspvall, B., Plass, M. F., Tarjan, R.: A linear-time algorithm for testing the truth of certain quantified boolean formulas. Inf. Process. Lett. 8(3), 121\u2013123 (1979)","journal-title":"Inf. Process. Lett."},{"issue":"3","key":"9762_CR2","doi-asserted-by":"publisher","first-page":"121","DOI":"10.1016\/0020-0190(79)90002-4","volume":"8","author":"BMF Aspvall","year":"1979","unstructured":"Aspvall, B.M.F., Plass, R.E.T.: A linear time algorithm for testing the truth of certain quantified boolean formulas. Inf. Process. Lett. 8(3), 121\u2013123 (1979)","journal-title":"Inf. Process. Lett."},{"key":"9762_CR3","doi-asserted-by":"crossref","unstructured":"Balcarek, J., Fiser, P., Schmidt, J.: Test Patterns Compression Technique Based on a Dedicated Sat-Based ATPG. In: L\u00f3pez, S. (ed.) 13Th Euromicro Conference on Digital System Design, Architectures, Methods and Tools, DSD 2010, 1-3 September 2010, Lille, France. Computer Society, pp 805\u2013808. IEEE (2010)","DOI":"10.1109\/DSD.2010.111"},{"key":"9762_CR4","doi-asserted-by":"crossref","unstructured":"Balcarek, J., Fiser, P., Schmidt, J.: Techniques for Sat-Based Constrained Test Pattern Generation. In: 14Th Euromicro Conference on Digital System Design, Architectures, Methods and Tools, DSD 2011, August 31 - September 2, 2011, Oulu, Finland, pp. 360\u2013366. IEEE Computer Society (2011)","DOI":"10.1109\/DSD.2011.50"},{"issue":"1","key":"9762_CR5","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0890-5401(92)90056-L","volume":"96","author":"P Berman","year":"1992","unstructured":"Berman, P., Schnitger, G.: On the complexity of approximating the independent set problem. Inf. Comput. 96(1), 77\u201394 (1992)","journal-title":"Inf. Comput."},{"issue":"3","key":"9762_CR6","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1051\/ita\/2010018","volume":"44","author":"H B\u00f6ckenhauer","year":"2010","unstructured":"B\u00f6ckenhauer, H., Forisek, M., Oravec, J., Steffen, B., Steinh\u00f6fel, K., Steinov\u00e1, M.: The uniform minimum-ones 2sat problem and its application to haplotype classification. RAIRO - Theor. Inf. and Applic. 44(3), 363\u2013377 (2010)","journal-title":"RAIRO - Theor. Inf. and Applic."},{"issue":"12","key":"9762_CR7","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/2043174.2043195","volume":"54","author":"G Brewka","year":"2011","unstructured":"Brewka, G., Eiter, T., Truszczynski, M.: Answer set programming at a glance. Commun. ACM 54(12), 92\u2013103 (2011)","journal-title":"Commun. ACM"},{"key":"9762_CR8","doi-asserted-by":"crossref","unstructured":"Buresh-Oppenheim, J., Mitchell, D. G.: Minimum Witnesses for Unsatisfiable 2Cnfs. In: SAT, pp. 42\u201347 (2006)","DOI":"10.1007\/11814948_6"},{"key":"9762_CR9","doi-asserted-by":"publisher","DOI":"10.1002\/9781118033166","volume-title":"Optimization Methods for Logical Inference. Series in Discrete Mathematics and Optimization","author":"V Chandru","year":"1999","unstructured":"Chandru, V., Hooker, J. N.: Optimization Methods for Logical Inference. Series in Discrete Mathematics and Optimization. Wiley, New York (1999)"},{"key":"9762_CR10","unstructured":"Chen, J., Lu, S., Sze, S. H., Zhang, F.: Improved algorithms for path, matching, and packing problems. In: Proceedings of the Eighteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA \u201907, pp 298\u2013307. Society for Industrial and Applied Mathematics, USA (2007)"},{"key":"9762_CR11","unstructured":"Colmerauer, A.: Logic Programming and Its Applications, chap. Theoretical Model of prologII, pp. 181\u2013200. Ablex Series in Artificial Intelligence Ablex Publishing Corporation (1986)"},{"key":"9762_CR12","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2009","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press, Cambridge (2009)","edition":"3rd edn."},{"key":"9762_CR13","unstructured":"Dorsch, R., Wunderlich, H.: Tailoring ATPG for embedded testing. In: Proceedings IEEE International Test Conference 2001, Baltimore, MD, USA, 30 October - 1 November 2001, pp. 530\u2013537. IEEE Computer Society (2001)"},{"issue":"3","key":"9762_CR14","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0743-1066(84)90014-1","volume":"1","author":"WF Dowling","year":"1984","unstructured":"Dowling, W. F., Gallier, J. H.: Linear-time algorithms for testing the satisfiability of propositional Horn formulae. J. Log. Program. 1(3), 267\u2013284 (1984)","journal-title":"J. Log. Program."},{"issue":"3","key":"9762_CR15","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1016\/j.tcs.2005.10.005","volume":"351","author":"MR Fellows","year":"2006","unstructured":"Fellows, M. R., Szeider, S., Wrightson, G.: On finding short resolution refutations and small unsatisfiable subsets. Theor. Comput. Sci. 351(3), 351\u2013359 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"9762_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16533-7","volume-title":"Exact Exponential Algorithms","author":"FV Fomin","year":"2010","unstructured":"Fomin, F. V., Kratsch, D.: Exact Exponential Algorithms, 1st edn. Springer, Berlin (2010)","edition":"1st edn."},{"key":"9762_CR17","volume-title":"Kernelization: Theory of Parameterized Preprocessing","author":"FV Fomin","year":"2019","unstructured":"Fomin, F. V., Lokshtanov, D., Saurabh, S., Zehavi, M.: Kernelization: Theory of Parameterized Preprocessing. Cambridge University Press, Cambridge (2019)"},{"issue":"2-3","key":"9762_CR18","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(85)90144-6","volume":"39","author":"A Haken","year":"1985","unstructured":"Haken, A.: The intractability of resolution. Theor. Comput. Sci. 39 (2-3), 297\u2013308 (1985)","journal-title":"Theor. Comput. Sci."},{"key":"9762_CR19","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/BFb0029974","volume":"1295","author":"K Iwama","year":"1997","unstructured":"Iwama, K.: Complexity of finding short resolution proofs. Lect. Notes Comput. Sci 1295, 309\u2013319 (1997)","journal-title":"Lect. Notes Comput. Sci"},{"key":"9762_CR20","unstructured":"Iwama, K., Miyano, E.: Intractability of read-once resolution. In: Proceedings of the 10th Annual Conference on Structure in Complexity Theory (SCTC \u201995), pp 29\u201336. IEEE Computer Society Press, USA (1995)"},{"key":"9762_CR21","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1016\/0743-1066(94)90033-7","volume":"s 19\u201320","author":"J Jaffar","year":"1994","unstructured":"Jaffar, J., Maher, M.: Constraint logic programming: a survey. J. Logic Programm. s 19\u201320, 503\u2013581 (1994)","journal-title":"J. Logic Programm."},{"issue":"3","key":"9762_CR22","first-page":"13","volume":"37","author":"T Janhunen","year":"2016","unstructured":"Janhunen, T., Niemel\u00e4, I.: The answer set programming paradigm. AI Mag. 37(3), 13\u201324 (2016)","journal-title":"AI Mag."},{"issue":"3","key":"9762_CR23","first-page":"317","volume":"1","author":"V Kann","year":"1994","unstructured":"Kann, V.: Polynomially bounded minimization problems that are hard to approximate. Nordic J. of Comput. 1(3), 317\u2013331 (1994)","journal-title":"Nordic J. of Comput."},{"key":"9762_CR24","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1016\/j.tcs.2018.02.002","volume":"729","author":"H Kleine B\u00fcning","year":"2018","unstructured":"Kleine B\u00fcning, H., Wojciechowski, P. J., Subramani, K.: Finding read-once resolution refutations in systems of 2CNF clauses. Theor. Comput. Sci. 729, 42\u201356 (2018)","journal-title":"Theor. Comput. Sci."},{"key":"9762_CR25","doi-asserted-by":"crossref","unstructured":"Kleine B\u00fcning, H., Wojciechowski, P. J., Subramani, K.: On the application of restricted cutting plane systems to horn constraint systems. In: The 12Th International Symposium on Frontiers of Combining Systems, London, United Kingdom, September 4-6, 2019, Proceedings, pp. 149\u2013164 (2019)","DOI":"10.1007\/978-3-030-29007-8_9"},{"key":"9762_CR26","doi-asserted-by":"crossref","unstructured":"Kleine B\u00fcning, H., Wojciechowski, P. J., Subramani, K.: Read-Once Resolutions in Horn Formulas. In: Frontiers in Algorithmics - 13Th International Workshop, FAW 2019, Sanya, China, April 29 - May 3, 2019, Proceedings, pp. 100\u2013110 (2019)","DOI":"10.1007\/978-3-030-18126-0_9"},{"key":"9762_CR27","unstructured":"Kratsch, D., McConnell, R. M., Mehlhorn, K., Spinrad, J.: Certifying Algorithms for Recognizing Interval Graphs and Permutation Graphs. In: SODA, pp. 158\u2013167 (2003)"},{"issue":"1","key":"9762_CR28","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1145\/322047.322059","volume":"25","author":"HR Lewis","year":"1978","unstructured":"Lewis, H. R.: Renaming a set of clauses as a horn set. J. ACM 25 (1), 134\u2013135 (1978)","journal-title":"J. ACM"},{"issue":"3","key":"9762_CR29","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/s10601-016-9257-7","volume":"22","author":"Y Lierler","year":"2017","unstructured":"Lierler, Y.: What is answer set programming to propositional satisfiability. Constraints An Int. J. 22(3), 307\u2013337 (2017)","journal-title":"Constraints An Int. J."},{"key":"9762_CR30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-24658-7","volume-title":"Answer Set Programming","author":"V Lifschitz","year":"2019","unstructured":"Lifschitz, V.: Answer Set Programming. Springer, Berlin (2019)"},{"key":"9762_CR31","unstructured":"Naor, M., Schulman, L. J., Srinivasan, A.: Splitters and near-optimal derandomization. In: Proceedings of IEEE 36th Annual Foundations of Computer Science, pp. 182\u2013191 (1995)"},{"key":"9762_CR32","unstructured":"Orponen, P., Mannila, H.: On approximation preserving reductions: Complete problems and robust measures. Tech. rep., Department of Computer Science University of Helsinki (1987)"},{"key":"9762_CR33","volume-title":"Computational Complexity","author":"CH Papadimitriou","year":"1994","unstructured":"Papadimitriou, C. H.: Computational Complexity. Addison-Wesley, New York (1994)"},{"key":"9762_CR34","unstructured":"Rushby, J. M.: Tutorial: Automated Formal Methods with Pvs, Sal, and Yices. In: SEFM, p. 262 (2006)"},{"issue":"2-3","key":"9762_CR35","first-page":"105","volume":"32","author":"T Schaub","year":"2018","unstructured":"Schaub, T., Woltran, S.: Answer set programming unleashed!. KI 32(2-3), 105\u2013108 (2018)","journal-title":"KI"},{"key":"9762_CR36","unstructured":"Subramani, K., Wojciechowski, P.: Finding Read-Once Refutations in 2Cnf Formulas and Variants - a Parameterized Perspective. In: The 16th International Symposium on Artificial Intelligence and Mathematics (2020)"},{"key":"9762_CR37","doi-asserted-by":"crossref","unstructured":"Szeider, S.: NP-completeness of refutability by literal-once resolution. In: Automated Reasoning, First International Joint Conference, IJCAR 2001, Siena, Italy, June 18-23, 2001, Proceedings, vol. 2083, pp 168\u2013181 (2001)","DOI":"10.1007\/3-540-45744-5_13"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-021-09762-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10472-021-09762-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-021-09762-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,19]],"date-time":"2022-01-19T00:16:37Z","timestamp":1642551397000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10472-021-09762-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,29]]},"references-count":37,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,1]]}},"alternative-id":["9762"],"URL":"https:\/\/doi.org\/10.1007\/s10472-021-09762-2","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"value":"1012-2443","type":"print"},{"value":"1573-7470","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,29]]},"assertion":[{"value":"10 June 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 June 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}