A linear time algorithm for unique Horn satisfiability

DOI10.1016/0020-0190(93)90178-CzbMath0791.68080OpenAlexW2002233041MaRDI QIDQ1313762

Daniele Pretolani

Publication date: 24 February 1994

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

Full work available at URL: https://doi.org/10.1016/0020-0190(93)90178-c

zbMATH Keywords

satisfiabilitydisjoint set uniondirected hypergraphsHorn formulas

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Graph theory (including graph drawing) in computer science (68R10) Logic in artificial intelligence (68T27)

Related Items (4)

Unique Horn renaming and Unique 2-Satisfiability ⋮ About some UP-based polynomial fragments of SAT ⋮ Complexity of pairwise shortest path routing in the grid ⋮ Partially dynamic maintenance of minimum weight hyperpaths

Cites Work

• A linear-time algorithm for a special case of disjoint set union
• Uniquely solvable quadratic Boolean equations
• The unique Horn-satisfiability problem and quadratic Boolean equations.
• Polynomial-time inference of all valid implications for Horn and related formulae
• Directed hypergraphs and applications
• Unique satisfiability of Horn sets can be solved in nearly linear time
• A new algorithm for the propositional satisfiability problem
• On the unique satisfiability problem
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Depth-First Search and Linear Graph Algorithms

This page was built for publication: A linear time algorithm for unique Horn satisfiability