Constraint satisfaction problems in clausal form: Autarkies, minimal unsatisfiability, and applications to hypergraph inequalities

摘要

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 considerirredundant generalised CNFs, and characterise some extremal minimallyunsatisfiable CNFs.