On finding solutions for extended Horn formulas

DOI10.1016/0020-0190(95)00019-9MaRDI QIDQ673602zbMATH OpenOpenAlexFDO

Authors John S. Schlipf, Fred S. Annexstein, John V. Franco, R. P. Swaminathan

Publication date 28 February 1997

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

Full work available at URL https://doi.org/10.1016/0020-0190(95)00019-9

zbMATH Keywords

AlgorithmsSatisfiabilityBalanced matricesExtended Horn formulasUnit resolution

Mathematics Subject Classification ID

Parallel algorithms in computer science (68W10)

Recommendations

• Recognition of q-Horn formulae in linear time
• Recognition of simple enlarged Horn formulas and simple extended Horn formulas
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing
• On the complexity of the maximum satisfiability problem for Horn formulas

Cites work

• scientific article; zbMATH DE number 1256705 (Why is no real title available?)
• Extended Horn sets in propositional logic
• The arborescence-realization problem

Cited in

(22)

• A CNF Class Generalizing Exact Linear Formulas
• Recognition of simple enlarged Horn formulas and simple extended Horn formulas
• Typical case complexity of satisfiability algorithms and the threshold phenomenon
• Satisfiability of acyclic and almost acyclic CNF formulas
• A perspective on certain polynomial-time solvable classes of satisfiability
• The Horn renamability, q-Horn and SLUR threshold for random \(k\)-CNF formulas
• On exact selection of minimally unsatisfiable subformulae
• Bounds on the size of PC and URC formulas
• A short note on some tractable cases of the satisfiability problem.
• Satisfiability of acyclic and almost acyclic CNF formulas. II
• Recognition of q-Horn formulae in linear time
• Generalising and unifying SLUR and unit-refutation completeness
• Properties of SLUR Formulae
• Generalising unit-refutation completeness and SLUR via nested input resolution
• Fuzzy logic programs as hypergraphs. Termination results
• The phase transition in random horn satisfiability and its algorithmic implications
• Mixed logical-linear programming
• Extended Horn sets in propositional logic
• A logic-based approach to polymer sequence analysis
• Propagation complete encodings of smooth DNNF theories
• Solving peptide sequencing as satisfiability
• A sharp threshold for the renameable-Horn and the \(q\)-Horn properties

This page was built for publication: On finding solutions for extended Horn formulas

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