How good is CPLEX  for the last series of test problems used in this McGeoch&Wang paper?  Remember, it is this paper that compared a specialized hardware from the D-Wave company with three software solvers, including CPLEX.  It generated lots of buzz because (a) D-Wave machine is claimed to be a quantum computer, and (b) because reported results show a dramatic speedup compared to CPLEX.  The paper used three series of test problems for the comparison.  We have revisited and improved CPLEX results dramatically on two test series as shown in previous blog entries: D-Wave vs CPLEX Comparison. Part 2: QUBO and D-Wave vs CPLEX Comparison. Part 1: QAP.   We now report results obtained on the last series, namely weighted max 2 sat problems (WMAX2SAT).

Let's map the traditional definitions of 2SAT, MAX2SAT, and WMAX2SAT problems into mathematical programing.  We have binary variables x₁,...,x_n.  A literal is either a variable x_i  or its complement (1-x_i).  A clause is a constraint of the form

sum_i l_i>= 1

where the l_i are literals.  If there are 2 literals we say it is a 2-clause

A 2SAT problem is decision problem where the constraints are 2-clauses. Given a 2SAT problem, the associated MAX2SAT problem is an optimization problem where the objective function is to maximize the number of clauses that can be satisfied.  The weighted MAX2SAT (WMAX2SAT) problem is a generalization where each clause has a weight, and the sum of the weights of the satisfied clauses has to be maximized.  Equivalently one can minimize the sum of the weights of the unsatisfied clauses. 

We will denote the clause with literals u_i and v_i with weight w_i by

w_i: u_i + v_i >= 1

The WMAX2SAT problem is to find values for the variables x_i such that the sum of the weights of the violated clauses is minimized. As shown in McGeoch & Wang, such problems are equivalent to

minimize sum_i wi (1 - u_i)(1 - v_i)

The rationale is the following.  A clause w_i: u_i + l_i >= 1 is violated if and only if u_i = v_i = 0, i.e. if and only if (1 - u_i)(1 - v_i) = 1.

Replacing literals by their definition and expanding literal products yields QUBOs of the form

sum_i<>j Q_ij x_i x_j + sum_i h_i x_i + R

For instance, let's look at a very simple problem with one clause:

2: x + y >= 1

this is equivalent to

minimize 2(1-x)(1-y)

yielding this QUBO

minimize 2xy -2x -2y + 2

McGeoch&Wang took 120 random instances from 2012 Max-SAT Evaluation competition  and modified them by generating random weights of the form -7.5 + k with k being a random integer in [0, 15].  These instances have 100,120, or 140 variables and between 1200 and 1600 clauses.

CPLEX was run with a time limit of 1800 seconds.  Results published in the paper are given in the table below.  It reads as follows.  At n = 100, CPLEX was able to find 30 optimal solutions (of 40 instances) and to certify optimality in 10 cases. In all tests the CPLEX solution was never observed to be more than 7.5 units from optimal.

n	100	120	140
CPLEX finds	30	31	33
CPLEX certify	10	13	11
max Dcp	7.5	6.5	5.5

Results in McGeoch&Wang paper

As for the QUBO test series we looked at four ways to (possibly) improve CPLEX performance compared to the results reported in the paper:

1. Use the latest CPLEX 12.5.1 release instead of the two years old 12.3 used in the paper
2. Use parallelism. CPLEX was limited to using one thread in the paper.
3. Use some CPLEX parameter tuning
4. Use alternative ways of modeling the test problems

We first reused what gave the best results for the QUBO series, namely running CPLEX 12.5.1 on a 32 core machine with aggressive use of Gomory fractional cuts and zero half cuts on a model where product of variables were automatically linearized.  Results are given below.  We report the timings for finding the best solution and prove it is optimal.  As  before, the mean is the shifted geometric mean.

n	min	mean	max
100	8.1	17.1	89
120	6.1	17.3	87
140	6.5	16.8	79

QUBO solving times with 32 threads in seconds

We see that CPLEX takes about 17 seconds on average to do it, with a worst case of 89 seconds.  We also see that CPLEX running time does not depend much on the number of variables.

Our results are dramatically better than those reported in the paper.  First of all, we are able to find and certify all optimal solutions in less than 90 seconds, whereas CPLEX could only certify about 1/4 of the solutions within 1800 seconds.  Let's evaluate the speedup.  The 10th fastest time for n=100 is 10.5 seconds.  It means that in at most 10.5 seconds we can find best solution and certify optimality of 10 problem instances.  In the paper this required up to 1800 seconds.  We therefore have a speedup of  170x (1800/10.5) .  Similarly for n=120, the 13th fastest time is 11.4, hence we have a speedup of  about 160x (1800/11.4).  Last, the 11th fastest time for n=140 is 11.8, which yields a speedup of  about 150x (1800/11.8).  Depending on the set of problems the speedup is between 150 and 170.  What took 1800 seconds in McGeoch&Wang experiments now takes about 11 seconds. 

How does it look compared to other methods studied in the paper? Results were reported graphically as follows.

With our new results the green boxes (for CPLEX) would now be similar to the blue boxes (the ones for the complete solver ak) for n=140.  CPLEX would be therefore be in the same league as the specialized complete solver ak.  It would also be not that far from heuristic methods, which is quite good given CPLEX certifies optimality of the solutions it finds.

Let's end with a discussion of how to best model WMAX2SAT problems as a MIP.   We would model clause violation with a new binary variable z_i for each clause.  This variable is 1 if and only if the clause is violated.  Then the objective function is

minimize sum_i w_i z_i

Let's relate z_i to the two variables appear in the clause:

w_i: u_i + v_i >= 1

z_i is violated if and only if u_i = 0 = v_i .  Therefore z_i = (1 - u_i)(1 - v_i) which can be linearized using the classical McCormick inequalities.

z_i >= 0

z_i>= 1 - x_i - x_j

z_i <= 1 - x_i

z_i <= 1 - x_j

Depending on the sign of w_i only two of the constraints need to be stated.   Simple isn't it?

Wait a minute, isn't that what McGeoch&Wang did?  Indeed, they also used the products (1 - u_i)(1 - v_i).  Shouldn't this yield to the same problem once linearized?  The short answer is not always.  For instance, let's look at a very simple problem with one clause:

2: x + y >= 1

which is equivalent to this QUBO

minimize 2xy -2x -2y + 2

We would then linearize this with an extra variable z = xy, yielding

minimize 2z -2x -2y +2

subject to

z -x -y >= -1

z >= 0

Our direct approach would yield this model, where z is the variable associated to the violation of the clause

minimize 2z

subject to

x + y + z >= 1

z >= 0

In general our model only contains the newly introduced variables in the objective function whereas the linearization of McGeoch&Wang models also have terms involving the original variables.  Both models have the same number of constraints, two per clauses.  It would have been nice to be able to compare the performance of both approaches.  Unfortunately we were only provided the QUBOs, not the WMAX2SAT problems.

It would be tempting to reconstruct the latter ones by undoing the transformation into QUBOs.  Unfortunately this is not a 1 to 1 transformation. For instance, this MAX2SAT problem

 1: x + y >= 1

-1: x + (1-z) >= 1

-1: y + z >= 1

yields this QUBO

minimize xy + xz - yz - x

This other WMAX2SAT problem yields the same QUBO.

-1: x + (1-y) >= 1

 1: x + z >= 1

-1: y + z >= 1

It may not be an issue for such simple problem, but undoing the transformation for larger problems looks like a combinatorial problem in itself.  Solving it is way beyond the experiment we wanted to perform.