Polynomially solvable satisfiability problems

DOI10.1016/0020-0190(88)90113-5zbMath0662.68037OpenAlexW2054160878MaRDI QIDQ1114394

Maria Grazia Scutellà, Giorgio Gallo

Publication date: 1988

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

Full work available at URL: https://doi.org/10.1016/0020-0190(88)90113-5

zbMATH Keywords

Horn clausessatisfiabilitypolynomially solvable

Mathematics Subject Classification ID

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

Related Items

A new algorithm for the propositional satisfiability problem, Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing, On resolution with short clauses, On computing minimal models, Hierarchies of polynomially solvable satisfiability problems, On the impact of stratification on the complexity of nonmonotonic reasoning, Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets, Special issues on The satisfiability problem (pp. 1--244) including papers from the 1st workshop on satisfiability, Certosa di Pontignano, Italy, April 29--May 3, 1996 and Boolean functions (pp. 245--479), Maximum renamable Horn sub-CNFs, Recognition of tractable satisfiability problems through balanced polynomial representations, On generalized Horn formulas and \(k\)-resolution, A hierarchy of tractable satisfiability problems, 1999 European Summer Meeting of the Association for Symbolic Logic, The complexity of the falsifiability problem for pure implicational formulas, Recognizing renamable generalized propositional Horn formulas is NP- complete, Tractable reasoning via approximation, On functional dependencies in \(q\)-Horn theories

Cites Work

• An \(O(n^ 2)\) algorithm for the satisfiability problem of a subset of propositional sentences in CNF that includes all Horn sentences
• The satisfiabilty problem for a class consisting of horn sentences and some non-horn sentences in proportional logic
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• The complexity of theorem-proving procedures