We study complement-invariant clause-sets F, where for every clause C ∈ F we have (C-bar) = {(x-bar):x ∈ C} ∈ F, i.e., F is closed under elementwise complementation of clauses. The reduced deficiency of a clause-set F is defined as δ_r(F): =1/2(δ(F)-n(F)), where δ(F) = c(F)-n(F) is the difference of the number of clauses and the number of variables, while the maximal reduced deficiency is δ_r~*(F): = max_(F' is contained in F) δ_r(F') ≥ 0. We show polynomial time SAT decision for complement-invariant clause-sets F with δ_r~*(F) = 0, exploiting the (non-trivial) decision algorithm for sign-non-singular (SNS) matrices given by [Robertson, Seymour, Thomas 1999; McCuaig 2004]. As an application, hypergraph 2-colourability decision is considered. Minimally unsatisfiable complement-invariant clause-sets F fulfil δ_r(F) = δ_r~*(F), and thus we immediately obtain polynomial time decidability of minimally unsatisfiable complement-invariant clause-sets F with δr(F) = 0, but we also give more direct algorithms and characterisations (especially for sub-classes). The theory of autarkies is the basis for all these considerations.
展开▼
