D-Wave vs CPLEX Comparison. Part 3: WMAX2SAT
How good is CPLEX for the last series of test problems used in this McGe Let's map the traditional definitions of 2SAT, MAX2SAT, and WMAX2SAT problems into mathematical programing. We have binary variables x1,...,xn. A literal is either a variable xi or its complement (1-xi). A clause is a constraint of the form sumi li>= 1 where the li 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 ui and vi with weight wi by wi: ui + vi >= 1 The WMAX2SAT problem is to find values for the variables xi such that the sum of the weights of the violated clauses is minimized. As shown in McGeoch & Wang, such problems are equivalent to minimize sumi wi (1 - ui)(1 - vi) The rationale is the following. A clause wi: ui + li >= 1 is violated if and only if ui = vi = 0, i.e. if and only if (1 - ui)(1 - vi) = 1. Replacing literals by their definition and expanding literal products yields QUBOs of the form sumi<>j Qij xi xj + sumi hi xi + 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 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.
Results in McGeoch&Wang paper
As for
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.
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 zi for each clause. This variable is 1 if and only if the clause is violated. Then the objective function is minimize sumi wi zi Let's relate zi to the two variables appear in the clause: wi: ui + vi >= 1 zi is violated if and only if ui = 0 = vi . Therefore zi = (1 - ui)(1 - vi) which can be linearized using the classical McCormick inequalities. zi >= 0 zi>= 1 - xi - xj zi <= 1 - xi zi <= 1 - xj Depending on the sign of wi 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 - ui)(1 - vi). 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. |