__
TR00-018 | 16th February 2000 00:00
__

#### An application of matroid theory to the SAT problem

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