Recognition of \(q\)-Horn formulae in linear time

DOI10.1016/0166-218X(94)90033-7zbMath0821.68109OpenAlexW1974563688WikidataQ59560996 ScholiaQ59560996MaRDI QIDQ1337669

Endre Boros, Xiaorong Sun, Peter L. Hammer

Publication date: 10 September 1995

Published in: Discrete Applied Mathematics (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0166-218x(94)90033-7

zbMATH Keywords

disjunctive normal form\(q\)-Horn Boolean expressions

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27)

Related Items (27)

On perfect \(0,\pm 1\) matrices ⋮ Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing ⋮ On the size of maximum renamable Horn sub-CNF ⋮ An explicit semidefinite characterization of satisfiability for Tseitin instances on toroidal grid graphs ⋮ On propositional definability ⋮ Variable and term removal from Boolean formulae ⋮ A CNF Class Generalizing Exact Linear Formulas ⋮ SAT backdoors: depth beats size ⋮ Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets ⋮ Trichotomy for integer linear systems based on their sign patterns ⋮ Maximum renamable Horn sub-CNFs ⋮ On connected Boolean functions ⋮ A CNF Formula Hierarchy over the Hypercube ⋮ Bounds on the size of PC and URC formulas ⋮ About some UP-based polynomial fragments of SAT ⋮ On semidefinite least squares and minimal unsatisfiability ⋮ Solving the resolution-free SAT problem by submodel propagation in linear time ⋮ Satisfiability of mixed Horn formulas ⋮ Strong Backdoors for Default Logic ⋮ Investigations on autark assignments ⋮ Default reasoning from conditional knowledge bases: Complexity and tractable cases ⋮ A short note on some tractable cases of the satisfiability problem. ⋮ A sharp threshold for the renameable-Horn and the \(q\)-Horn properties ⋮ Typical case complexity of satisfiability algorithms and the threshold phenomenon ⋮ A perspective on certain polynomial-time solvable classes of satisfiability ⋮ On functional dependencies in \(q\)-Horn theories ⋮ Backdoors to q-Horn

Cites Work

• A simplified NP-complete satisfiability problem
• Complete problems for deterministic polynomial time
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• Horn logic, search and satisfiability. A collection of papers in memory of Robert G. Jeroslow
• Polynomial-time inference of all valid implications for Horn and related formulae
• On renamable Horn and generalized Horn functions
• Branch-and-cut solution of inference problems in propositional logic
• Question-asking strategies for Horn clause systems
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Algorithms for testing the satisfiability of propositional formulae
• Recognizing disguised NR(1) instances of the satisfiability problem
• On the Complexity of Timetable and Multicommodity Flow Problems
• Renaming a Set of Clauses as a Horn Set
• A Complexity Index for Satisfiability Problems
• Extended Horn sets in propositional logic
• Depth-First Search and Linear Graph Algorithms
• The complexity of theorem-proving procedures

This page was built for publication: Recognition of \(q\)-Horn formulae in linear time