Monadic Krom Satisfiability (MKS)
Category: Logic
Input
A monadic Krom formula $F$.
Problem
Is $F$ satisfiable?
Definitions
A Krom formula is a $2$-CNF formula. That is, a formula in CNF with at most two disjuncts per clause. Let $\varphi$ and $\psi$ be predicate letters that may be preceded by a negation. A conjunct of $F$ is monadic if it is of the form $(\varphi y_1 y_1 \vee \psi y_1 y_1)$.
Status
$\P$-complete (Denenberg and Lewis [1]).
Remarks
An algorithm showing the problem is in P is given in [1]. The reduction to show hardness is from a Nonacceptance Problem for Pushdown Automata (Denenberg [2][1]), see 2DPDA.
References
- L. Denenberg and H. R. Lewis (1984). The complexity of the satisfiability problem for Krom formulas.
- L. Denenberg (1984). Computational Complexity of Logical Problems.
- Greenlaw, R., Hoover, H. J., and Ruzzo, W. L. (1995). Limits to Parallel Computation: P-Completeness Theory. Oxford University Press. Problem A.6.4.