ECCC-Report TR00-018https://eccc.weizmann.ac.il/report/2000/018Comments and Revisions published for TR00-018en-usTue, 07 Mar 2000 09:52:22 +0200
Paper TR00-018
| An application of matroid theory to the SAT problem |
Oliver Kullmann
https://eccc.weizmann.ac.il/report/2000/018A 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.
Tue, 07 Mar 2000 09:52:22 +0200https://eccc.weizmann.ac.il/report/2000/018