[FOM] Formally verifying "checkers is a draw"

[martdowd at aol.com]

I have an example of computer verification.  According to Bondy and Hemminger Manvel conjectured in 1970 that colored graphs were reconstructible.  Weinstein claimed in 1979 that edge colorings of K_5 are reconstructible.  As one topic of s psper on colored graph reconstruction, I decided to check this for K_6.  After laboriously enumerating the edge colorings of K_6 (using Nauty), I first checked the claim for K_5.  A counterexample was found, in under a second, which is easily checked by hand.

This was all done with combinatorial enumeration using Nauty.  The paper will appear in IJPAM; if anyone would like a copy I will temporarily put it on my web site www.hyperonsoft.com.

- Martin Dowd

 

 

 

-----Original Message-----
From: Timothy Y. Chow <tchow at alum.mit.edu>
To: Foundations of Mathematics <fom at cs.nyu.edu>
Sent: Sun, Aug 3, 2014 12:16 pm
Subject: Re: [FOM] Formally verifying "checkers is a draw"


On Sun, 3 Aug 2014, Josef Urban wrote:
> Both the Four Color theorem and Flyspeck involved at some point 
> enumeration of a large number of cases. If I understand correctly, the 
> technique used in both cases was (essentially) to verify the 
> case-enumerating algorithms and run them, instead of verifying the 
> certificates. It would be interesting to compare the orders of magnitude 
> dealt with with in those cases with Schaeffer's.

Thanks for the pointers.  I found this relevant paper:

http://arxiv.org/abs/1301.1702

The abstract says, in part, "The Flyspeck project includes about 1000 
nonlinear inequalities. We successfully tested our method on more than 100 
Flyspeck inequalities and estimated that the formal verification procedure 
is about 3000 times slower than an informal verification method 
implemented in C++."

As for the four-colour theorem, the Robertson et al. proof involved only 
633 configurations, so I assume that the Coq proof involved a similar 
number of configurations.

For comparison, the Schaeffer et al. paper says, "The stored proof tree is 
only 10^7 positions. Saving the entire proof tree, from the start of the 
game so that every line ends in an endgame database position, would 
require many tens of terabytes, resources that were not available. 
Instead, only the top of the proof tree, the information maintained by the 
manager, is stored on disk.  When a user queries the proof, if the end of 
a line of play in the proof is reached, then the solver is used to 
continue the line into the databases. This substantially reduces the 
storage needs, at the cost of recomputing (roughly 2 min per search)." 
Later on the paper also says, "How much computation was done in the proof? 
Roughly speaking, there are 10^7 positions in the stored proof tree, each 
representing a search of 10^7 positions (relatively small because of the 
extensive disk operations). Hence, 10^14 is a good ballpark estimate of 
the forward search effort."

I hesitate to draw firm conclusions without understanding the details 
better, but it sounds to me like the checkers case is many orders of 
magnitude larger than the four-color case or the Flyspeck case (even 
granting that the Flyspeck project involves additional tedious 
computations beyond the nonlinear equations).  It sounds like one might 
either have to write down 10^14 cases, or write down a database of 10^7 
cases and deal with a lot of computation---perhaps 10^7 * (2 min) * 3000?

Tim
_______________________________________________
FOM mailing list
FOM at cs.nyu.edu
http://www.cs.nyu.edu/mailman/listinfo/fom

 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20140805/e4e6e5a2/attachment.html>