Recognition of \(q\)-Horn formulae in linear time
From MaRDI portal
Publication:1337669
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
Related Items
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
