{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:09:01Z","timestamp":1750306141713,"version":"3.41.0"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"3","license":[{"start":{"date-parts":[[2017,7,31]],"date-time":"2017-07-31T00:00:00Z","timestamp":1501459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100002428","name":"FWF Austrian Science Fund","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2017,7,31]]},"abstract":"<jats:p>In many practical settings it is useful to find a small unsatisfiable subset of a given unsatisfiable set of constraints. We study this problem from a parameterized complexity perspective, taking the size of the unsatisfiable subset as the natural parameter where the set of constraints is either (i) given a set of clauses, i.e., a formula in conjunctive normal Form (CNF), or (ii) as an instance of the Constraint Satisfaction Problem (CSP).<\/jats:p>\n          <jats:p>\n            In general, the problem is fixed-parameter\n            <jats:italic>in<\/jats:italic>\n            tractable. For an instance of the propositional satisfiability problem (SAT), it was known to be W[1]-complete. We establish A[2]-completeness for CSP instances, where A[2]-hardness prevails already for the Boolean case.\n          <\/jats:p>\n          <jats:p>With these fixed-parameter intractability results for the general case in mind, we consider various restricted classes of inputs and draw a detailed complexity landscape. It turns out that often Boolean CSP and CNF formulas behave similarly, but we also identify notable exceptions to this rule.<\/jats:p>\n          <jats:p>The main part of this article is dedicated to classes of inputs that are induced by Boolean constraint languages that Schaefer [1978] identified as the maximal constraint languages with a tractable satisfiability problem. We show that for the CSP setting, the problem of finding small unsatisfiable subsets remains fixed-parameter intractable for all Schaefer languages for which the problem is non-trivial. We show that this is also the case for CNF formulas with the exception of the class of bijunctive (Krom) formulas, which allows for an identification of a small unsatisfiable subset in polynomial time.<\/jats:p>\n          <jats:p>In addition, we consider various restricted classes of inputs with bounds on the maximum number of times that a variable occurs (the degree), bounds on the arity of constraints, and bounds on the domain size. For the case of CNF formulas, we show that restricting the degree is enough to obtain fixed-parameter tractability, whereas for the case of CSP instances, one needs to restrict the degree, the arity, and the domain size simultaneously to establish fixed-parameter tractability.<\/jats:p>\n          <jats:p>Finally, we relate the problem of finding small unsatisfiable subsets of a set of constraints to the problem of identifying whether a given variable-value assignment is entailed or forbidden already by a small subset of constraints. Moreover, we use the connection between the two problems to establish similar parameterized complexity results also for the latter problem.<\/jats:p>","DOI":"10.1145\/3091528","type":"journal-article","created":{"date-parts":[[2017,8,14]],"date-time":"2017-08-14T12:24:33Z","timestamp":1502713473000},"page":"1-46","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["On the Parameterized Complexity of Finding Small Unsatisfiable Subsets of CNF Formulas and CSP Instances"],"prefix":"10.1145","volume":"18","author":[{"given":"Ronald De","family":"Haan","sequence":"first","affiliation":[{"name":"Algorithms and Complexity Group, TU Wien, Vienna, Austria"}]},{"given":"Iyad","family":"Kanj","sequence":"additional","affiliation":[{"name":"School of Computing, DePaul University, Chicago, IL, United States"}]},{"given":"Stefan","family":"Szeider","sequence":"additional","affiliation":[{"name":"Algorithms and Complexity Group, TU Wien, Vienna, Austria"}]}],"member":"320","published-online":{"date-parts":[[2017,8,11]]},"reference":[{"doi-asserted-by":"publisher","key":"e_1_2_1_1_1","DOI":"10.1007\/s00453-006-1214-1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_2_1","DOI":"10.1016\/0097-3165(86)90060-9"},{"volume-title":"Computational Complexity\u2014A Modern Approach","author":"Arora Sanjeev","unstructured":"Sanjeev Arora and Boaz Barak . 2009. Computational Complexity\u2014A Modern Approach . Cambridge University Press . I--XXIV, 1--579 pages. Sanjeev Arora and Boaz Barak. 2009. Computational Complexity\u2014A Modern Approach. Cambridge University Press. I--XXIV, 1--579 pages.","key":"e_1_2_1_3_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.1007\/978-3-319-21668-3_5"},{"doi-asserted-by":"publisher","key":"e_1_2_1_5_1","DOI":"10.5555\/2350156.2350163"},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.3233\/SAT190094"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (Lecture Notes in Computer Science), Armin Biere and Carla P. Gomes (Eds.)","volume":"4121","author":"Buresh-Oppenheim Joshua","unstructured":"Joshua Buresh-Oppenheim and David G. Mitchell . 2006. Minimum witnesses for unsatisfiable 2CNFs . In Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (Lecture Notes in Computer Science), Armin Biere and Carla P. Gomes (Eds.) , Vol. 4121 . 42--47. Joshua Buresh-Oppenheim and David G. Mitchell. 2006. Minimum witnesses for unsatisfiable 2CNFs. In Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (Lecture Notes in Computer Science), Armin Biere and Carla P. Gomes (Eds.), Vol. 4121. 42--47."},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1016\/S0022-0000(03)00075-8"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1016\/j.ic.2005.05.001"},{"doi-asserted-by":"publisher","key":"e_1_2_1_10_1","DOI":"10.1016\/j.jcss.2006.04.007"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1007\/978-3-642-30891-8_11"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.5555\/2016945.2016964"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1145\/2752952.2752961"},{"doi-asserted-by":"publisher","key":"e_1_2_1_14_1","DOI":"10.1007\/978-3-319-21275-3"},{"doi-asserted-by":"publisher","key":"e_1_2_1_15_1","DOI":"10.5555\/1622810.1622817"},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.1007\/978-3-642-39071-5_28"},{"key":"e_1_2_1_17_1","volume-title":"Technical Report 1304.5479. arXiv.org. (updated version of de Haan et al.","author":"de Haan Ronald","year":"2013","unstructured":"Ronald de Haan , Iyad Kanj , and Stefan Szeider . 2013b. Local Backbones . Technical Report 1304.5479. arXiv.org. (updated version of de Haan et al. 2013 a). Ronald de Haan, Iyad Kanj, and Stefan Szeider. 2013b. Local Backbones. Technical Report 1304.5479. arXiv.org. (updated version of de Haan et al. 2013a)."},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1109\/ICTAI.2014.72"},{"doi-asserted-by":"publisher","key":"e_1_2_1_19_1","DOI":"10.1016\/0743-1066(84)90014-1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.1137\/S0097539792228228"},{"doi-asserted-by":"publisher","key":"e_1_2_1_21_1","DOI":"10.1016\/0304-3975(94)00097-3"},{"doi-asserted-by":"publisher","key":"e_1_2_1_22_1","DOI":"10.1007\/978-1-4612-0515-9"},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1007\/978-1-4471-5559-1"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI\u201901)","author":"Dubois Olivier","year":"2001","unstructured":"Olivier Dubois and Gilles Dequen . 2001 . A backbone-search heuristic for efficient solving of hard 3-SAT formulae . In Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI\u201901) , Bernhard Nebel (Ed.). 248--253. Olivier Dubois and Gilles Dequen. 2001. A backbone-search heuristic for efficient solving of hard 3-SAT formulae. In Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI\u201901), Bernhard Nebel (Ed.). 248--253."},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.1016\/j.tcs.2008.09.065"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1016\/j.tcs.2005.10.005"},{"key":"e_1_2_1_27_1","series-title":"An EATCS Series","volume-title":"Parameterized Complexity Theory. Texts in Theoretical Computer Science","author":"Flum J\u00f6rg","unstructured":"J\u00f6rg Flum and Martin Grohe . 2006. Parameterized Complexity Theory. Texts in Theoretical Computer Science . An EATCS Series , Vol. XIV . Springer-Verlag , Berlin . J\u00f6rg Flum and Martin Grohe. 2006. Parameterized Complexity Theory. Texts in Theoretical Computer Science. An EATCS Series, Vol. XIV. Springer-Verlag, Berlin."},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1016\/0166-218X(93)90045-P"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.1007\/978-3-642-23786-7_24"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.1093\/comjnl\/bxm056"},{"doi-asserted-by":"publisher","key":"e_1_2_1_31_1","DOI":"10.1007\/978-3-642-35843-2_20"},{"key":"e_1_2_1_32_1","volume-title":"Proceedings of the 17th European Conference on Artificial Intelligence (ECAI 2006)","volume":"141","author":"Hemery Fred","year":"2006","unstructured":"Fred Hemery , Christophe Lecoutre , Lakhdar Sais , and Fr\u00e9d\u00e9ric Boussemart . 2006 . Extracting MUCs from constraint networks . In Proceedings of the 17th European Conference on Artificial Intelligence (ECAI 2006) (Frontiers in Artificial Intelligence and Applications) , Vol. 141 . 113--117. Fred Hemery, Christophe Lecoutre, Lakhdar Sais, and Fr\u00e9d\u00e9ric Boussemart. 2006. Extracting MUCs from constraint networks. In Proceedings of the 17th European Conference on Artificial Intelligence (ECAI 2006) (Frontiers in Artificial Intelligence and Applications), Vol. 141. 113--117."},{"key":"e_1_2_1_33_1","volume-title":"Symposium on Theoretical Aspects of Computer Science, Thomas Schwentick and Christoph D\u00fcrr (Eds.)","volume":"9","author":"Hertli Timon","year":"2011","unstructured":"Timon Hertli , Robin A. Moser , and Dominik Scheder . 2011 . Improving PPSZ for 3-SAT using critical variables . In Symposium on Theoretical Aspects of Computer Science, Thomas Schwentick and Christoph D\u00fcrr (Eds.) , Vol. 9 . Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 237--248. Timon Hertli, Robin A. Moser, and Dominik Scheder. 2011. Improving PPSZ for 3-SAT using critical variables. In Symposium on Theoretical Aspects of Computer Science, Thomas Schwentick and Christoph D\u00fcrr (Eds.), Vol. 9. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, 237--248."},{"key":"e_1_2_1_34_1","volume-title":"SAT2000: Highlights of Satisfiability Research in the year","author":"Holger","year":"2000","unstructured":"Holger H. Hoos and Thomas St\u00fctzle. 2000. SATLIB: An online resource for research on SAT . In SAT2000: Highlights of Satisfiability Research in the year 2000 , Ian Gent, Hans van Maaren, and Toby Walsh (Eds.). Kluwer Academic, 283--292. Holger H. Hoos and Thomas St\u00fctzle. 2000. SATLIB: An online resource for research on SAT. In SAT2000: Highlights of Satisfiability Research in the year 2000, Ian Gent, Hans van Maaren, and Toby Walsh (Eds.). Kluwer Academic, 283--292."},{"doi-asserted-by":"publisher","key":"e_1_2_1_35_1","DOI":"10.1007\/s00453-007-9008-7"},{"doi-asserted-by":"publisher","key":"e_1_2_1_36_1","DOI":"10.5555\/3102787.3102801"},{"doi-asserted-by":"publisher","key":"e_1_2_1_37_1","DOI":"10.1006\/jcss.2001.1774"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 13th AAAI Conference on Artificial Intelligence (AAAI\u201996)","author":"Kautz Henry","year":"1996","unstructured":"Henry Kautz and Bart Selman . 1996 . Pushing the envelope: Planning, propositional logic, and stochastic search . In Proceedings of the 13th AAAI Conference on Artificial Intelligence (AAAI\u201996) . AAAI Press, 1194--1201. Henry Kautz and Bart Selman. 1996. Pushing the envelope: Planning, propositional logic, and stochastic search. In Proceedings of the 13th AAAI Conference on Artificial Intelligence (AAAI\u201996). AAAI Press, 1194--1201."},{"key":"e_1_2_1_39_1","volume-title":"Proceedings of the 20th National Conference on Artificial Intelligence and the 17th Innovative Applications of Artificial Intelligence Conference (AAAI","author":"Kilby Philip","year":"2005","unstructured":"Philip Kilby , John K. Slaney , Sylvie Thi\u00e9baux , and Toby Walsh . 2005 . Backbones and backdoors in satisfiability . In Proceedings of the 20th National Conference on Artificial Intelligence and the 17th Innovative Applications of Artificial Intelligence Conference (AAAI 2005). 1368--1373. Philip Kilby, John K. Slaney, Sylvie Thi\u00e9baux, and Toby Walsh. 2005. Backbones and backdoors in satisfiability. In Proceedings of the 20th National Conference on Artificial Intelligence and the 17th Innovative Applications of Artificial Intelligence Conference (AAAI 2005). 1368--1373."},{"doi-asserted-by":"publisher","key":"e_1_2_1_41_1","DOI":"10.1109\/CCC.2000.856741"},{"doi-asserted-by":"publisher","key":"e_1_2_1_43_1","DOI":"10.1093\/comjnl\/bxm003"},{"doi-asserted-by":"publisher","key":"e_1_2_1_44_1","DOI":"10.1016\/j.artint.2004.11.002"},{"volume-title":"Proceedings of SAT 2004 (7th International Conference on Theory and Applications of Satisfiability Testing).","author":"Lynce In\u00eas","unstructured":"In\u00eas Lynce and Jo\u00e3o P . Marques Silva. 2004. On computing minimum unsatisfiable cores . In Proceedings of SAT 2004 (7th International Conference on Theory and Applications of Satisfiability Testing). In\u00eas Lynce and Jo\u00e3o P. Marques Silva. 2004. On computing minimum unsatisfiable cores. In Proceedings of SAT 2004 (7th International Conference on Theory and Applications of Satisfiability Testing).","key":"e_1_2_1_45_1"},{"key":"e_1_2_1_46_1","volume-title":"Computing minimally unsatisfiable subformulas: State of the art and future directions. Journal of Multiple-Valued Logic and Soft Computing","author":"Marques-Silva Jo\u00e3o","year":"2012","unstructured":"Jo\u00e3o Marques-Silva . 2012. Computing minimally unsatisfiable subformulas: State of the art and future directions. Journal of Multiple-Valued Logic and Soft Computing ( 2012 ), 163--183. Jo\u00e3o Marques-Silva. 2012. Computing minimally unsatisfiable subformulas: State of the art and future directions. Journal of Multiple-Valued Logic and Soft Computing (2012), 163--183."},{"doi-asserted-by":"publisher","key":"e_1_2_1_47_1","DOI":"10.1109\/SWAT.1972.29"},{"doi-asserted-by":"publisher","key":"e_1_2_1_48_1","DOI":"10.1093\/acprof:oso\/9780198566076.001.0001"},{"volume-title":"Computational Complexity","author":"Papadimitriou Christos H.","unstructured":"Christos H. Papadimitriou . 1994. Computational Complexity . Addison-Wesley . Christos H. Papadimitriou. 1994. Computational Complexity. Addison-Wesley.","key":"e_1_2_1_49_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_50_1","DOI":"10.1006\/jcss.1999.1626"},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of the 14th National Conference on Artificial Intelligence (AAAI\u201997)","author":"Parkes Andrew J.","year":"1997","unstructured":"Andrew J. Parkes . 1997 . Clustering at the phase transition . In Proceedings of the 14th National Conference on Artificial Intelligence (AAAI\u201997) . AAAI Press, 340--345. Andrew J. Parkes. 1997. Clustering at the phase transition. In Proceedings of the 14th National Conference on Artificial Intelligence (AAAI\u201997). AAAI Press, 340--345."},{"volume-title":"Efficiency and stability of hypergraph SAT algorithms","author":"Prelotani Daniele","unstructured":"Daniele Prelotani . 1996. Efficiency and stability of hypergraph SAT algorithms . In Cliques, Coloring and Satisfiability, David S. Johnson and Michael A. Trick (Eds.). AMS , 479--498. Daniele Prelotani. 1996. Efficiency and stability of hypergraph SAT algorithms. In Cliques, Coloring and Satisfiability, David S. Johnson and Michael A. Trick (Eds.). AMS, 479--498.","key":"e_1_2_1_52_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_54_1","DOI":"10.1016\/j.jcss.2009.04.003"},{"doi-asserted-by":"publisher","key":"e_1_2_1_55_1","DOI":"10.1145\/800133.804350"},{"doi-asserted-by":"publisher","key":"e_1_2_1_56_1","DOI":"10.1016\/0010-4655(96)00062-8"},{"volume-title":"Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI\u201901)","author":"John","unstructured":"John K. Slaney and Toby Walsh. 2001. Backbones in optimization and approximation . In Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI\u201901) , Bernhard Nebel (Ed.). 254--259. John K. Slaney and Toby Walsh. 2001. Backbones in optimization and approximation. In Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI\u201901), Bernhard Nebel (Ed.). 254--259.","key":"e_1_2_1_57_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_58_1","DOI":"10.1109\/TCBB.2006.52"},{"doi-asserted-by":"publisher","key":"e_1_2_1_60_1","DOI":"10.1016\/0304-3975(76)90061-X"},{"doi-asserted-by":"publisher","key":"e_1_2_1_61_1","DOI":"10.1007\/10722167_36"},{"doi-asserted-by":"publisher","key":"e_1_2_1_62_1","DOI":"10.1016\/0304-3975(76)90062-1"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3091528","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3091528","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:37:30Z","timestamp":1750217850000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3091528"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,31]]},"references-count":58,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2017,7,31]]}},"alternative-id":["10.1145\/3091528"],"URL":"https:\/\/doi.org\/10.1145\/3091528","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2017,7,31]]},"assertion":[{"value":"2016-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-08-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}