Tha bj-phi program that comes with the library generates HTML pages with cytoscape.js graphs to visualize the solving of Pigeon Hole Principle (Pigeonhole or PHP) instances.
This example shows that the ben-jose SAT solver can be trained and that it generates short proofs for Pigeon Hole Principle instances.
Assuming the program ''bj-phi'' is in the path, and from the source tree directory, do:
cd ben-jose/src/programs/tests/phi sh clean_sh bj-phi 4 firefox ./phi_hole_4/phi_hole_4_all_steps.htm &
will execute the bj-phi program for PHP-4 and it will use the file
./dbg_ben_jose.conf
to configure the debugging system to generate an HTML log file of the the solving process for PHP-4. In this link you can find the output of the first run. To understand the output relate to the code in github, it's documentation, and to the paper explaining the proposed trainable strategy to SAT solving.
In order to restart the original state before the first run: that is to delete the {\skeleton} and the generated files by bj-phi simply run:
sh ./clean_sh