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


$$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.


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.

  • 1
    $\begingroup$ I do not think that it is fair to change the question significantly after you receive an answer. $\endgroup$ Sep 24 '12 at 16:59
  • $\begingroup$ 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 ? $\endgroup$ Sep 24 '12 at 21:27
  • $\begingroup$ 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. $\endgroup$ Sep 24 '12 at 21:44
  • $\begingroup$ 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. $\endgroup$ 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.

[1] Creignou, A dichotomy theorem for maximum generalized satisfiability problems, JCSS 51, 511-522 (1995).

  • 1
    $\begingroup$ Thank you. I updated my question with help of your answer. But you have to be careful with the term NP-complete when talking about optimization problems (which are not decision problems). $\endgroup$ Sep 24 '12 at 8:23

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.