An \(O(n^ 2)\) algorithm for the satisfiability problem of a subset of propositional sentences in CNF that includes all Horn sentences (Q1097717)

Based on the results of Ìtai and Makowsky that recognize satisfiable Horn sentences in O(n) time, the authors present in this paper an algorithm that improves the performance of the algorithm of Yamasaki and Doshita of solving the satisfiability problem for a class \(S_ 0\) of propositional sentences that properly contains all Horn sentences. The algorithm, its correctness and complexity, and the structure of \(S_ 0\) are presented.