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

DOI10.1016/0020-0190(87)90200-6zbMath0635.68108OpenAlexW1996333228MaRDI QIDQ1097717

B. George

Publication date: 1987

Published in: Information Processing Letters (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0020-0190(87)90200-6

zbMATH Keywords

complexitysatisfiability problemHorn sentencespropositional sentences

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Mechanization of proofs and logical operations (03B35)

Related Items

On renamable Horn and generalized Horn functions ⋮ Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing ⋮ Polynomially solvable satisfiability problems ⋮ On generalized Horn formulas and \(k\)-resolution ⋮ A hierarchy of tractable satisfiability problems ⋮ Algorithms for the maximum satisfiability problem

Cites Work

• The satisfiabilty problem for a class consisting of horn sentences and some non-horn sentences in proportional logic
• Unification as a complexity measure for logic programming