Polynomially solvable satisfiability problems (Q1114394)

We address the well known satisfiability problem (SAT), i.e., the problem of checking whether a given propositional formula is satisfiable. Although the general satisfiability problem is NP-complete, some particular cases of SAT are known to be easy. The most important of those cases is HORN-SAT, i.e., the satisfiability problem in the case of Horn clauses: actually, an instance of HORN-SAT can be solved in linear time. \textit{S. Yamasaki} and \textit{S. Doshita} [Inf. Control 59, 1-12 (1983; Zbl 0564.03010)] have introduced a new subclass of SAT, \(S_ 0\), which is polynomially solvable and which strictly includes HORN-SAT. Here we introduce a family of subclasses of SAT, \(\Gamma_ 0\), \(\Gamma_ 1\),..., \(\Gamma_ k\),..., such that \(HORN\)-SAT\(=\Gamma_ 0\), \(S_ 0=\Gamma_ 1\), \(\Gamma_ k\supseteq \Gamma_{k-1}\), \(k=1\), 2,..., and \(\Gamma_ k\) approaches to SAT as k increases. For each k, \(\Gamma_ k\) is solvable in \(O(n^* n^ k)\) time, where n is the number of propositional letters, m is the number of clauses, and \(n^*=O(n m)\) is the size of the input. An algorithm to check whether a given instance of SAT belongs to \(\Gamma_ k\), for any k, which runs in \(O(n^* n^ k)\) time, is also described.