AN O(N-2) ALGORITHM FOR THE SATISFIABILITY PROBLEM OF A SUBSET OF PROPOSITIONAL SENTENCES IN CNF THAT INCLUDES ALL HORN SENTENCES

The authors present a simple straightforward O(n**2) algorithm for the satisfiability problem for a class S//0 of propositional sentences that properly contains all Horn sentences. The algorithm basically invokes an algorithm that recognizes satisfiable Horn sentences in O(n) time for inputs of length n. Also given is a linear-time reduction from satisfiable sentences in S//0 to a certain subset of itself. This can be seen as a pointer to the easy structure of S//0.