This website contains the code for the numerical computation discussed in S. Heilman, A. Jagannath, and A. Naor, ``Solution of the Propeller Conjecture in R3''. This code was run many times on several different computers. The techincal requirements for the code are quite modest, with the processor speed only affecting the total run time and the total memory requirement being less than 200 Mb. You can run it on anything from a dedicated compute server to a laptop computer (we have tried both).
We ran the code in two different ways. The simplest way was to run it in a serial fashion. That is, we ran the program as a single instance which performed each step of the algorithm described in the paper one after the other. This took 37.8 hours to complete on a single processor of a compute server with 3.3 GhZ Intel Xenon processors. The second way we ran it was to parallelize the algorithm by breaking up the domain of interest into 7 distinct portions and running separate instances on each. This took 12.8 hours when split up between seven 2.4 GhZ AMD Opteron processors.
Please feel free to download the code and run it on your own computer so that you understand how straightforward a process runnning the proof actually is. As written the code should compile on any machine. To obtain the code, just download the tar-ed gzipped file to what ever directory you wish, unzip and untar it (type ``tar -xvzf propeller.tar.gz''). If you happen to be working on a linux or mac, compiling the code is particularly easy. Just type ``make'' in the directory that contains the code. This should work provided your system has g++ (which mac and linux systems do). Alternatively, you can run a precompiled version available here. Currently, Windows is not supported. If you wish to run this on a windows computer you must compile the code yourself.
We have written a command-line user interface so that interacting with the code is easy. To run the proof (serially), type ``./the_proof -e prove_the_theorem''. To test that the code is running as we say it is, type ``./the_proof -e test_suite'' and the functional tests described below will run. To generate the plots demonstrating that the grid refinement procedure is working (see functional testing of the net refinement ), simply type ``python test_refinement.py'' after you have run the test suite. Please note that this plotting procedure will require access to a computer with python and matplotlib (a python plotting package). This is now default in Mac OSX Lion. If at any point you have an issue, just type ``./the_proof'' and a help page will appear.
The code can be obtained in two ways. It is available as a single tar-ed gzipped file . It is also available for download on a by file basis here , and precompiled here (When you download the precompiled file, please rename the file from ``the_proof.o'' to ``the_proof''. The filename was purposely changed for the website to avoid issues with many operating systems/browsers which to convert the file to text rather than treating it as an executable.)
The code is broken up in to 5 distinct files.
This component of the code is intended to extend the standard arithmetic functionality in c++ to work for lists with 3 elements. All arithmetical operations are performed pointwise. It also implements a few of the standard metrics on R3 and related functions.
The functional testing component of this code, test_list_arith(), demonstrates that the list arithmetic works correctly to the accuracy stated in Heilman et al.
We extend and/or replace basic mathematical functions in the standard cmath library. These replacements/extensions are created so that we can have explicit control over the error properties of the functions involved.
Currently the functional testing suite just demonstrates that the functions do obtain typical values when evaluated.
This portion of the code contains all of the code relevant to the generation and refinement processes for the net that we use in the problem.
It is important to demonstrate that this portion of the code does in fact perform the proper refinement. This is discussed in the page on functional testing of the net refinement . There you will find an explaination of the refinement procedure, a demonstration of it in action as well as information on how to use the functional testing code and scripts.
This contains all of the bounds used in the proof of the theorem. These bound are rigorous in the sense that they have been relaxed so as to account for possible numerical error in their evaluation.
This contains the code that parses the command-line input from the user, as well as the outlines of the major components of the theorem.
The basic command-lines are described by the help menu that appears when one runs ''./the_proof'' without passing any arguments.
Using the command-line user interface is fairly straight forward. As described above, proving the theorem serially and testing the code are particularly easy. Proving the theorem in a parallelized fashsion is also straight-forward but requires more work on the part of the user.
To parallelize the proof, begin by typing ''./the_proof -e generate_first_list''. This begins the process by traversing the net with grid spacing π/100, refining to a grid spacing of π/1000, and traversing this new net. It will then produce a file called ``the_list_pi_by_1000.l''. This is the list of points that remain after running this process. From here the user can refine different portions of the_list_pi_by_1000.l individually using the refine_the_list experiment.
Suppose that I wanted to refine the first 500000 points in the_list_pi_by_1000.l to a grid spacing of π/10000 and run the traversal on this new region. To do so I would run ``./the_proof -e refine_the_list -f the_list_pi_by_1000.l -n 0 500000 -r 1001 10001''. The argument -f [filename] specifies the file to be refined. The argument -n [first] [last] specifies from what line to what line we wish to refine. The argument -r [old] [new] tells the program to refine from a grid spacing of π/(old+1) to a grid spacing of π/(new+1).
To complete the proof, the user must perform the refine_the_list experiment repeatedly on the subsets of the grid generated by the code until all of the files put out by the code are empty.