Sub-exponential complexity of regular linear CNF formulas

TL;DR

This paper expands the class of regular linear CNF formulas known to have sub-exponential complexity for satisfiability, introducing the concept of disjointedness to generalize previous results.

Contribution

It introduces the property of disjointedness and shows that all monotone, regular, d-disjointed LCNF formulas have sub-exponential XSAT complexity, broadening prior findings.

Findings

Regular LCNF formulas with bounded disjointedness are of sub-exponential complexity.

The class of d-disjointed formulas includes the previously studied XLCNF formulas.

Sub-exponential complexity extends to formulas with bounded mean disjointedness.

Abstract

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.