Constraint satisfaction problems in clausal form: Autarkies, minimal unsatisfiability, and applications to hypergraph inequalities
Oliver Kullmann · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2006
Generalised CNFs are considered using such literals, which exclude exactly one possible value from the domain of the variable. First we consider poly-time SAT decision (and fixed-parameter tractability) exploiting matching theory. Then we consider irredundant generalised CNFs, and characterise some extremal minimally unsatisfiable CNFs.