# $NP \ vs \ co-NP$: tautology to SAT and vice versa?

Let define formula $\Phi%$ given in CNF and it's complement $\overline \Phi$.

$\Phi$ is satisfiable iff $\overline \Phi$ is not tautology and vice versa.

$\Phi$ can be converted to $\overline \Phi$ in polynomial time using following method:

1. Change all literals with non-literals and vice versa: $\forall i:x_i \Rightarrow \overline {x_i}; \ \overline {x_i} \Rightarrow x_i$.

2. Change all disjunctions with conjunctions and vice versa.

This property is a corollary of CNF/DNF definitions.

This will give us a DNF $\ \overline \Phi\$ of the same length as $\ \Phi$.

Assuming DIMACS format SAT solver can solve tautology this way:

1. Multiply all variables by $-1$.
2. Solve SAT.
3. Return $\overline {answer}$, where $answer$ is global (final) answer for SAT.

Example 1:

$\Phi = (x \lor y \lor \overline z) \land (\overline x \lor t) \land (\overline y \lor \overline t) = 1100.1010.0101.0000$ - is satisfiable.

$\overline \Phi = (\overline x \land \overline y \land z) \lor (x \land \overline t) \lor (y \land t) = 0011.0101.1010.1111$ - is not tautology.

Example 2:

$\Phi = (x \lor y) \land (\overline x \lor y) \land (\overline x \lor \overline y) \land (x \lor \overline y)= 0000$ - is not satisfiable.

$\overline \Phi = (\overline x \land \overline y) \lor (x \land \overline y) \lor (x \land y) \lor (\overline x \land y) = 1111$ - is tautology.

Does this proves that $NP = co-NP$? Or, maybe, somewhere I'm wrong with complexity classes?

• No. Why would it prove that? If you edit the question to give more of your thought process, we might be able to clarify where you went wrong. As it stands there is an enormous gap in your reasoning, so it's hard to know how to help. Try writing a proof where you justify every step, and maybe you'll spot where you went wrong. If not, edit the question to show that proof. But note that checking "is my proof correct?" questions typically aren't very interesting here.
– D.W.
May 19, 2017 at 15:53
• $\varphi$ SAT $\iff$ $\lnot$($\lnot \varphi$ TOT). The second $\lnot$ is easy to remove by using De Morgan's laws, as you described. But the first $\lnot$ can't be easily removed because you can't just use a non-deterministic Turing machine (resp. one of the class used to define co-NP) and then reverse its result. Because a non-deterministic machine accepts iff some branch accepts. And once it has accepted, you can't do anything else. In other words, you can't use the result of a non-deterministic decision procedure: you can only transform the input and then return whatever it returns. May 19, 2017 at 17:25
• @xavierm02, NTM can't convert formulae? If tautology is given as input it can reduce it to SAT this way, if I'm correct. The only difference is that answer will be inverted. May 19, 2017 at 17:45
• Not (there is a computation that accepts) isn't equivalent to there is a computation that rejects. May 19, 2017 at 17:56
• @xavierm02, this algorithm allows to solve tautology with SAT solvers this way (assuming DIMACS format): 1. Multiply all variables by -1. 2. Solve SAT. 3. Return $\overline{answer}$. May 19, 2017 at 17:56