Linear-time algorithms for testing the satisfiability of propositional horn formulae
- 1 October 1984
- journal article
- Published by Elsevier BV in The Journal of Logic Programming
- Vol. 1 (3), 267-284
- https://doi.org/10.1016/0743-1066(84)90014-1
Abstract
New algorithms for deciding whether a (propositional) Horn formula is satisfiable are presented. If the Horn formula A contains K distinct propositional letters and if it is assumed that they are exactly P1,…, PK, the two algorithms presented in this paper run in time O(N), where N is the total number of occurrences of literals in A. By representing a Horn proposition as a graph, the satisfiability problem can be formulated as a data flow problem, a certain type of pebbling. The difference between the two algorithms presented here is the strategy used for pebbling the graph. The first algorithm is based on the principle used for finding the set of nonterminals of a context-free grammar from which the empty string can be derived. The second algorithm is a graph traversal and uses a “call-by-need” strategy. This algorithm uses an attribute grammar to translate a propositional Horn formula to its corresponding graph in linear time. Our formulation of the satisfiability problem as a data flow problem appears to be new and suggests the possibility of improving efficiency using parallel processors.Keywords
This publication has 4 references indexed in Scilit:
- Unit Refutations and Horn SetsJournal of the ACM, 1974
- Symbolic logic and mechanical theorem proving: Chin-Liang Chang and Richard Char-Tung Lee. Academic Press, New York, 1973Artificial Intelligence, 1974
- Reducibility among Combinatorial ProblemsPublished by Springer Science and Business Media LLC ,1972
- The complexity of theorem-proving proceduresPublished by Association for Computing Machinery (ACM) ,1971