CoCalc -- Day8.sagews

Project: GBP-Hamiltonicity-2018

Views: ¹⁰⁷

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()
nb1 = Graph("Edj_")
tutte = graphs.TutteGraph()
pete = graphs.PetersenGraph()

robertson = graphs.RobertsonGraph()
hoffman = graphs.HoffmanGraph()
folkman = graphs.FolkmanGraph()
house = graphs.HouseGraph()

subdivided_k5 = graphs.CompleteGraph(5)
subdivided_k5.subdivide_edge((0,1),1)
subdivided_k5.show()
subdivided_k5.chromatic_index()

grid_2_3=graphs.Grid2dGraph(2,3)
grid_3_3=graphs.Grid2dGraph(3,3)
grid_3_3_3 = graphs.GridGraph([3,3,3])
k_4_6 = graphs.CompleteBipartiteGraph(4,6)
k3_4_edge=graphs.CompleteBipartiteGraph(3,4)
k3_4_edge.add_edge(0,1)

c5_chord_tail = graphs.CycleGraph(5)
c5_chord_tail.add_edge(0,2)
c5_chord_tail.add_vertex()
c5_chord_tail.add_edge(1,5)

ham1 = Graph("I~EGYCxyG")
ham2 = Graph("IjCKY{Tvg")
ham3 = Graph("Shk{\LP[mZnPDR^LaE{qz?GCIhgCcmL?C")

c8_chorded = graphs.CycleGraph(8)
c8_chorded.add_edge(0,3)
c8_chorded.add_edge(4,7)

5
5

load("conjecturing.py")
load("gt.sage")

loaded utilities
loaded invariants
loaded properties
loaded theorems
loaded graphs

Remember to load DIMACS and Sloane graphs if you want them

#Run 1 of Day 8
#Return to Sufficient Condition Conjectures
#using all graph objects so far
#the graph "throwing" from gt.sage is a CE to: ore or overhull -> hamiltonian
#add theorem: cartesian product & outerplanr 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)
current_graph_objects.append(nb1)
current_graph_objects.append(tutte)
current_graph_objects.append(hoffman)
current_graph_objects.append(robertson)
current_graph_objects.append(folkman)
current_graph_objects.append(house)
current_graph_objects.append(subdivided_k5)
current_graph_objects.append(gould)
current_graph_objects.append(grid_2_3)
current_graph_objects.append(grid_3_3_3)
current_graph_objects.append(grid_3_3)
current_graph_objects.append(k_4_6)
current_graph_objects.append(k3_4_edge)
current_graph_objects.append(throwing)
current_graph_objects.append(graphs.FosterGraph())
current_graph_objects.append(graphs.DesarguesGraph())
current_graph_objects.append(graphs.Tutte12Cage())
current_graph_objects.append(graphs.BiggsSmithGraph())
current_graph_objects.append(graphs.TutteCoxeterGraph())
current_graph_objects.append(k4)
current_graph_objects.append(graphs.CompleteBipartiteGraph(3,3))
current_graph_objects.append(graphs.PappusGraph())
current_graph_objects.append(graphs.CoxeterGraph())
current_graph_objects.append(graphs.DodecahedralGraph())

property_of_interest = properties.index(Graph.is_hamiltonian)

theorem_s1 = lambda g: g.is_bipartite() and g.is_strongly_regular()
theorem_s2 = lambda g: g.is_circular_planar() and g.is_bipartite()

theorems = [Graph.is_cycle, Graph.is_clique, theorem_s1, is_ore, is_dirac, is_chvatal_erdos, theorem_s2]

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

is_deg

#NOTE to self: precoded necessary conditions: is_two_connected

#Run 1 of Day 8 rerun with throwing graph, CE from yesterday
#Return to Sufficient Condition Conjectures
#using all graph objects so far
#adding some pre-coded known sufficient conditions: is_haggkvist_nicoghossian, is_fan, is_planar_transitive, is_generalized_dirac, is_lindquester

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)
current_graph_objects.append(hoffman)
current_graph_objects.append(robertson)
current_graph_objects.append(folkman)
current_graph_objects.append(house)
current_graph_objects.append(subdivided_k5)
current_graph_objects.append(gould)
current_graph_objects.append(grid_2_3)
current_graph_objects.append(grid_3_3_3)
current_graph_objects.append(grid_3_3)
current_graph_objects.append(k_4_6)
current_graph_objects.append(k3_4_edge)
current_graph_objects.append(throwing)

current_graph_objects.append(graphs.FosterGraph())
current_graph_objects.append(graphs.DesarguesGraph())
current_graph_objects.append(graphs.Tutte12Cage())
current_graph_objects.append(graphs.BiggsSmithGraph())
current_graph_objects.append(graphs.TutteCoxeterGraph())
current_graph_objects.append(k4)
current_graph_objects.append(graphs.CompleteBipartiteGraph(3,3))
current_graph_objects.append(graphs.PappusGraph())
current_graph_objects.append(graphs.CoxeterGraph())
current_graph_objects.append(graphs.DodecahedralGraph())

property_of_interest = properties.index(Graph.is_hamiltonian)

theorem_s1 = lambda g: g.is_bipartite() and g.is_strongly_regular()
theorem_s2 = lambda g: g.is_circular_planar() and g.is_bipartite()

theorems = [Graph.is_cycle, Graph.is_clique, theorem_s1, is_ore, is_dirac, is_chvatal_erdos, theorem_s2]

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

#Run 1 of Day 8 rerun with throwing graph, CE from yesterday
#Return to Sufficient Condition Conjectures
#using all graph objects so far
#adding some pre-coded known sufficient conditions: is_haggkvist_nicoghossian, is_fan, is_planar_transitive, is_generalized_dirac, is_lindquester

current_graph_objects = [k3,pete,c5,k5_5,k3_4,EH,c7_chord,bow_tie,k5,p3,glasses,fish,c5_tail,triangle_with_tail, is_haggkvist_nicoghossian, is_fan, is_planar_transitive, is_generalized_dirac, is_lindquester]

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)
current_graph_objects.append(hoffman)
current_graph_objects.append(robertson)
current_graph_objects.append(folkman)
current_graph_objects.append(house)
current_graph_objects.append(subdivided_k5)
current_graph_objects.append(gould)
current_graph_objects.append(grid_2_3)
current_graph_objects.append(grid_3_3_3)
current_graph_objects.append(grid_3_3)
current_graph_objects.append(k_4_6)
current_graph_objects.append(k3_4_edge)
current_graph_objects.append(throwing)
"""
current_graph_objects.append(graphs.FosterGraph())
current_graph_objects.append(graphs.DesarguesGraph())
current_graph_objects.append(graphs.Tutte12Cage())
current_graph_objects.append(graphs.BiggsSmithGraph())
current_graph_objects.append(graphs.TutteCoxeterGraph())
current_graph_objects.append(k4)
current_graph_objects.append(graphs.CompleteBipartiteGraph(3,3))
current_graph_objects.append(graphs.PappusGraph())
current_graph_objects.append(graphs.CoxeterGraph())
current_graph_objects.append(graphs.DodecahedralGraph())
"""
property_of_interest = properties.index(Graph.is_hamiltonian)

theorem_s1 = lambda g: g.is_bipartite() and g.is_strongly_regular()
theorem_s2 = lambda g: g.is_circular_planar() and g.is_bipartite()

theorems = [Graph.is_cycle, Graph.is_clique, theorem_s1, is_ore, is_dirac, is_chvatal_erdos, theorem_s2]

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

'\ncurrent_graph_objects.append(graphs.FosterGraph())\ncurrent_graph_objects.append(graphs.DesarguesGraph())\ncurrent_graph_objects.append(graphs.Tutte12Cage())\ncurrent_graph_objects.append(graphs.BiggsSmithGraph())\ncurrent_graph_objects.append(graphs.TutteCoxeterGraph())\ncurrent_graph_objects.append(k4)\ncurrent_graph_objects.append(graphs.CompleteBipartiteGraph(3,3))\ncurrent_graph_objects.append(graphs.PappusGraph())\ncurrent_graph_objects.append(graphs.CoxeterGraph())\ncurrent_graph_objects.append(graphs.DodecahedralGraph())\n'

c5_chord_tail = graphs.CycleGraph(5)
c5_chord_tail.add_edge(0,2)
c5_chord_tail.add_vertex()
c5_chord_tail.add_edge(1,5)
c5_chord_tail.show()

5

#Run 2 of Day 8 
#found CE to claw-free XOR chordal implies hamiltonian: c5 with chord and appended vertex
#Return to Sufficient Condition Conjectures
#using all graph objects so far
#adding some pre-coded known sufficient conditions: is_haggkvist_nicoghossian, is_fan, is_planar_transitive, is_generalized_dirac, is_lindquester

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)
current_graph_objects.append(hoffman)
current_graph_objects.append(robertson)
current_graph_objects.append(folkman)
current_graph_objects.append(house)
current_graph_objects.append(subdivided_k5)
current_graph_objects.append(gould)
current_graph_objects.append(grid_2_3)
current_graph_objects.append(grid_3_3_3)
current_graph_objects.append(grid_3_3)
current_graph_objects.append(k_4_6)
current_graph_objects.append(k3_4_edge)
current_graph_objects.append(throwing)
current_graph_objects.append(c5_chord_tail)

#current_graph_objects.append(graphs.FosterGraph())
#order = 90
current_graph_objects.append(graphs.DesarguesGraph())
#current_graph_objects.append(graphs.Tutte12Cage())
#order = 126
#current_graph_objects.append(graphs.BiggsSmithGraph())
#order = 102
current_graph_objects.append(graphs.TutteCoxeterGraph())
current_graph_objects.append(k4)
current_graph_objects.append(graphs.CompleteBipartiteGraph(3,3))
current_graph_objects.append(graphs.PappusGraph())
current_graph_objects.append(graphs.CoxeterGraph())
current_graph_objects.append(graphs.DodecahedralGraph())

property_of_interest = properties.index(Graph.is_hamiltonian)

theorem_s1 = lambda g: g.is_bipartite() and g.is_strongly_regular()
theorem_s2 = lambda g: g.is_circular_planar() and g.is_bipartite()

theorems = [Graph.is_cycle, Graph.is_clique, theorem_s1, is_ore, is_dirac, is_chvatal_erdos, theorem_s2]
#add is_haggkvist_nicoghossian, is_fan, is_planar_transitive, is_generalized_dirac, is_lindquester

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

L = [thm(g) for thm in theorems]
all(L)
not any(L)

False
True

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)
current_graph_objects.append(hoffman)
current_graph_objects.append(robertson)
current_graph_objects.append(folkman)
current_graph_objects.append(house)
current_graph_objects.append(subdivided_k5)
current_graph_objects.append(gould)
current_graph_objects.append(grid_2_3)
current_graph_objects.append(grid_3_3_3)
current_graph_objects.append(grid_3_3)
current_graph_objects.append(k_4_6)
current_graph_objects.append(k3_4_edge)
current_graph_objects.append(throwing)
current_graph_objects.append(c5_chord_tail)

#current_graph_objects.append(graphs.FosterGraph())
#order = 90
current_graph_objects.append(graphs.DesarguesGraph())
#current_graph_objects.append(graphs.Tutte12Cage())
#order = 126
#current_graph_objects.append(graphs.BiggsSmithGraph())
#order = 102
current_graph_objects.append(graphs.TutteCoxeterGraph())
current_graph_objects.append(k4)
current_graph_objects.append(graphs.CompleteBipartiteGraph(3,3))
current_graph_objects.append(graphs.PappusGraph())
current_graph_objects.append(graphs.CoxeterGraph())
current_graph_objects.append(graphs.DodecahedralGraph())

for g in current_graph_objects:
    L = [thm(g) for thm in theorems]
    if all(L) and not g.is_hamiltonian():
        print g

#NEED a graph that's Hamiltoniaan but dooen't satisfy ANY current sufficient condition for hamiltonicity
#try to find a random one
def randomHam(n,p):
    G=graphs.CycleGraph(n)
    H=graphs.RandomGNP(n,p)
    return G.union(H)

while true:
    g = randomHam(20,.5)
    L = [thm(g) for thm in theorems]
    if not any(L):
        print g.graph6_string()
        break

Shk{\LP[mZnPDR^LaE{qz?GCIhgCcmL?C

g=Graph("Shk{\LP[mZnPDR^LaE{qz?GCIhgCcmL?C")
g.show()
g.is_hamiltonian()
for thm in theorems:
    print thm(g)

True
False
False
False
False
False
False
False

#Run 2 of Day 8 
#found CE to claw-free XOR chordal implies hamiltonian: c5 with chord and appended vertex
#Return to Sufficient Condition Conjectures
#using all graph objects so far
#adding some pre-coded known sufficient conditions: is_haggkvist_nicoghossian, is_fan, is_planar_transitive, is_generalized_dirac, is_lindquester

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)
current_graph_objects.append(hoffman)
current_graph_objects.append(robertson)
current_graph_objects.append(folkman)
current_graph_objects.append(house)
current_graph_objects.append(subdivided_k5)
current_graph_objects.append(gould)
current_graph_objects.append(grid_2_3)
current_graph_objects.append(grid_3_3_3)
current_graph_objects.append(grid_3_3)
current_graph_objects.append(k_4_6)
current_graph_objects.append(k3_4_edge)
current_graph_objects.append(throwing)
current_graph_objects.append(c5_chord_tail)

#current_graph_objects.append(graphs.FosterGraph())
#order = 90
current_graph_objects.append(graphs.DesarguesGraph())
#current_graph_objects.append(graphs.Tutte12Cage())
#order = 126
#current_graph_objects.append(graphs.BiggsSmithGraph())
#order = 102
current_graph_objects.append(graphs.TutteCoxeterGraph())
current_graph_objects.append(k4)
current_graph_objects.append(graphs.CompleteBipartiteGraph(3,3))
current_graph_objects.append(graphs.PappusGraph())
current_graph_objects.append(graphs.CoxeterGraph())
current_graph_objects.append(graphs.DodecahedralGraph())
current_graph_objects.append(ham1)
current_graph_objects.append(ham2)
current_graph_objects.append(ham3)

property_of_interest = properties.index(Graph.is_hamiltonian)

theorem_s1 = lambda g: g.is_bipartite() and g.is_strongly_regular()
theorem_s2 = lambda g: g.is_circular_planar() and g.is_bipartite()

theorems = [Graph.is_cycle, Graph.is_clique, theorem_s1, is_ore, is_dirac, is_chvatal_erdos, theorem_s2]
#add is_haggkvist_nicoghossian, is_fan, is_planar_transitive, is_generalized_dirac, is_lindquester

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

#NOTE: WHY aren't we getting new conjectures??!?!?!? there are now 3 graphs ham1, ham2 and ham3 which are hamiltonian but don't satisfy any sufficient condition

[]

ham1

Graph on 10 vertices

##run 3 of Day 8, necessary conditions
#pyramid graph is a CE to (is_hamiltonian)->((is_weakly_chordal)->(is_chvatal_erdos))
#adding theorems is_two_connected, alpha_leq_order_over_two

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)
current_graph_objects.append(hoffman)
current_graph_objects.append(robertson)
current_graph_objects.append(folkman)
current_graph_objects.append(house)
current_graph_objects.append(subdivided_k5)
current_graph_objects.append(gould)
current_graph_objects.append(grid_2_3)
current_graph_objects.append(grid_3_3_3)
current_graph_objects.append(grid_3_3)
current_graph_objects.append(k_4_6)
current_graph_objects.append(k3_4_edge)
current_graph_objects.append(throwing)
current_graph_objects.append(c5_chord_tail)

#current_graph_objects.append(graphs.FosterGraph())
#order = 90
current_graph_objects.append(graphs.DesarguesGraph())
#current_graph_objects.append(graphs.Tutte12Cage())
#order = 126
#current_graph_objects.append(graphs.BiggsSmithGraph())
#order = 102
current_graph_objects.append(graphs.TutteCoxeterGraph())
current_graph_objects.append(k4)
current_graph_objects.append(graphs.CompleteBipartiteGraph(3,3))
current_graph_objects.append(graphs.PappusGraph())
current_graph_objects.append(graphs.CoxeterGraph())
current_graph_objects.append(graphs.DodecahedralGraph())
current_graph_objects.append(ham1)
current_graph_objects.append(ham2)
current_graph_objects.append(ham3)

current_graph_objects.append(pyramid)

#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)
theorem_n1 = lambda g: not is_cubic(g) or is_class1(g)

theorems = [matching_robust, is_van_den_heuvel, theorem_n1, is_two_connected, alpha_leq_order_over_two]
#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_weakly_chordal)->(order_leq_twice_max_degree))
(is_hamiltonian)->(((is_regular)->(is_kite_free))&(matching_covered))
(is_hamiltonian)->(((is_regular)->(is_kite_free))&(alpha_leq_order_over_two))
(is_hamiltonian)->((is_anti_tutte)|(is_edge_transitive))
(is_hamiltonian)->(((is_regular)->(is_kite_free))&(is_van_den_heuvel))
(is_hamiltonian)->(((is_eulerian)|(is_planar))|(has_lovasz_theta_equals_cc))

#c8 with 2 chords is hamiltonian & weakly chordal but order = 8 is nor <= 2* max degree
c8_chorded = graphs.CycleGraph(8)
c8_chorded.add_edge(0,3)
c8_chorded.add_edge(4,7)
c8_chorded.show()

c8_chorded.is_weakly_chordal()
order_leq_twice_max_degree(c8_chorded)

True
False

##run 4 of Day 8, necessary conditions
#pyramid graph is a CE to (is_hamiltonian)->((is_weakly_chordal)->(is_chvatal_erdos))
#adding theorems is_two_connected, alpha_leq_order_over_two

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)
current_graph_objects.append(hoffman)
current_graph_objects.append(robertson)
current_graph_objects.append(folkman)
current_graph_objects.append(house)
current_graph_objects.append(subdivided_k5)
current_graph_objects.append(gould)
current_graph_objects.append(grid_2_3)
current_graph_objects.append(grid_3_3_3)
current_graph_objects.append(grid_3_3)
current_graph_objects.append(k_4_6)
current_graph_objects.append(k3_4_edge)
current_graph_objects.append(throwing)
current_graph_objects.append(c5_chord_tail)

#current_graph_objects.append(graphs.FosterGraph())
#order = 90
current_graph_objects.append(graphs.DesarguesGraph())
#current_graph_objects.append(graphs.Tutte12Cage())
#order = 126
#current_graph_objects.append(graphs.BiggsSmithGraph())
#order = 102
current_graph_objects.append(graphs.TutteCoxeterGraph())
current_graph_objects.append(k4)
current_graph_objects.append(graphs.CompleteBipartiteGraph(3,3))
current_graph_objects.append(graphs.PappusGraph())
current_graph_objects.append(graphs.CoxeterGraph())
current_graph_objects.append(graphs.DodecahedralGraph())
current_graph_objects.append(ham1)
current_graph_objects.append(ham2)
current_graph_objects.append(ham3)

current_graph_objects.append(pyramid)

#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)
theorem_n1 = lambda g: not is_cubic(g) or is_class1(g)

theorems = [matching_robust, is_van_den_heuvel, theorem_n1, is_two_connected, alpha_leq_order_over_two]
#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_weakly_chordal)->(order_leq_twice_max_degree))
(is_hamiltonian)->(((is_regular)->(is_kite_free))&(matching_covered))
(is_hamiltonian)->(((is_regular)->(is_kite_free))&(alpha_leq_order_over_two))
(is_hamiltonian)->((is_anti_tutte)|(is_edge_transitive))
(is_hamiltonian)->(((is_regular)->(is_kite_free))&(is_van_den_heuvel))
(is_hamiltonian)->(((is_eulerian)|(is_planar))|(has_lovasz_theta_equals_cc))


load("gt_precomputed_database.sage")
precomputed = precomputed_properties_for_conjecture()

#trying precomputed database with the same last run

(is_hamiltonian)->(((is_regular)->(is_kite_free))&(matching_covered))
(is_hamiltonian)->(((is_regular)->(is_kite_free))&(alpha_leq_order_over_two))
(is_hamiltonian)->(((is_eulerian)|(is_planar))|(has_lovasz_theta_equals_cc))
(is_hamiltonian)->((is_anti_tutte)|(is_edge_transitive))
(is_hamiltonian)->(((is_regular)->(is_kite_free))&(is_van_den_heuvel))

#Run 5 of Day 8, rerun of earlier using precomputed database 
#found CE to claw-free XOR chordal implies hamiltonian: c5 with chord and appended vertex
#Return to Sufficient Condition Conjectures
#using all graph objects so far
#adding some pre-coded known sufficient conditions: is_haggkvist_nicoghossian, is_fan, is_planar_transitive, is_generalized_dirac, is_lindquester

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)
current_graph_objects.append(hoffman)
current_graph_objects.append(robertson)
current_graph_objects.append(folkman)
current_graph_objects.append(house)
current_graph_objects.append(subdivided_k5)
current_graph_objects.append(gould)
current_graph_objects.append(grid_2_3)
current_graph_objects.append(grid_3_3_3)
current_graph_objects.append(grid_3_3)
current_graph_objects.append(k_4_6)
current_graph_objects.append(k3_4_edge)
current_graph_objects.append(throwing)
current_graph_objects.append(c5_chord_tail)

#current_graph_objects.append(graphs.FosterGraph())
#order = 90
current_graph_objects.append(graphs.DesarguesGraph())
#current_graph_objects.append(graphs.Tutte12Cage())
#order = 126
#current_graph_objects.append(graphs.BiggsSmithGraph())
#order = 102
current_graph_objects.append(graphs.TutteCoxeterGraph())
current_graph_objects.append(k4)
current_graph_objects.append(graphs.CompleteBipartiteGraph(3,3))
current_graph_objects.append(graphs.PappusGraph())
current_graph_objects.append(graphs.CoxeterGraph())
current_graph_objects.append(graphs.DodecahedralGraph())
current_graph_objects.append(ham1)
current_graph_objects.append(ham2)
current_graph_objects.append(ham3)
current_graph_objects.append(c8_chorded)

property_of_interest = properties.index(Graph.is_hamiltonian)

theorem_s1 = lambda g: g.is_bipartite() and g.is_strongly_regular()
theorem_s2 = lambda g: g.is_circular_planar() and g.is_bipartite()

theorems = [Graph.is_cycle, Graph.is_clique, theorem_s1, is_ore, is_dirac, is_chvatal_erdos, theorem_s2]
#add is_haggkvist_nicoghossian, is_fan, is_planar_transitive, is_generalized_dirac, is_lindquester

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

kite_with_tail.show()

#Run 5 of Day 8, rerun of earlier using precomputed database 
#found CE to claw-free XOR chordal implies hamiltonian: c5 with chord and appended vertex
#Return to Sufficient Condition Conjectures
#using all graph objects so far
#adding some pre-coded known sufficient conditions: is_haggkvist_nicoghossian, is_fan, is_planar_transitive, is_generalized_dirac, is_lindquester

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)
current_graph_objects.append(hoffman)
current_graph_objects.append(robertson)
current_graph_objects.append(folkman)
current_graph_objects.append(house)
current_graph_objects.append(subdivided_k5)
current_graph_objects.append(gould)
current_graph_objects.append(grid_2_3)
current_graph_objects.append(grid_3_3_3)
current_graph_objects.append(grid_3_3)
current_graph_objects.append(k_4_6)
current_graph_objects.append(k3_4_edge)
current_graph_objects.append(throwing)
current_graph_objects.append(c5_chord_tail)

#current_graph_objects.append(graphs.FosterGraph())
#order = 90
current_graph_objects.append(graphs.DesarguesGraph())
#current_graph_objects.append(graphs.Tutte12Cage())
#order = 126
#current_graph_objects.append(graphs.BiggsSmithGraph())
#order = 102
current_graph_objects.append(graphs.TutteCoxeterGraph())
current_graph_objects.append(k4)
current_graph_objects.append(graphs.CompleteBipartiteGraph(3,3))
current_graph_objects.append(graphs.PappusGraph())
current_graph_objects.append(graphs.CoxeterGraph())
current_graph_objects.append(graphs.DodecahedralGraph())
current_graph_objects.append(ham1)
current_graph_objects.append(ham2)
current_graph_objects.append(ham3)
current_graph_objects.append(c8_chorded)

property_of_interest = properties.index(Graph.is_hamiltonian)

theorem_s1 = lambda g: g.is_bipartite() and g.is_strongly_regular()
theorem_s2 = lambda g: g.is_circular_planar() and g.is_cartesian_product()

theorems = [Graph.is_cycle, Graph.is_clique, theorem_s1, is_ore, is_dirac, is_chvatal_erdos, theorem_s2]
#add is_haggkvist_nicoghossian, is_fan, is_planar_transitive, is_generalized_dirac, is_lindquester

conjs = propertyBasedConjecture(current_graph_objects, properties, property_of_interest, theory = theorems, time = 5, precomputed = precomputed, verbose=False, debug=True)
for c in conjs:
    print c

> Generation process was stopped by the conjecturing heuristic.
> Found 5 unlabeled trees.
> Found 27602 labeled trees.
> Found 2793 valid expressions.
((is_heliotropic_plant)&(is_regular))->(is_hamiltonian)
(has_dart)->(is_hamiltonian)
(is_planar_transitive)->(is_hamiltonian)
((is_distance_regular)&(is_bipartite))->(is_hamiltonian)
((is_van_den_heuvel)&(is_circular_planar))->(is_hamiltonian)
((is_claw_free)&(is_van_den_heuvel))->(is_hamiltonian)
((~(is_weakly_chordal))&(is_eulerian))->(is_hamiltonian)

for g in current_graph_objects:
    if any(thm(g) for thm in theorems) and not g.is_hamiltonian():
        print g
        g.show()

Path graph

Graph on 7 vertices

p3.is_cartesian_product()

False

count = 0
for thm in theorems:
    print count, thm(glasses)
    count += 1

False
False
False
False
False
False
True

p3.is_circular_planar()

True

#Run 6 of Day 8, rerun of earlier using precomputed database 
#Return to Sufficient Condition Conjectures
#using all graph objects so far
#adding some pre-coded known sufficient conditions: is_haggkvist_nicoghossian, is_fan, is_planar_transitive, is_generalized_dirac, is_lindquester

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)
current_graph_objects.append(hoffman)
current_graph_objects.append(robertson)
current_graph_objects.append(folkman)
current_graph_objects.append(house)
current_graph_objects.append(subdivided_k5)
current_graph_objects.append(gould)
current_graph_objects.append(grid_2_3)
current_graph_objects.append(grid_3_3_3)
current_graph_objects.append(grid_3_3)
current_graph_objects.append(k_4_6)
current_graph_objects.append(k3_4_edge)
current_graph_objects.append(throwing)
current_graph_objects.append(c5_chord_tail)

#current_graph_objects.append(graphs.FosterGraph())
#order = 90
current_graph_objects.append(graphs.DesarguesGraph())
#current_graph_objects.append(graphs.Tutte12Cage())
#order = 126
#current_graph_objects.append(graphs.BiggsSmithGraph())
#order = 102
current_graph_objects.append(graphs.TutteCoxeterGraph())
current_graph_objects.append(k4)
current_graph_objects.append(graphs.CompleteBipartiteGraph(3,3))
current_graph_objects.append(graphs.PappusGraph())
current_graph_objects.append(graphs.CoxeterGraph())
current_graph_objects.append(graphs.DodecahedralGraph())
current_graph_objects.append(ham1)
current_graph_objects.append(ham2)
current_graph_objects.append(ham3)
current_graph_objects.append(c8_chorded)

property_of_interest = properties.index(Graph.is_hamiltonian)

theorem_s1 = lambda g: g.is_bipartite() and g.is_strongly_regular()
theorem_s2 = lambda g: g.is_circular_planar() and g.is_cartesian_product()

theorems = [Graph.is_cycle, Graph.is_clique, theorem_s1, is_ore, is_dirac, is_chvatal_erdos, theorem_s2,
is_haggkvist_nicoghossian, is_fan, is_planar_transitive, is_generalized_dirac, is_lindquester]

conjs = propertyBasedConjecture(current_graph_objects, properties, property_of_interest, theory = theorems, time = 5, precomputed = precomputed, verbose=False, debug=True)
for c in conjs:
    print c

> Generation process was stopped by the conjecturing heuristic.
> Found 5 unlabeled trees.
> Found 27602 labeled trees.
> Found 2793 valid expressions.
((is_dart_free)->(is_planar_transitive))->(is_hamiltonian)
((is_heliotropic_plant)&(is_regular))->(is_hamiltonian)
((is_distance_regular)&(is_bipartite))->(is_hamiltonian)
((is_van_den_heuvel)&(is_circular_planar))->(is_hamiltonian)
((is_claw_free)&(is_van_den_heuvel))->(is_hamiltonian)
((~(is_weakly_chordal))&(is_eulerian))->(is_hamiltonian)



def kite_necklace(k):
    #returns k kites joined head to tail
    if k==1:
        return Graph('DJk')
    g = graphs.CycleGraph(2*k)
    for i in [0..k-1]:
        g.subdivide_edge((0+2*i,1+2*i),1)
        g.add_edge(0+2*i,1+2*i)
        g.subdivide_edge((0+2*i,1+2*i),1)
        g.add_edge(2*k+2*i,2*k+2*i+1)
    return g

kite_necklace_3 = kite_necklace(3)
kite_necklace_3.order()
kite_necklace_3.show()

12

conjs[4]

((is_claw_free)&(is_van_den_heuvel))->(is_hamiltonian)

conjs[4](kite_necklace_3)

True

kite_necklace_2 = kite_necklace(2)
kite_necklace_2.order()
kite_necklace_2.show()

8