# What is the complexity of HORN-2CNF entailment?

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?

• It should be NL-complete: Just translate the formula into a directed graph, and solve some reachability problems. Commented Nov 15, 2021 at 11:53

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$$.