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.

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.

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(k)) := \\\text{Searches for the element $e$ between $start$ and $end$ with help of the $CompareProcedure(k)$, so that holds $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.

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.

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(k)) := \\\text{Searches for the element $e$ between $start$ and $end$ with help of the $CompareProcedure(k)$, so that holds $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 changed the question a bit, because what I really wanted to know is:

Question: Is there a more direct reduction without much overhead from MaxUNSAT to MaxSAT (or to minUNSAT)?

Something like $MaxUNSAT(\phi) = MaxSAT(\neg\phi)$ (which does not work).

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(k)) := \\\text{Searches for the element $e$ between $start$ and $end$ with help of the $CompareProcedure(k)$, so that holds $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.