[Back]

I. Kanj, R. de Haan, St. Szeider:
"Small Unsatisfiable Subsets in Constraint Satisfaction";
Talk: The IEEE International Conference on Tools with Artificial Intelligence, Special Track on SAT and CSP Technologies (ICTAI), Limassol, Cyprus; 2014-11-10 - 2014-11-12; in: "IEEE-ICTAI 2014", (2014).

The problem of finding small unsatisfiable subsets of a set of constraints is important for various applications in computer science and artificial intelligence. We study the problem of identifying whether a given instance to the constraint satisfaction problem (CSP) has an unsatisfiable subset of size at most k from a parameterized complexity point of view. We show that the problem of finding small unsatisfiable subsets of a CSP instance is harder than the corresponding problem for CNF formulas. Moreover, we show that the problem is not fixed-parameter tractable when restricting the problem to any maximal tractable Boolean constraint language (for which the problem is nontrivial). We show that the problem is hard even when the maximum number of occurrences of any variable is bounded by a constant, a restriction which leads to fixed-parameter tractability for the case of CNF formulas. Finally, we relate the problem of finding small unsatisfiable subsets to the problem of identifying variable assignments that are enforced already by a small number of constraints (backbones), or that are ruled out already by a small number of constraints (anti-backbones).

Project Head Stefan Szeider:
Parameterized Compilation

Project Head Stefan Szeider:
The Parameterized Complexity of Reasoning Problems