Polynomially solvable satisfiability problems

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15) Analysis of algorithms and problem complexity (68Q25)

Review text

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.

Recommendations

Cites work

Cited in

(33)

This page was built for publication: Polynomially solvable satisfiability problems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1114394)