Abstract:
A basic property of minimally unsatisfiable clause-sets F is that c(F) >= n(F) + 1 holds, where c(F) is the number of clauses, and n(F) the number of variables. Let MUSAT(k) be the class of minimally unsatisfiable clause-sets F with c(F) <= n(F) + k. Poly-time decision algorithms are known for the classes MUSAT(1) and SMUSAT(1) ("strongly" minimally unsatisfiable clause-sets, where addition of any literal to any clause renders them satisfiable). We show that for all k the classes MUSAT(k) and SMUSAT(k) are poly-time decidable. In fact we arrive at the stronger conclusion, that the SAT problem (as well as the MAXSAT problem and some other interesting tasks) for clause-sets F, such that c(F') <= n(F') + k for all subsets F' of F holds, is decidable in polynomial time for any constant k. In doing so, we combine ideas from matching and matroid theory with techniques from the area of resolution refutations.