Sparsity pattern


FormulatorBill Cook
DonatorPaul Seymour
Integer Objective4.23000000e+02
LP Objective4.03846474e+02
Root LP Basisseymour.bas.gz
Set partitioning
Set packing285
Set covering4659
Equality Knapsacks
Bin packing
Invariant Knapsack
Integer Knapsack
Upper bounds
Lower bounds
Mixed 0/1
General Cons.
References CeriaFerrisLinderothPatakiSchmieta2000 FerrisPatakiSchmieta2001

The following text was copied from the website

The instance was posed by mathematician Bill Cook, as a by-product of a new proof of the Four Color Theorem by Neil Robertson, Daniel Sanders, Paul Seymour, and Robin Thomas. The Four Color Theorem states that any map can be colored using four colors in such a way that adjacent regions (i.e. those sharing a common boundary segment, not just a point) receive different colors.

The Seymour problem is to find the smallest unavoidable set of configurations that must be "reduced" in order to prove the Four Color Theorem. Here "reduced" is a technical term meaning that the configuration can be shown to not exist in a minimal counterexample to the Four Color Theorem. Seymour claims to have found a solution of value 423, but until this work, we are aware of no one (including Seymour) who has been able to reproduce a solution of this value. The problem actually has many solutions of value 423.

The problem was solved in two phases.

The first phase, carried out at Columbia University, combined the integer programming techniques of preprocessing, disjunctive cutting planes, and branch and bound to create a list of 256 problems. The list of problems created was equivalent to the Seymour problem in the sense that if all problems in the list could be solved, then the Seymour problem would be solved.

The second phase was to solve all of the problems in the list. This required an enormous amount of computational power. To garner the necessary computational resources, the Condor system for high throughput computing was used. By using Condor, the problems were able to be solved during idle time on workstations at the University of Wisconsin-Madison, the Alberquerque High Performance Computing Center, the Argonne National Laboratory, the National Center for Supercomputing Applications (NCSA), and Columbia University's Computational Optimization Research Center.

The authors find it interesting to note that the Seymour problem itself was solved in a similar way to which the Four Color Theorem was proved. First a small list of objects that needed to be "checked", or "reduced" was determined. Computers were relied upon to do this checking. It took less than four hours of CPU time to complete the proof of the Four Color Theorem. Proving that 423 was the optimal solution to the Seymour problem took more than 9000 CPU hours.

To solve the problems, the commercial integer progamming software packages CPLEX and XPRESS-MP were used. We greatly acknowledge the support of both ILOG, Inc. and of Dash Associates for the use of their software.

Last Update : 2010/06/09 13:56:11 $ by Gerald Gamrath
© 2010 by Konrad-Zuse-Zentrum für Informationstechnik Berlin (ZIB)