Why is Max SAT in P if SAT in P?

Question

It holds that if SAT could be solved in poly time, one can also find in poly time the assignment that satisfies most clauses of the original formula. Does anyone have any idea how to show this? Let's assume we have algorithm A to decide in poly time if a given formula could be satisfied or not. How one can use this to find in poly time the assignment that satisfies most clauses. I know that using this assumption leads to also being able to find satisfying assignment in poly time (if the formula is in SAT), but if the formula is not in SAT how can we find what is the sub-formula with maximum clauses that belongs to SAT without iterating over the powerset of the clauses which will lead to exp time algorithm?

Answer 1

Suppose that you have a CNF formula $x$ with input size $n$, and that you can solve $\text{SAT}$ in $O(n^c)$ time for some constant $c$.

We construct a new formula $y$. For each clause $l_i$ in $x$, with terms $v_{i,k}$, add a new variable $t_i$ and the CNF clauses $\bigwedge_i(\neg t_i \vee l_i)$ and $ \bigwedge_{i,k} (t_i \vee \neg v_{i,k})$.

Now this formula is only satisfiable if $t_i$ is assigned a truth value equal to $l_i$, and our input size is bounded by linear function of the original size. We then add a "at least $k$ out of $n$" constraint to this formula on the $t$ variables. This also adds a polynomial number of clauses. Now the formula is only satisfiable if at least $k$ clauses of the original formula are satisfiable.

Now we can simply solve $\log_2(n)$ instances of the above formula, doing a binary search with $k$ to find the maximal number of clauses that are satisfiable simultaneously.

Answer 2

This is the reduction from SAT to MaxSAT given we have a polynomial time algorithm for MaxSAT. Take some instance of a SAT problem $f$. Since SAT requires all clauses in $f$ be satisfied or return that none exists, we can set $k=m$ and run Max_SAT($f=(CNF),k=m$). If exactly $k$ clauses in $f$ are satisfied, it returns the solution. If less than $k$ clauses are satisfied, MaxSAT returns No which would also match the output of a SAT solver.