# How to reduce MaxUNSAT to MaxSAT?

Is it possible to reduce MaxUNSAT to MaxSAT in a polynomial way ?

When considering the MaxSAT problem, one often considers also the MinUNSAT problem, which is almost the same. And for a propositional formula f in CNF it holds:

|f| = MaxSAT(f) + MinUNSAT(f)


where |f| is the number of clauses of f.

When considering MaxUNSAT and the corresponding MinSAT problem, the same relationship holds:

|f| = MaxUNSAT(f) + MinSAT(f)


Now, I was wondering if there is also a relationship between those two pairs, e.g. to reduce MaxSAT to MaxUNSAT or MinSAT (or the other way round) ?

Unfortunately, I could not figure out one by myself. And maybe there is none ?

Update 1: Inspired by Yuval Filmus's answer, I will give a reduction for my question.

Reduction from MaxUNSAT to its corresponding decision problem:

Let $$\phi = {C_1, ..., C_m}$$ a set of clauses over the variables $$x_1, ..., x_n$$, then it holds: $$MaxUNSAT(\phi) = BinarySearch(0, |\phi|, MaxUNSAT(\phi, k) )$$ with

BinarySearch(start, end, CompareProcedure( )):

Searches for the element e between start and end so that CompareProcedure(e)=true and CompareProcedures(e+1)=false

and

$$MaxUNSAT(\phi, k) := \exists v\in\{0, 1\}^n:\sum_{i=1}^m 1 - I_v(C_i) \geq k$$ where $$I_v$$ is the interpretation of a propositional formula under assignment $$v$$.

Reduction from decision problem $$MaxUNSAT(\phi, k)$$ to SAT:

One can reduce the devision problem $$MaxUNSAT(\phi, k)$$ to the SAT problem by adding blocking variables to each clause and adding a cardinality constraint as propositional formula to limit the number of used clauses with help of the blocking variables.

I can describe this in more detail, if needed.

Conculsion:

One can reduce the MaxUNSAT problem to the SAT problem and then solve the SAT problem with the MaxSAT problem. This is a reduction that works in polynomial time.

• I do not think that it is fair to change the question significantly after you receive an answer. – Tsuyoshi Ito Sep 24 '12 at 16:59
• I do not think it has changed significantly. The question just changed from "How to reduce ... " to "How to reduce it in a more direct way". But if you want, I can break this question into two questions (open up a new question for the second one) to make things more clear/fair ? – John Threepwood Sep 24 '12 at 21:27
• I personally think so, because Yuval has already answered your original question and it seems that the purpose of your edit in revision 5 is to make his answer invalid. Other people may think otherwise, though. – Tsuyoshi Ito Sep 24 '12 at 21:44
• Yuval Filmus did not answer my question. He proved that there exists a reduction, but my question was not "Is it possible to reduce" but "How to reduce". So either way, his answer helped me to find a reduction, but did not provide a solution by itself. Therefore, my change did not touch his answer. But I understand the confusion of the change and to make things clear/fair again, I will open up a new question and rephrase this one to its original. – John Threepwood Sep 24 '12 at 21:54

Both MaxSAT and MaxUNSAT are NP-complete, and so can be reduced to one another. MaxSAT is NP-hard by (trivial) reduction from SAT. To see that MaxUNSAT is NP-hard, we follow Creignou [1] and reduce from MaxCUT. Given an instance $G=(V,E)$ of MaxCUT, consider the instance $$\bigwedge_{(x,y) \in E} (x \lor \lnot y) \land (\lnot x \lor y).$$ Each cut corresponds to a $0/1$ assignment to the vertices. If an edge $(x,y)$ is separated by a cut, then one of the two corresponding clauses will be unsatisfied, and otherwise none will be unsatisfied.