A linear time algorithm for unique Horn satisfiability

DOI10.1016/0020-0190(93)90178-CMaRDI QIDQ1313762zbMATH OpenOpenAlexFDO

Authors D. 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

directed hypergraphsdisjoint set unionHorn formulassatisfiability

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)

Review text

The Unique-HornSAT problem asks whether there exists a unique solution to a given Horn satisfiability problem. Here, we propose a linear time Unique-HornSAT algorithm. We use directed hypergraphs to represent Horn formulas; our method combines a hypergraph transformation technique with the search of strongly connected components in a sub-graph. In the proposed implementation, we solve a particular disjoint set union problem, for which linear amortized time algorithms are known. A similar result was obtained independently by Berman, Franco and Schlipf, although they fail to obtain a linear complexity.

Recommendations

• Unique satisfiability of Horn sets can be solved in nearly linear time
• Unique Horn renaming and Unique 2-Satisfiability
• The unique Horn-satisfiability problem and quadratic Boolean equations.
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• On the complexity of unique circuit SAT

Cites work

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

Cited in

(8)

• A linear algorithm for renaming a set of clauses as a Horn set
• The unique Horn-satisfiability problem and quadratic Boolean equations.
• Partially dynamic maintenance of minimum weight hyperpaths
• Unique satisfiability of Horn sets can be solved in nearly linear time
• scientific article; zbMATH DE number 991069 (Why is no real title available?)
• About some UP-based polynomial fragments of SAT
• Unique Horn renaming and Unique 2-Satisfiability
• Complexity of pairwise shortest path routing in the grid

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

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