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:Change all literals with non-literals and vice versa: $\forall i:x_i \Rightarrow \overline {x_i}; \ \overline {x_i} \Rightarrow x_i$.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:Multiply all variables by $-1$.Solve SAT. 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?
$NP \ vs \ co-NP$: tautology to SAT and vice versa?
complexity theory;np complete;satisfiability;np
Your algorithm doesn't prove NP = co-NP because you're using a Cook reduction to go from DNF-TAUTOLOGIES to CNF-SAT.  NP and co-NP aren't separate complexity classes under Cook reductions, they are separate under Karp reductions.  Under Karp reduction, changing the output of Turing machine after you've performed the polynomial-time transformation is specifically disallowed.So while your algorithm is a way to use a SAT solver to validate proofs, it doesn't say anything about whether NP = co-NP.