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?


2 Answers 2


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.

  • $\begingroup$ thank you very much for the answer but can you please further explain what you mean by Vi,k? each clause consist of different variables Vi or -Vi, so i’m not sure what you mean by Vi,k. Also same miss understanding about ^(and) i,k. Could u add a little example? $\endgroup$ Dec 2, 2018 at 19:18
  • $\begingroup$ @user4464936 Sorry, I meant term. So $v_{i,k}$ can be the variable or the negated variable as it appears in the original clause. $\bigwedge_{i,k}$ means the conjunction for all valid $i, k$. $\endgroup$
    – orlp
    Dec 2, 2018 at 19:49

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.

  • $\begingroup$ This reduction goes in the wrong way. It shows that if MaxSAT is in P, then SAT is in P. The question asks to show the reverse. $\endgroup$
    – D.W.
    Apr 5, 2019 at 15:18
  • $\begingroup$ You're right - let me see if I can modify it. $\endgroup$ Apr 6, 2019 at 9:06

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.