Propositional Horn Clause Satisfiability (PHCS)
Category: Logic
Input
A set $S$ of Horn clauses in the propositional calculus.
Problem
Is $S$ satisfiable?
Status
$\P$-complete (Kasif [1], Plaisted [2]).
Remarks
The reduction to show hardness is from AGAP. The problem remains $\P$-complete when there are at most three literals per clause [2]. Plaisted has shown that two problems involving proofs of restricted depth are also $\P$-complete. They are the Two Literal Horn Clause Unique Matching Problem and the Three Literal Horn Clause Problem [2]. Kasif observes that PHCS remains $\P$-complete when the set of clauses is restricted so that implications have at most two atoms on their right-hand side [3].
References
- S. Kasif (1986). On the parallel complexity of discrete relaxation in constraint satisfaction networks.
- D. A. Plaisted (1984). Complete problems in the first-order predicate calculus.
- S. Kasif (1990). On the parallel complexity of discrete relaxation in constraint satisfaction networks.
- Greenlaw, R., Hoover, H. J., and Ruzzo, W. L. (1995). Limits to Parallel Computation: P-Completeness Theory. Oxford University Press. Problem A.6.3.