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.