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
$\begingroup$
$\endgroup$
1
-
2$\begingroup$ Did you mean satisfied or satisfiable? $\endgroup$– Stig HemmerMay 13, 2020 at 7:43
Add a comment
|
3 Answers
$\begingroup$
$\endgroup$
10
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$– IvoMay 13, 2020 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$– JiKMay 13, 2020 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$ May 13, 2020 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$– IvoMay 14, 2020 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$– JiKMay 16, 2020 at 19:17
$\begingroup$
$\endgroup$
yet we can't determined such a thing due to the fact that SAT is NP-hard and the "UNSAT" is co-Np-hard.
$\begingroup$
$\endgroup$
9
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.
answered May 13, 2020 at 0:31
-
$\begingroup$ There are other ways to transform formulas into other formulas than just removing or adding constraints. $\endgroup$– JiKMay 13, 2020 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$– JiKMay 13, 2020 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$ May 13, 2020 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$– JiKMay 13, 2020 at 16:22
-
$\begingroup$ Yes. You have added a constraint that makes the formula unsatisfiable. $\endgroup$ May 13, 2020 at 16:33