What is the complexity of HORN-2CNF entailment?

Question

I know the entailment of a propositional variable in a HORN-3CNF formula is $P$-complete.

I can't find any publication in which it has been shown the complexity of the same problem for HORN-2CNF formulas. Can someone help me?

Answer 1

I don't know any publication where this is stated, but it is an $NLOGSPACE$-complete. For the lower bound one can give a reduction from the reachability problem, which is the problem of determining whether there is a path between two vertices $s$ and $t$ in a given (directed) graph $G= (V,E)$. Indeed, the following formula $$p_s \land \bigwedge_{(v,u) \in E} \neg p_v \lor p_u$$ entails $p_t$ iff there is a path between $s$ and $t$.

For the upper bound, we can argue as follows. Consider an arbitrary formula $\varphi$ in HORN-2CNF form $$\bigwedge_{i\in I} p_i \land \bigwedge_{j\in J} \neg p_j \land \bigwedge_{k,\ell} \neg p_k \lor p_\ell \land \bigwedge_{k,\ell} \neg p_k \lor \neg p_\ell$$ To check whether this formula entails a given propositional symbol $q$, one first checks whether it is satisfiable (this problem is in $NLOGSPACE$) and returns true in case it is not satisfiable. If it satisfiable, one can go through all "positive" atomic formulas $p_i$ and for each of them run the following procedure, which has as its variables a counter $c$ and the current propositional symbol $p_k$:

1. If $p_k = q$, then return true.
2. If $c = |\varphi| +1$, then return false
3. If there is no $\ell$ so that $\neg p_k \lor p_\ell$ occurs in $\varphi$, then return false
4. Guess an $\ell$ so that $\neg p_k \lor p_\ell$ occurs in $\varphi$ and set $p_k := p_\ell$.
5. Go to step 1.

Since $|\varphi|$ can be represented using a logarithmic amount of bits in the size of $|\varphi|$, it is clear that the above procedure uses only logarithmic work space. Furthermore it is clear that $\varphi$ entails $q$ iff for some $i\in I$ the above procedure returns true.

EDIT: After posting this answer, I realized that there is a much simpler argument for the upper bound. If $\varphi$ is in 2CNF, then $\varphi \models p$ iff $\neg \varphi \lor p$ is valid iff $\varphi \land \neg p$ is unsatisfiable. Since $\varphi$ is in 2CNF, the latter problem is in $coNLOGSPACE=NLOGSPACE$.