A perspective on certain polynomial time solvable classes of satis

The scope of certain well-studied polynomial-time solvable classes of Satis ability is investigated relative to a polynomial-time solvable class consisting of what we call matched formulas. The class of matched for-mulas has not been studied in the literature, probably because it seems not to contain many challenging formulas. Yet, we nd 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 innity. For m=n> 2=k(k 1), the probability that 1 a random formula is SLUR, q-Horn, extended Horn, CC-balanced, or renamable Horn tends to 0. Form=n <:64, random formulas are matched formulas with probability tending to 1. For m=n k