cf:

• Othello is Solved http://arxiv.org/abs/2310.19387

• https://github.com/eukaryo/edax-reversi-AVX-v446mod2

The files containing the analysis results can be downloaded from https://doi.org/10.6084/m9.figshare.24420619 . Inside, there are 2587 csv files named like knowledge_[-OX]{64}\.csv . Please place them in the same directory as the files in this repository.

There are 2587 files with names matching the regular expression knowledge_[-OX]{64}\.csv . Each file represents computation results. Each row is a result computed by Edax. The columns, from left to right, are: the OBF representation of the position with 36 empty squares, depth fed to Edax, strength fed to Edax (100 means complete analysis), upper score bound, lower score bound, and the number of positions Edax explored.

The upper and lower score bounds represent the true theoretical values when the depth is 36 and the strength is 100. If the strength is not 100, the same value is entered, indicating a predicted value. The number of positions Edax explored is positive when the command-line option given to Edax looks like:

$ ./Edax_mod2 -solve hoge.obf -level 60 -n 1 -hash-table-size 23 -verbose 2 -alpha -3 -beta 3 -width 200

Running with these options should return the exact same number of explored positions (reproducibility was prioritized). A negative value means different command-line options were used, for instance, parallelized or different alpha and beta values.

The following has been tested with python 3.8.10.

First, execute:

$ make
$ bunzip2 -k opening_book_freq.csv.bz2
$ sh prep-edax-and-eval.sh

This will produce four executable files: p006, p007, solve33, and p008_manyeval.

p006 takes a 50-empty square position (p) and a knowledge file (k) as arguments (for details, please read Source.cpp). It checks if the position p can be weakly solved using the knowledge from file k. If it cannot, it outputs a set of "predictions" that would be sufficient for weak resolution. Even if it can be weakly solved, it still outputs a file, but it's just a CSV file with a header, indicating that the set of "predictions" is empty. Here, a "prediction" is a row in the CSV file, consisting of the OBF format of the position with 36 empty squares, lower score bound, upper score bound, and a predicted score. The prediction suggests that the game-theoretic value of that position with 36 empty squares likely falls within that range. If all "predictions" are positively resolved, then the original 50-empty square position is considered resolved. The final predicted score isn't directly related to the "prediction" itself but is provided for reference in case one wants to solve more challenging positions first.

In addition, p006 outputs files named like result_e50[-OX]{64}\.csv . If the proof is complete, this file contains the upper and lower game-theoretic value bounds as proof results.

Running all_p006.py will execute p006 in parallel for all 2587 positions.

p007 assumes that proofs using p006 are complete and that the supporting knowledge files exist. It then performs an ideal alphabeta search, outputs the number of positions explored for all visited nodes and the minimum terminal nodes required for proof. The output files are named like result_[-OX]{64}_abtree\.csv . At the same time, smaller files named like result_[-OX]{64}_e50\.csv are also output, containing the lower and upper game-theoretic value bounds for the 50-empty square position.

Running all_p007.py will execute p007 in parallel for all 2587 positions. Approximately 4GB of main memory might be needed per logical core.

solve33 operates under the assumption that output files from p007 for all 2587 positions are available. It proves, through depth-first search, that starting from any of position with 36 empty squares, one cannot reach a position where the player to move has more than 33 legal moves. This is to address potential bugs in Othello software implementations that can only store up to 32 moves.

p008_manyeval also assumes that output files from p007 for all 2587 positions are available. For all position with 36 empty squares, it evaluates the position using p006's static evaluation function and pairs the evaluation with the number of positions explored by Edax. The output is a massive CSV file for creating figures in the paper.

check_contradiction_tasklist_e50result.py is explained. Initially, when predicting the values of the 2587 positions with 50 empty squares, there were calculated bounds within which the game-theoretic value of each positions needed to be proven to demonstrate that the initial position is a draw. This script reads all the output files from p006 named result_e50[-OX]{64}\.csv and checks for contradictions between these initial predictions and the actual proven upper and lower bounds.

The script make_50_book.py is executed after the proofs for all 2587 positions with 50 empty squares have been completed. It calculates the upper and lower bounds of the game-theoretic value for all positions that can be reached from the initial position down to 50 empty squares, and writes the results to a file. The script reads all files named result_e50[-OX]{64}\.csv , conducts a depth-first search to determine the values, and outputs the results to a file named result_e50_opening_book.csv .

convert-abtree-all.py operates under the assumption that all 2588 files, including the output files named result_[-OX]{64}_abtree\.csv for all 2587 positions and result_e50_opening_book.csv, are present. The script reads every line from these files, and if the proven game result is either a "win", "win or draw", "draw", "draw or lose", or "lose" for the player to move, it compresses the position and its result into 17 ASCII characters. The script then uses UNIX's sort and uniq commands to remove duplicates and writes the results to a massive text file named all_result_abtree_encoded_sorted_unique.csv . Scripts that play moves ensuring no loss by table lookup will perform binary searches on this file.

reversi_player.py is a script that uses the all_result_abtree_encoded_sorted_unique.csv file and the Edax_mod2 executable to play Reversi as a player that never loses.

1. Download the analysis result files from https://doi.org/10.6084/m9.figshare.24420619 and place the 2587 csv files with names like knowledge_[-OX]{64}\.csv in the same directory as this repository's files.

2. Ensure you have enough storage space, as executing all_p007.py and convert-abtree-all.py in the next steps will produce text files totaling about 300GB.

3. Execute the following commands:

   $ make
   $ bunzip2 -k opening_book_freq.csv.bz2
   $ sh prep-edax-and-eval.sh
   $ python3 all_p007.py
   $ python3 make_50_book.py
   $ python3 convert-abtree-all.py
   

4. Once you have all_result_abtree_encoded_sorted_unique.csv and Edax_mod2, you're all set.

By executing

$ sh prep-edax-and-eval.sh

you can create the Edax_mod2 executable, which can be used to solve positions with 36 empty squares. Assuming p006 has been created using make, you can execute solve_all_e50_subproblems.py to solve all 2587 positions with 50 empty squares. solve_all_e50_subproblems.py is just an example of the solution process. If you truly want to solve these positions, it might be better to prepare a workflow according to the specifications of a computing cluster or similar infrastructure.