Suppose we have an instance of the Max-SAT problem given by . Design an ILP with the variables for each variable in (with ) and for each clause in (with ).
Now add the following constraints,
this will relate to the variables and clauses being true or false.
To add constraints to reflect the clauses suppose contains positive literals involving variables and negative literals . So we have the clause
For each clause add the following constraint
this guarantees for integer points can only be 1 if for some or for some .
Lastly to define the reduction, we need to define the objective function
This reduction takes time , as we need to go through each clause to convert them into functionals. So this takes polynomial time.
When provided with a solution to the ILP return the solution to the Max-SAT problem with true for all and false for all . This takes time so takes polynomial time.
Let be the max value of the constructed ILP and be the max value of Max-SAT. From Claim 1 we have . Equally Claim 2 gives us . This provides that and we have the solution of the contracted ILP if and only if we have a solution to the Max-SAT problem.
Claim 1
Claim 1
An assignment to the variables of is reversed transformed into a feasible point in the contracted ILP and the value of its objective function is the number of satisfied clauses.
Proof of Claim 1
Set and , 1 if true and 0 if false. This satisfies the bounds on the variables and they are integers. The clause constraint
is satisfied as if there is a literal making true the corresponding value of or is 1 allowing to be 1.
The objective function
is the number of satisfied clauses by definition.
Claim 2
Claim 2
A feasible point in the constructed ILP is transformed into a valid assignment of the variables and the value of the objective function is less than or equal to the number of satisfied clauses.
Proof of Claim 2
We set with being True and being False. The clause constraint
guarantees that if this assignment doesn’t satisfy then as and