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 ... more >>>