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?

  • 2
    $\begingroup$ It should be NL-complete: Just translate the formula into a directed graph, and solve some reachability problems. $\endgroup$
    – Gamow
    Nov 15, 2021 at 11:53

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.