Day4.sagews

#this the conjecturing program
load("conjecturing.py")

#this is a list of pre-coded graphs, properties, and invariants
load("gt-nb.sage")

loaded utilities loaded invariants loaded properties loaded theorems loaded graphs Remember to load DIMACS and Sloane graphs if you want them

k3 = graphs.CompleteGraph(3)
#[(is_clique)->(is_hamiltonian)] is TRUE
k3_4 = graphs.CompleteBipartiteGraph(3,4)
k5_5 = graphs.CompleteBipartiteGraph(5,5)
#(is_cycle)->(is_hamiltonian) is TRUE
k2 = graphs.CompleteGraph(2)
EH = graphs.EllinghamHorton54Graph()
#CLAIM: ((is_strongly_regular)&(is_bipartite))->(is_hamiltonian) is true for n>2
#NB presented a proof: we need to write this up!
pete = graphs.PetersenGraph()
c5 = graphs.CycleGraph(5)
fish = Graph([(0,1),(1,2),(2,3),(3,4),(4,5),(5,2),(2,0)])
c5_tail = graphs.CycleGraph(5)
#c5_tail.add_vertex()
c5_tail.add_edge(0,5)
bow_tie = Graph(5)
bow_tie.add_edges([(0,1),(1,2),(2,3),(3,4),(4,2),(2,0)])
c7 = graphs.CycleGraph(7)
c7_chord = graphs.CycleGraph(7)
c7_chord.add_edge(0,2)
glasses = Graph(7)
glasses.add_edges([(0,1),(1,2),(2,3),(3,4),(4,5),(5,6),(6,3),(3,0)])
p3 = graphs.PathGraph(3)
k5 = graphs.CompleteGraph(5)

triangle_with_tail = graphs.CompleteGraph(3)
triangle_with_tail.add_edge(0,3)
blanusa2 = graphs.BlanusaSecondSnarkGraph()
duplex = Graph("Iv?GOKFY?")
heawood = graphs.HeawoodGraph()
frucht = graphs.FruchtGraph()

#Run 5 of Day 3
#duplex is a counterexample to: planar & regular implies hamiltonian

current_graph_objects = [k3,pete,c5,k5_5,k3_4,EH,c7_chord,bow_tie,k5,p3,glasses,fish,c5_tail,triangle_with_tail]
current_graph_objects.append(blanusa2)
current_graph_objects.append(frucht)
current_graph_objects.append(heawood)
current_graph_objects.append(duplex)

#properties = [Graph.is_hamiltonian, Graph.is_clique, Graph.is_regular,Graph.is_cycle,Graph.is_bipartite,Graph.is_chordal,Graph.is_strongly_regular,Graph.is_eulerian, Graph.is_triangle_free, Graph.is_distance_regular, Graph.is_perfect, Graph.is_planar]

#the properties list used in the conjecturing program will be the on from gt.sage

property_of_interest = properties.index(Graph.is_hamiltonian)

theorem1 = lambda g: g.is_bipartite() and g.is_strongly_regular()

theorems = [Graph.is_cycle, Graph.is_clique, theorem1]

conjs = propertyBasedConjecture(current_graph_objects, properties, property_of_interest, theory = theorems)
for c in conjs:
    print c

((is_van_den_heuvel)&(is_planar))->(is_hamiltonian) ((is_perfect)&(is_distance_regular))->(is_hamiltonian)

for g in current_graph_objects:
    if diameter_equals_radius(g) and is_van_den_heuvel(g) and not g.is_hamiltonian():
        print g

Blanusa Second Snark Graph

for g in current_graph_objects:
    if g.is_planar() and is_van_den_heuvel(g):
        print g.name()

Complete graph Cycle graph Cycle graph Frucht graph

frucht.show()

for g in current_graph_objects:
    print g
    g.show()

alpha_critical_Bw

Petersen graph

Cycle graph

Complete bipartite graph

Complete bipartite graph

Ellingham-Horton 54-graph

Cycle graph

Graph on 5 vertices

Complete graph

p3

Graph on 7 vertices

fish

Cycle graph

Complete graph

Blanusa Second Snark Graph

Frucht graph

Heawood graph

Graph on 10 vertices

blanusa2.is_hamiltonian()

False

frucht.is_hamiltonian()

True

#neal's CE to 2nd conjecture
nb1 = Graph("Edj_")
nb1.is_planar()
is_van_den_heuvel(nb1)
nb1.is_hamiltonian()
nb1.show()

True True False

#Run 1 of Day 4
#add nb1: CE to: (is_van_den_heuvel)&(is_planar))->(is_hamiltonian
current_graph_objects = [k3,pete,c5,k5_5,k3_4,EH,c7_chord,bow_tie,k5,p3,glasses,fish,c5_tail,triangle_with_tail]
current_graph_objects.append(blanusa2)
current_graph_objects.append(frucht)
current_graph_objects.append(heawood)
current_graph_objects.append(duplex)
current_graph_objects.append(nb1)

#properties = [Graph.is_hamiltonian, Graph.is_clique, Graph.is_regular,Graph.is_cycle,Graph.is_bipartite,Graph.is_chordal,Graph.is_strongly_regular,Graph.is_eulerian, Graph.is_triangle_free, Graph.is_distance_regular, Graph.is_perfect, Graph.is_planar]

#the properties list used in the conjecturing program will be the on from gt.sage

property_of_interest = properties.index(Graph.is_hamiltonian)

theorem1 = lambda g: g.is_bipartite() and g.is_strongly_regular()

theorems = [Graph.is_cycle, Graph.is_clique, theorem1]

conjs = propertyBasedConjecture(current_graph_objects, properties, property_of_interest, theory = theorems)
for c in conjs:
    print c

((is_three_connected)&(is_planar))->(is_hamiltonian) ((is_perfect)&(is_distance_regular))->(is_hamiltonian) ((is_line_graph)^(is_chordal))->(is_hamiltonian)

tutte = graphs.TutteGraph()
tutte.show()
is_three_connected(tutte)

True

#Run 2 of Day 4
#add Tutte graph which is a CE to: (is_three_connected)&(is_planar))->(is_hamiltonian)
current_graph_objects = [k3,pete,c5,k5_5,k3_4,EH,c7_chord,bow_tie,k5,p3,glasses,fish,c5_tail,triangle_with_tail]
current_graph_objects.append(blanusa2)
current_graph_objects.append(frucht)
current_graph_objects.append(heawood)
current_graph_objects.append(duplex)
current_graph_objects.append(nb1)
current_graph_objects.append(tutte)

#properties = [Graph.is_hamiltonian, Graph.is_clique, Graph.is_regular,Graph.is_cycle,Graph.is_bipartite,Graph.is_chordal,Graph.is_strongly_regular,Graph.is_eulerian, Graph.is_triangle_free, Graph.is_distance_regular, Graph.is_perfect, Graph.is_planar]

#the properties list used in the conjecturing program will be the on from gt.sage

property_of_interest = properties.index(Graph.is_hamiltonian)

theorem1 = lambda g: g.is_bipartite() and g.is_strongly_regular()

theorems = [Graph.is_cycle, Graph.is_clique, theorem1]

conjs = propertyBasedConjecture(current_graph_objects, properties, property_of_interest, theory = theorems)
for c in conjs:
    print c

((has_paw)&(is_three_connected))->(is_hamiltonian) ((is_perfect)&(is_distance_regular))->(is_hamiltonian) ((is_line_graph)^(is_chordal))->(is_hamiltonian)

paw.show()

#Run 3 of Day 4
#a1st run of necessary conditions for hamiltonicity
current_graph_objects = [k3,pete,c5,k5_5,k3_4,EH,c7_chord,bow_tie,k5,p3,glasses,fish,c5_tail,triangle_with_tail]
current_graph_objects.append(blanusa2)
current_graph_objects.append(frucht)
current_graph_objects.append(heawood)
current_graph_objects.append(duplex)
current_graph_objects.append(nb1)
current_graph_objects.append(tutte)

#properties = [Graph.is_hamiltonian, Graph.is_clique, Graph.is_regular,Graph.is_cycle,Graph.is_bipartite,Graph.is_chordal,Graph.is_strongly_regular,Graph.is_eulerian, Graph.is_triangle_free, Graph.is_distance_regular, Graph.is_perfect, Graph.is_planar]

#the properties list used in the conjecturing program will be the on from gt.sage

property_of_interest = properties.index(Graph.is_hamiltonian)

theorems = []
#we're started with no knowledge of necessary conditions for hamiltonicity

conjs = propertyBasedConjecture(current_graph_objects, properties, property_of_interest, theory = theorems, sufficient=False)
for c in conjs:
    print c

(is_hamiltonian)->(matching_covered) (is_hamiltonian)->(is_van_den_heuvel) (is_hamiltonian)->(is_anti_tutte) (is_hamiltonian)->((is_distance_regular)|(is_planar))

for g in current_graph_objects:
    print g
    print matching_covered(g)
    g.show()

Complete graph True

Petersen graph True

Cycle graph True

Complete bipartite graph True

Complete bipartite graph True

Ellingham-Horton 54-graph True

Cycle graph True

Graph on 5 vertices True

Complete graph True

Path graph True

Graph on 7 vertices True

Graph on 6 vertices False

Cycle graph False

Complete graph False

Blanusa Second Snark Graph True

Frucht graph True

Heawood graph True

Graph on 10 vertices False

Graph on 6 vertices False

Tutte Graph True

#NOTE: we proved something by accident by mis-interpreting the 1st conjecture:
#hamiltonian -> removing any edge does not change the matching number
#CLAIM: c6 with a chord that creates a triangle is a CE to: (is_hamiltonian)->(matching_covered)
#Lovasz-Plummer Matching Theory defines a graph to matching covered if every edge is in a perfect matching
#(so a graph that's of odd order can't be matching-covered)
#matching-critical = a graph is matching critical if removing any edge changes the matching number
#not_matching_critical = a graph is *not* matching critical if removing *some* edge leaves the matching number the same
#matching_robust = a graph is matching robust if removing any edge leaves the matching number the same
#WE PROVED: hamiltonian -> matching_robust

#UPDATE: what the program thought *IS* true
#we just yo get our vocabulary straight

#NOTE: (is_hamiltonian)->(is_van_den_heuvel) is a known theorem, we'll add that too

#TO FIX: gt.sage's matching_covered definition
matching_robust = lambda g: matching_covered(g)

c6_chord = graphs.CycleGraph(6)
c6_chord.add_edge(0,2)
matching_covered(c6_chord)

True

c6_chord.show()

#Run 4 of Day 4
# run of necessary conditions for hamiltonicity
#add theorem about matching robustness

#UPDATE: what the program thought *IS* true
#we just yo get our vocabulary straight

#NOTE: (is_hamiltonian)->(is_van_den_heuvel) is a known theorem, we'll add that too

#TO FIX: gt.sage's matching_covered definition
matching_robust = lambda g: matching_covered(g)

current_graph_objects = [k3,pete,c5,k5_5,k3_4,EH,c7_chord,bow_tie,k5,p3,glasses,fish,c5_tail,triangle_with_tail]
current_graph_objects.append(blanusa2)
current_graph_objects.append(frucht)
current_graph_objects.append(heawood)
current_graph_objects.append(duplex)
current_graph_objects.append(nb1)
current_graph_objects.append(tutte)

#properties = [Graph.is_hamiltonian, Graph.is_clique, Graph.is_regular,Graph.is_cycle,Graph.is_bipartite,Graph.is_chordal,Graph.is_strongly_regular,Graph.is_eulerian, Graph.is_triangle_free, Graph.is_distance_regular, Graph.is_perfect, Graph.is_planar]

#the properties list used in the conjecturing program will be the on from gt.sage

property_of_interest = properties.index(Graph.is_hamiltonian)

matching_robust = lambda g: matching_covered(g)
theorems = [matching_robust, is_van_den_heuvel]
#we're started with no knowledge of necessary conditions for hamiltonicity

conjs = propertyBasedConjecture(current_graph_objects, properties, property_of_interest, theory = theorems, sufficient=False)
for c in conjs:
    print c

(is_hamiltonian)->((is_perfect)->(has_radius_equal_diameter)) (is_hamiltonian)->((is_independence_irreducible)|(is_distance_regular)) (is_hamiltonian)->((is_perfect)|(is_planar)) (is_hamiltonian)->((is_triangle_free)->(is_distance_regular))

Graph.is_weakly_