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

bridge 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

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s