# Automated Counterexample Search for Properties Conjectures

After several hitches, Nico has the properties-conjecture engine running smoothly: at least one Sage invariant (treewidth) runs too slowly to be useable for our purposes.

Now we can run the program in fully-automated mode: the program starts with the pre-existing list of graphs it knows, generates conjectures, looks for counterexamples, adds them to the list of graphs and repeats. For the following run the program was set to search for counterexamples with up to 8 vertices and to do as many as 3 “steps” or repetitions of this process. The engine will stop either when it runs out of potential counterexamples, or after three steps had been completed.

In the following run (the first non super-small testing run) the program generates 3 conjectures, finds and adds counterexamples to them, and finally generates a fourth conjecture which is true for all graphs with (at least 3 and) up to 8 vertices. (The properties are built-in Sage graph properties or have definitions that can be found in the file gt.py).

Found the following conjectures:

(is_hamiltonian)->(((is_planar)->(is_anti_tutte2))&(is_van_den_heuvel))

Looking for counterexamples with 3 vertices

Looking for counterexamples with 4 vertices

Adding Graph on 4 vertices: C^

Found the following conjectures:

(is_hamiltonian)->(((has_empty_KE_part)->(is_anti_tutte2))&(is_van_den_heuvel))

Looking for counterexamples with 3 vertices

Looking for counterexamples with 4 vertices

Looking for counterexamples with 5 vertices

Â Adding Graph on 5 vertices: DU{

Found the following conjectures:

(is_hamiltonian)->(((is_cubic)->(is_anti_tutte2))&(is_van_den_heuvel))

Looking for counterexamples with 3 vertices

Looking for counterexamples with 4 vertices

Looking for counterexamples with 5 vertices

Looking for counterexamples with 6 vertices

Looking for counterexamples with 7 vertices

Looking for counterexamples with 8 vertices

No counterexample found

The conjectures are stored in the variable conjectures.

[(is_hamiltonian)->(((is_cubic)->(is_anti_tutte2))&(is_van_den_heuvel))]

The property is_anti_tutte2 is one that the invariant conjecturing found that was true for all the hamiltonian graphs it knew about – but false for the (non-hamiltonian) Tutte graph. A graphs g is anti_tutte2 if and only if:

independence_number(g) <= domination_number(g) + g.radius() 1