The study of regular linear conjunctive normal form (LCNF) formulas is of interest because exact satisfiability (XSAT) is known to be NP-complete for this class of formulas. In a recent paper it was shown that the subclass of regular exact LCNF formulas (XLCNF) is of sub-exponential complexity, i.e. XSAT can be determined in sub-exponential time. Here I show that this class is just a subset of a larger class of LCNF formulas which display this very kind of complexity. To this end I introduce the property of disjointedness of LCNF formulas, measured, for a single clause C, by the number of clauses which have no variable in common with C. If for a given LCNF formula F all clauses have the same disjointedness d we call F d-disjointed and denote the class of such formulas by dLCNF. XLCNF formulas correspond to the special cased=0. One main result of the paper is that the class of all monotone l-regular LCNF formulas which are d-disjointed, with d smaller than some upper bound D, is of sub-exponential complexity. This result can be generalized to show that all monotone, l-regular LCNF formulas F which have a bounded mean disjointedness, are of sub-exponential XSAT-complexity, as well.
تحميل البحث