An application of matroid theory to the SAT problem

We consider the deficiency δ(F):=c(F)-n(F) and the maximal deficiency δ*(F):=max_F´⊆F^δ(F) of a clause-set F (a conjunctive normal form), where c(F) is the number of clauses in F and n(F) is the number of variables. Combining ideas from matching and matroid theory with techniques from the area of resolution refutations, we prove that for clause-sets F with δ*(F)⩽k, where k is considered as a constant, the SAT problem, the minimally unsatisfiability problem and the MAXSAT problem are decidable in polynomial time (previously, only poly-time decidability of the minimally unsatisfiability problem was known, and that only for k=1)