# Determining when equal 2CNF has pure literal

Let us assume that we have a 2CNF $\varphi(X,y)$. Then we want to see if there is equal formula where $y$ (or $\overline y$) is pure literal. Can this be done in polynomial time? Are there some criteria for understanding this? Can we say if any minimal CNF has $y$ as pure literal, then all of them do?

Simple example:

$\varphi(x_1,x_2,y)=(x_1\lor y)\land(x_1\lor\overline y)\land(x_2\lor y)$.

Equal minimal 2CNF: $x_1\land(x_2\lor y)$.

Pure literal - literal that has only negative/positive appearances in formula.

Equal formula. We say formulas $\varphi$ and $\psi$ are equal if $\varphi\oplus\psi\equiv0$.

Minimal formula - shortest equal formula.

P.S. Last question is the most significant because it also answers if minimal 2CNF has all pure literals.

• By equal formula do you mean produces the same truth table? – Kyle Jones Aug 31 '17 at 22:22
• @KyleJones, yes, equality symbol between 2 formulas must be a tautology. – rus9384 Aug 31 '17 at 22:29
• What do you mean by "where $y$ is pure literal"? What's a pure literal? What do you mean by "equal formula"? What do you mean by "minimal", exactly? Can you define all terms that you are using in the question? Please edit the question to incorporate the information into the question -- don't just leave clarifications in the comments. Thank you! – D.W. Sep 4 '17 at 6:38