 Author
 Date
 82017
 Title
 On the Parameterized Complexity of Finding Small Unsatisfiable Subsets of CNF Formulas and CSP Instances
 Journal
 ACM Transactions on Computational Logic
 Volume  Issue number
 18  3
 Article number
 21
 Number of pages
 46
 Document type
 Article
 Faculty
 Interfacultary Research Institutes
 Institute
 Institute for Logic, Language and Computation (ILLC)
 Abstract

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).
In general, the problem is fixedparameter intractable. 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.
With these fixedparameter 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.
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 fixedparameter intractable for all Schaefer languages for which the problem is nontrivial. 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.
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 fixedparameter tractability, whereas for the case of CSP instances, one needs to restrict the degree, the arity, and the domain size simultaneously to establish fixedparameter tractability.
Finally, we relate the problem of finding small unsatisfiable subsets of a set of constraints to the problem of identifying whether a given variablevalue 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.
 URL
 go to publisher's site
 Language
 English
 Permalink
 http://hdl.handle.net/11245.1/7c229384d41c419592d61b5e24f18dd6
Disclaimer/Complaints regulations
If you believe that digital publication of certain material infringes any of your rights or (privacy) interests, please let the Library know, stating your reasons. In case of a legitimate complaint, the Library will make the material inaccessible and/or remove it from the website. Please Ask the Library, or send a letter to: Library of the University of Amsterdam, Secretariat, Singel 425, 1012 WP Amsterdam, The Netherlands. You will be contacted as soon as possible.