given a formula S (that is built of binary variables and "or", "not", "and" gates). IS there a polynomial algorithim that builds S' that satisfies:
S' satisfied if and only if S doesn't satisfied.
which means: S' is in SAT if and only if S not in SAT

  • 2
    $\begingroup$ Did you mean satisfied or satisfiable? $\endgroup$ – Stig Hemmer May 13 '20 at 7:43

The existence of such an algorithm would imply co-NP is included in NP which is unlikely

Checking that a formula is satisfiable: NP, generate proof by providing a solution

Checking that a formula is unsafisfiable: co-NP, generating proof can be harder, in classical proof systems the shortest proof of unsatisfiability of an arbitrary formula can be exponentially long

The algorithm you are looking for would mean all problems in co-NP have a short refutation, by providing a solution to the "opposite" formula. Therefore we are unaware of the existence of such an algorithm.

  • $\begingroup$ This answer is incomplete, it explains why solving is not possible in polynomial time, but it does not provide any reason why solving is a requirement for reversing the SAT answer. $\endgroup$ – Ivo May 13 '20 at 9:33
  • $\begingroup$ @Ivo I don't understand what you mean by "solving is a requirement for reversing the SAT answer". This answer doesn't talk about solving, and membership in NP and co-NP isn't really related to being able to solve anything. $\endgroup$ – JiK May 13 '20 at 12:12
  • $\begingroup$ Expanding the answer a bit: A function $f$ with $f(\varphi) \in \overline{\mathrm{SAT}}$ iff $\varphi \in \mathrm{SAT}$ is a many-one reduction showing $\mathrm{SAT} \leq_\mathsf{P} \overline{\mathrm{SAT}}$. As $\overline{\mathrm{SAT}}$ is known to be $\mathsf{coNP}$-complete, the existence of such a reduction implies $\mathsf{coNP} \subseteq \mathsf{NP}$, which is an open question and seems rather unlikely given that if it were to be true, then $\mathsf{coNP} = \mathsf{NP}$ and thus a collapse of the polynomial hierarchy to the first level looks probable. $\endgroup$ – Watercrystal May 13 '20 at 14:07
  • $\begingroup$ @JiK I meant solving as in deciding if it / is not in SAT. TO give an example with another problem called EVEN: given an integer, decide whether that integer is even. This question would ask "given an instance x, return an instance y not in EVEN iff the instance is in EVEN". An algorithm that can do that is y = x + 1, which works without knowing whether x is in EVEN or not. ... $\endgroup$ – Ivo May 14 '20 at 23:39
  • 1
    $\begingroup$ @Ivo The answer only talks about the hypothesized asymmetry of NP and co-NP, which would imply the asymmetry of SAT and UNSAT, and this answer does explain why that means a polynomial algoritm for the question is not likely to exist. There is nothing about algorithms that deciding whether a formula is satisfiable in this answer, NP and co-NP are not about algorithms that solve problems. $\endgroup$ – JiK May 16 '20 at 19:17

yet we can't determined such a thing due to the fact that SAT is NP-hard and the "UNSAT" is co-Np-hard.


There can't be such a polynomial-time algorithm that reliably inverts satisfiability unless P = NP.

If S is satisfiable, you can only make it unsatisfiable by adding constraints. If S is unsatisfiable, you can only make it satisfiable by removing constraints. By the law of the excluded middle S must be satisfiable or unsatisfiable, which means your algorithm must either add or remove constraints, which means that you must be able to determine whether S is satisfiable or unsatisfiable in polynomial time before you can decide what changes to make. That is, you must have a polynomial-time algorithm that decides Boolean satisfiability as a necessary first step.

  • $\begingroup$ There are other ways to transform formulas into other formulas than just removing or adding constraints. $\endgroup$ – JiK May 13 '20 at 12:14
  • $\begingroup$ For example, if the problem is restricted to 2-CNF formulas, there is an obvious answer that gives a formula with just a 0 or 2 clauses, no matter the input formula size. $\endgroup$ – JiK May 13 '20 at 12:52
  • $\begingroup$ There are no other ways that affect satisfiability or unsatisfiability, which is the point of this exercise. And your 2-CNF example just further illustrates my point in that there is a polynomial-time algorithm that decides satisfiability for 2-CNF formulas so you can decide what to do, and what you end up doing is removing or adding constraints. $\endgroup$ – Kyle Jones May 13 '20 at 16:07
  • $\begingroup$ I'm not following. If the input is $(x \vee y) \wedge (y \vee z) \wedge (z \vee x)$, which is satisfiable, a correct algorithm could output $(x \vee x) \wedge (\neg x \vee \neg x)$, which is unsatisfiable. Is this what you call "removing or adding constraints"? $\endgroup$ – JiK May 13 '20 at 16:22
  • $\begingroup$ Yes. You have added a constraint that makes the formula unsatisfiable. $\endgroup$ – Kyle Jones May 13 '20 at 16:33

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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