# Proving unsatisfiability of a propositional formula

I have a propositional formula $F$ and an assignment of truth variables $A$. The assignment $A$ assigns a truth value to each variable in $F$ and then it can be evaluated.

I have a function which for a given formula $F$ and a given assignment $A$ checks if both $A$ and $\overline A$ evaluate to the same truth value. It looks like this:

boolean checkSymmetry (Formula F, Assignment A) {

if (evaluate(A) == evaluate((not A)))
return true;
else
return false;
}


Now I want to use method checkUnsatisfiability to check if a given formula $F'$ is "symmetric" as described above. Something like:

boolean checkSymmetryWithCheckUnsatisfiability (Formula F) {

/* The checkSymmetry problem is reduced to the checkUnsatisfiability problem to which I have a solution. */
boolean result = cleverUseOfCheckUnsatisfiability(F);

// result is true if Formula F is "symmetric", otherwise false
return result;
}


All right, so there is no way to reduce checkUnsatisfiability to checkSymmetry since that would mean reducing an NP-Complete to an easy one which is impossible unless $P = NP$, thanks to @xavierm02 and especially @chi for clarifying this.

Since checkSymmetry is easy and checkUnsatisfiability is hard It should be possible to reduce checkSymmetry to checkUnsatisfiability in polynomial time, is that correct? If so, how would I do that?

• cherckSymmetry is in the complexity class P (attained by your implementation) and checkUnsatisfiability is in co-NP. So there will be some complicated / brute-force-ish things hapnenning in cleverUseOfCheckSymmetry other than just calling checkSymmetry (or your algorithm is a simple proof that co-NP = P and therefore that P = NP, but that's very very unlikely). – xavierm02 Jul 21 '17 at 15:49
• @xavierm02 Good point, I updated the question with a follow up question. – Anna Vopureta Jul 21 '17 at 21:48

If we take the problem precisely as stated, the answer is negative, assuming $P\neq NP$. Indeed, checkSymmetry is trivially implementable in polynomial time, since it takes as input both the formula $F$ and the assignment $A$, so it can check those. Hence, if a reduction existed, that would imply that unsatisfiability is polynomially decidable, hence $P=NP$.

(Update: my guess below was not what the OP wanted, but I am leaving it here anyway.)

However, I guess your checkSymmetry is meant to take only $F$ as input, and check something equivalent to the validity of $F \iff \bar F$, where $\bar F$ is $F$ with every atomic formula negated.

Then, we can reduce checking validity of any propositional formula to checking symmetry.

Given any $F$, take $G := P \land \lnot F$, where $P$ is an atomic formula not occuring in $F$. We have $$\models F \iff \models (G \iff \bar G)$$

($\Rightarrow$) Assume $\models F$: we deduce immediately $\models \bar F$.

We need to prove that $$\models (P \land \lnot F) \iff (\lnot P \land \lnot \bar F)$$ but we know $F$ and $\bar F$ are true for all assignments, so the above simplifies to $\models \bot \iff \bot$ which is trivial.

($\Leftarrow$) Assume $\models G \iff \bar G$. We need to prove $\models F$. Let $A$ be an assignment for $F$. Extend it to $B:=A[P\mapsto \top]$. We have $$B \models G \iff \bar G$$ which is $$B \models (P \land \lnot F) \iff (\lnot P \land \lnot \bar F)$$ which, thanks to the choice of $B(P)$ simplifies to $$B \models \lnot F \iff \bot$$ hence $B \models F$, and we also have $A \models F$ since $P$ does not occur in $F$.

• The first part is helpful, the assumption you took about checkSymmetry in the second part is wrong, it does take F and A as input. – Anna Vopureta Jul 21 '17 at 16:15
• I updated the question, what do you think about reducing checkUnsatisfiability to checkSymmetry in polynomial time? – Anna Vopureta Jul 21 '17 at 21:49
• @AnnaVopureta It is impossible unless P=NP fpr the same reason. You are still trying to reduce a hard problem to a easy one -- if you could do that efficiently, the first problem would not be hard. – chi Jul 21 '17 at 22:12
• You are right, my efforts were going in the wrong direction, I updated the question, does it make sense now? – Anna Vopureta Jul 21 '17 at 22:29
• @AnnaVopureta The other direction is trivial: in polynomial type you can check for symmetry during the reduction, then output any fixed satisfiable (if not symmetric) or unsatisfiable (if symmetric) formula. Any PTIME problem can be reduced in PTIME to any nontrivial problem. – chi Jul 21 '17 at 23:32