We are testing a new “properties” version of the program. We decided to use the hamiltonicity of a graph as our test property. We are generating upper and lower bounds (necessary and, respectively, sufficient) conditions for a graph to have a hamiltonian cycle. Instead of automatic search for counterexample to generated conjectures, we are finding them ourselves – as we watch how the program is performing. On the 11th round of the lower bound conjectures, the program conjectured:
Here’s the entire Sage cell, together with the list of objects the program knows and the command to run the program.
#11 adding K~wWGKA?gB_N and K~wWGGB?oD_N which are CE’s to first conjecture of round #10
objects = [graphs.CompleteGraph(3), graphs.CycleGraph(4), graphs.PathGraph(4), graphs.PetersenGraph(), c4c4, graphs.StarGraph(3).cartesian_product(graphs.CompleteGraph(2)), graphs.CycleGraph(7), graphs.ChvatalGraph(), graphs.TutteGraph(), Graph(‘J~wWGGB?wF_’), c5c5, c3p2, Graph(“K~wWGKA?gB_N”), Graph(“K~wWGGB?oD_N”)]
propertyBasedConjecture(objects, properties, property, theory = theory, verbose = false, debug = false)