<p>I don't know any publication where this is stated, but it is an <span class="math-container">$NLOGSPACE$</span>-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 <span class="math-container">$s$</span> and <span class="math-container">$t$</span> in a given (directed) graph <span class="math-container">$G= (V,E)$</span>. Indeed, the following formula
<span class="math-container">$$p_s \land \bigwedge_{(v,u) \in E} \neg p_v \lor p_u$$</span>
entails <span class="math-container">$p_t$</span> iff there is a path between <span class="math-container">$s$</span> and <span class="math-container">$t$</span>.</p>
<p>For the upper bound, we can argue as follows. Consider an arbitrary formula <span class="math-container">$\varphi$</span> in <strong>HORN-2CNF</strong> form
<span class="math-container">$$\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$$</span>
To check whether this formula entails a given propositional symbol <span class="math-container">$q$</span>, one first checks whether it is satisfiable (this problem is in <span class="math-container">$NLOGSPACE$</span>) and returns <strong>true</strong> in case it is not satisfiable. If it satisfiable, one can go through all &quot;positive&quot; atomic formulas <span class="math-container">$p_i$</span> and for each of them run the following procedure, which has as its variables a counter <span class="math-container">$c$</span> and the current propositional symbol <span class="math-container">$p_k$</span>:</p>
<ol>
<li>If <span class="math-container">$p_k = q$</span>, then return <strong>true</strong>.</li>
<li>If <span class="math-container">$c = |\varphi| +1$</span>, then return <strong>false</strong></li>
<li>If there is no <span class="math-container">$\ell$</span> so that <span class="math-container">$\neg p_k \lor p_\ell$</span> occurs in <span class="math-container">$\varphi$</span>, then return <strong>false</strong></li>
<li>Guess an <span class="math-container">$\ell$</span> so that <span class="math-container">$\neg p_k \lor p_\ell$</span> occurs in <span class="math-container">$\varphi$</span> and set <span class="math-container">$p_k := p_\ell$</span>.</li>
<li>Go to step 1.</li>
</ol>
<p>Since <span class="math-container">$|\varphi|$</span> can be represented using a logarithmic amount of bits in the size of <span class="math-container">$|\varphi|$</span>, it is clear that the above procedure uses only logarithmic work space. Furthermore it is clear that <span class="math-container">$\varphi$</span> entails <span class="math-container">$q$</span> iff for some <span class="math-container">$i\in I$</span> the above procedure returns <strong>true</strong>.</p>
<p><strong>EDIT:</strong> After posting this answer, I realized that there is a much simpler argument for the upper bound. If <span class="math-container">$\varphi$</span> is in <strong>2CNF</strong>, then <span class="math-container">$\varphi \models p$</span> iff <span class="math-container">$\neg \varphi \lor p$</span> is valid iff <span class="math-container">$\varphi \land \neg p$</span> is unsatisfiable. Since <span class="math-container">$\varphi$</span> is in <strong>2CNF</strong>, the latter problem is in <span class="math-container">$coNLOGSPACE=NLOGSPACE$</span>.</p>

CC BY-SA 4.0
2021-11-15T10:01:08.237Z
2021-11-15T13:52:01.627Z
2021-11-15T13:52:01.627Z
Reijo Jaakkola
<p>I know the entailment of a propositional variable in a <strong>HORN-3CNF</strong> formula is <span class="math-container">$P$</span>-complete.</p>
<p>I can't find any publication in which it has been shown the complexity of the same problem for <strong>HORN-2CNF</strong> formulas. Can someone help me?</p>

CC BY-SA 4.0
2021-11-15T11:53:51.143Z
It should be NL-complete: Just translate the formula into a directed graph, and solve some reachability problems.
Gamow
<complexity-classes><complexity-theory><p-hardness>
What is the complexity of HORN-2CNF entailment?
Abel Freid
# What is the complexity of HORN-2CNF entailment?

(Asked by: username_0 on 2021-11-14)

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?

**Tags:** complexity-classes, complexity-theory, p-hardness
> **Comments:**
> **username_1**: It should be NL-complete: Just translate the formula into a directed graph, and solve some reachability problems.  

---

## 1 answers

### Answer by username_2 on 2021-11-15. Score: 8 | Accepted answer

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


---

