[Back]

R. de Haan, I. Kanj, S. Szeider:
"On the Parameterized Complexity of Finding Small Unsatisfiable Subsets of CNF Formulas and CSP Instances";
ACM Transactions on Computational Logic, 18 (2017), 1 - 46.

In many practical settings it is useful to nd a small unsatis able
subset of a given unsatis able set of con- straints. We study this
problem from a parameterized complexity perspective, taking the size
of the unsat- is able 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
xed-parameter intractable. For an instance of the propositional satis
ability 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 xed-parameter intractability
results for the general case in mind, we consider various re- stricted
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] identi ed as the maximal
constraint languages with a tractable satis ability problem. We show
that for the CSP setting, the problem of nding small unsatis able
subsets remains xed- 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 identi cation of a small unsatis
able 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
xed-parameter tractability, whereas for the case of CSP instances, one
needs to restrict the degree, the arity, and the domain size
simultaneously to establish xed-parameter tractability. Finally, we
relate the problem of nding small unsatis able 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.

http://dx.doi.org/10.1145/3091528

https://dl.acm.org/citation.cfm?doid=3130378.3091528