<p>This is impossible in polynomial time unless P = NP. Such a transformation would give a reduction of the coNP-complete validity problem <span class="math-container">$\{\psi:\top\models\psi\}$</span> to the polynomial-time decidable problem <span class="math-container">$\top'\models\psi'$</span>, where <span class="math-container">$\top'$</span> is a constant-size formula, and <span class="math-container">$\psi'$</span> is a CNF.</p>
<p>The best you can do is to reduce <span class="math-container">$\varphi\models\psi$</span> to <span class="math-container">$\varphi'\models\psi''$</span> where <span class="math-container">$\varphi'$</span> is a 3CNF (using the Tseitin transform) and <span class="math-container">$\psi''$</span> is a 3DNF (using the dual Tseitin transform, making sure that the extension variables introduced in <span class="math-container">$\varphi'$</span> and <span class="math-container">$\psi''$</span> are disjoint). You can’t make <span class="math-container">$\psi''$</span> a CNF by the argument above, and dually, you can’t make <span class="math-container">$\varphi'$</span> a DNF (if <span class="math-container">$\psi''$</span> depends only on <span class="math-container">$\psi$</span>, not on <span class="math-container">$\varphi$</span>).</p>

CC BY-SA 4.0
2022-04-24T10:11:15.357Z
2022-04-24T10:20:16.003Z
2022-04-24T10:20:16.003Z
Emil Jeřábek
<p>Suppose you have two propositional formulas <span class="math-container">$\varphi$</span> and <span class="math-container">$\psi$</span>, <strong>not necessarily in CNF</strong>. I want to convert them to 3CNF efficiently (hence introducing auxiliary variables) in such a way that <span class="math-container">$\varphi \models \psi$</span> if and only if <span class="math-container">$\varphi' \models \psi'$</span>, where the latter are the transformed formulas, written in 3CNF.</p>
<p>The usual Tseitin encoding for Boolean formulas preserves satisfiability, but it does not preserve entailment, so it doesn't work. Is there any other known notion of translation that preserves this?</p>
<p><strong>Edit</strong>. I need <span class="math-container">$\varphi'$</span> to depend exclusively on <span class="math-container">$\varphi$</span>.</p>

CC BY-SA 4.0
2022-04-22T12:44:51.057Z
Let $\varphi'$ be the Tseitin encoding of $\varphi\land\neg\psi$, and $\psi'=\bot$.
Emil Jeřábek
CC BY-SA 4.0
2022-04-23T13:04:56.137Z
For the purposes of my reduction this doesn't really work; I need $\varphi'$ to depend exclusively on $\varphi$. I'm trying to preserve compilability in the Cadoli style.
Noel Arteche
CC BY-SA 4.0
2022-04-23T15:21:44.730Z
You can't do that, then. If you fix $\varphi=\top$, you'd get a reduction of the coNP-complete validity problem to the CNF validity problem, which is in P. The best you can hope for is to make $\varphi'$ a CNF, and $\psi'$ a DNF.
Emil Jeřábek
<lo.logic><polynomial-time><boolean-formulas>
Efficient transformation into CNF preserving entailment
Noel Arteche
# Efficient transformation into CNF preserving entailment

(Asked by: username_0 on 2022-04-22)

Suppose you have two propositional formulas $\varphi$ and $\psi$, **not necessarily in CNF**. I want to convert them to 3CNF efficiently (hence introducing auxiliary variables) in such a way that $\varphi \models \psi$ if and only if $\varphi' \models \psi'$, where the latter are the transformed formulas, written in 3CNF.

The usual Tseitin encoding for Boolean formulas preserves satisfiability, but it does not preserve entailment, so it doesn't work. Is there any other known notion of translation that preserves this?

**Edit**. I need $\varphi'$ to depend exclusively on $\varphi$.

**Tags:** lo.logic, polynomial-time, boolean-formulas

> **Comments:**
> **username_1**: Let $\varphi'$ be the Tseitin encoding of $\varphi\land\neg\psi$, and $\psi'=\bot$.  
> **username_0**: For the purposes of my reduction this doesn't really work; I need $\varphi'$ to depend exclusively on $\varphi$. I'm trying to preserve compilability in the Cadoli style.  
> **username_1**: You can't do that, then. If you fix $\varphi=\top$, you'd get a reduction of the coNP-complete validity problem to the CNF validity problem, which is in P. The best you can hope for is to make $\varphi'$ a CNF, and $\psi'$ a DNF.  

---

## 1 answers

### Answer by username_1 on 2022-04-24. Score: 4 | Accepted answer

This is impossible in polynomial time unless P = NP. Such a transformation would give a reduction of the coNP-complete validity problem $\{\psi:\top\models\psi\}$ to the polynomial-time decidable problem $\top'\models\psi'$, where $\top'$ is a constant-size formula, and $\psi'$ is a CNF.

The best you can do is to reduce $\varphi\models\psi$ to $\varphi'\models\psi''$ where $\varphi'$ is a 3CNF (using the Tseitin transform) and $\psi''$ is a 3DNF (using the dual Tseitin transform, making sure that the extension variables introduced in $\varphi'$ and $\psi''$ are disjoint). You can’t make $\psi''$ a CNF by the argument above, and dually, you can’t make $\varphi'$ a DNF (if $\psi''$ depends only on $\psi$, not on $\varphi$).


---

