2
$\begingroup$

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?

Improve this question
$\endgroup$
9
  • $\begingroup$ 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. $\endgroup$
    – D.W. ♦
    May 19, 2017 at 15:53
  • 1
    $\begingroup$ $\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. $\endgroup$
    – xavierm02
    May 19, 2017 at 17:25
  • $\begingroup$ @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. $\endgroup$
    – rus9384
    May 19, 2017 at 17:45
  • $\begingroup$ Not (there is a computation that accepts) isn't equivalent to there is a computation that rejects. $\endgroup$
    – xavierm02
    May 19, 2017 at 17:56
  • $\begingroup$ @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}$. $\endgroup$
    – rus9384
    May 19, 2017 at 17:56

1 Answer 1

Reset to default
4
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.