Let us present an integer linear formulation of this problem. So, for every clause C(i) we define by T(i) the set of Boolean variables that appear unnegated in cross C(i). And by F(i) the set of Boolean variables that appear negated in clause C(i). Now let's describe the variables of the integer linear program formulation. We have a variable for z(i) for every clause that is equal to 1 if the clause is satisfied, 0 otherwise. We have also a variable x(j) for every boolean variable. This Boolean variable is 1 if variable x(j) is true, 0 otherwise. So, which is our integer linear programing formulation. We want to maximize the weight of a satisfied clause. So, the objective function would be the sum over all the clauses of the product of the weight of the clause times the variable that indicates if the clause is satisfied. On the other hand, the clause to be satisfied, since every clause is in disjunctive form, must have at least one true literal true. So, for all of the true literals in the clause, we have that the sum of the variables x(j) for all the true literals plus the sum of all the negated variables for all the negated literals must be at least z(i). This means that a Boolean variable associated with a true literal must be 1 or a Boolean variable associated with a false literal must be 0. Moreover, in the integer linear programing formulation of this problem we have that x(j) and z(i) must be either 0 or 1. We do is to drop these integral constraints so that x(j) may be any variable between 0 and 1. z(i) must be between 0 and 1. And, this has no interpretation in terms of setting to true or to false a variable because setting a variable to an intermediate value is senseless. But we will see how we can exploit this in our rounding scheme.

---