A perspective on certain polynomial-time solvable classes of satisfiability Original Research Article

The scope of certain well-studied polynomial-time solvable classes of Satisfiability is investigated relative to a polynomial-time solvable class consisting of what we call matched formulas. The class of matched formulas has not been studied in the literature, probably because it seems not to contain many challenging formulas. Yet, we find that, in some sense, the matched formulas are more numerous than Horn, extended Horn, renamable Horn, q-Horn, CC-balanced, or single lookahead unit resolution (SLUR) formulas. The behavior of random k-CNF formulas generated by the constant clause-width model is investigated as n and m, the numbers of variables and clauses, go to infinity. For m/n>2/k(k−1), the probability that a random formula is SLUR, q-Horn, extended Horn, CC-balanced, or renamable Horn tends to 0. For m/n<0.64, random formulas are matched formulas with probability tending to 1. For m/nk−1⩾2k/k!, random formulas are solved by a certain polynomial-time resolution procedure with probability tending to 1. The propositional connection graph is introduced to represent clause structure for formulas with general-width clauses. Cyclic substructures are exhibited that occur with high probability and prevent formulas from being in the previously studied polynomial-time solvable classes, but do not prevent them from being in the matched class. We believe that part of the significance of this work lies in guiding the future development of polynomial-time solvable classes of Satisfiability.