Efficient transformation into CNF preserving entailment

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

• Let $\varphi'$ be the Tseitin encoding of $\varphi\land\neg\psi$, and $\psi'=\bot$. Commented Apr 22, 2022 at 12:44
• 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. Commented Apr 23, 2022 at 13:04
• 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. Commented Apr 23, 2022 at 15:21

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