SharedDay2.sagewsOpen in CoCalc
load("conjecturing.py")

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)

#Last run from Day 1
graph_objects = [k3,pete,c5,k5_5,k3_4,EH]

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]

property_of_interest = 0

conjs = propertyBasedConjecture(graph_objects, properties, property_of_interest)
for c in conjs:
print c

((is_strongly_regular)&(is_bipartite))->(is_hamiltonian) (is_cycle)->(is_hamiltonian)
EH.is_bipartite()

True
EH.is_strongly_regular()

False
EH.is_hamiltonian()

False
EH.is_regular()

True
#don't want repeated true conjectures
#we want conjectures that give us information about graphs which are not currently accounted for by our theory
#THEORY OF SUFFICIENT FOR HAMILTONICITY => cycle graphs, complete graphs, strongly regular bipartite graphs
#NOTE: current graphs are all covered by our theory
#NEED a graph that's not complete or a cycle or strongly regular bipartite
#IDEA: add c7 with a chord
c7 = graphs.CycleGraph(7)
c7_chord = graphs.CycleGraph(7)

c7_chord.show()

#ADD C7_CHORD
graph_objects = [k3,pete,c5,k5_5,k3_4,EH,c7_chord]

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]

property_of_interest = 0

conjs = propertyBasedConjecture(graph_objects, properties, property_of_interest)
for c in conjs:
print c

(is_cycle)->(is_hamiltonian) ((~(is_bipartite))^(is_strongly_regular))->(is_hamiltonian)
#Run2 of Day2 sufficient conditions for Hamiltonicity
#force the program to eliminate conjectures that we know are true
graph_objects = [k3,pete,c5,k5_5,k3_4,EH,c7_chord]

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]

property_of_interest = 0

theorems = [Graph.is_cycle]

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

(((is_bipartite)|(is_regular))->(is_cycle))->(is_hamiltonian) ((~(is_bipartite))^(is_strongly_regular))->(is_hamiltonian)
#bow tie should be a counterexample to the 12st conjecture
bow_tie = Graph(5)
bow_tie.show()

#Run3 of Day2 sufficient conditions for Hamiltonicity

graph_objects = [k3,pete,c5,k5_5,k3_4,EH,c7_chord,bow_tie]

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]

property_of_interest = 0

theorems = [Graph.is_cycle]

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

(((is_bipartite)|(is_cycle))&(is_strongly_regular))->(is_hamiltonian) (((is_bipartite)|(is_regular))^(~(is_chordal)))->(is_hamiltonian)
#Run4 of Day2 sufficient conditions for Hamiltonicity
#the path on 3 vertices p3 is a CE to the 2nd conjecture
#the 12st is true and implied by current theory
#k3 is the only included complete graph, we'll add k5 to see if the complete graph conjecture is repreated
p3 = graphs.PathGraph(3)
k5 = graphs.CompleteGraph(5)
graph_objects = [k3,pete,c5,k5_5,k3_4,EH,c7_chord,bow_tie,k5,p3]

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]

property_of_interest = 0

theorems = [Graph.is_cycle]

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

((is_strongly_regular)&(is_bipartite))->(is_hamiltonian) (((is_bipartite)|(is_regular))^(~(is_eulerian)))->(is_hamiltonian)
#Run5
#the graph "glasses" consisting of 2 c4s amalgamated at a single vertex is a CE to the 2nd conjecture
#the 1st is true and can be eliminated with theory
glasses = Graph(7)
graph_objects = [k3,pete,c5,k5_5,k3_4,EH,c7_chord,bow_tie,k5,p3,glasses]

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]

property_of_interest = 0

theorems = [Graph.is_cycle]

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

((is_cycle)|(is_clique))->(is_hamiltonian) (((is_chordal)|(is_bipartite))^(~(is_strongly_regular)))->(is_hamiltonian)
#Run6
#the 1st is true and can be eliminated with theory

graph_objects = [k3,pete,c5,k5_5,k3_4,EH,c7_chord,bow_tie,k5,p3,glasses]

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]

property_of_interest = 0

theorems = [Graph.is_cycle, Graph.is_clique]

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

(((is_strongly_regular)&(is_bipartite))|(is_clique))->(is_hamiltonian) (((is_bipartite)|(is_cycle))&(is_strongly_regular))->(is_hamiltonian) (((is_chordal)|(is_bipartite))^(~(is_strongly_regular)))->(is_hamiltonian)
#Run7
#C5 with a pendant vertex is a CE to the 3rd conjecture
c5_tail = graphs.CycleGraph(5)
c5_tail.show()

5
k5.is_apex




#Run7
#add new properties - need more properties to get simpler conjectures
graph_objects = [k3,pete,c5,k5_5,k3_4,EH,c7_chord,bow_tie,k5,p3,glasses]

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]

property_of_interest = 0

theorems = [Graph.is_cycle, Graph.is_clique]

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

(~((is_triangle_free)|(is_chordal)))->(is_hamiltonian) ((is_perfect)&(is_distance_regular))->(is_hamiltonian) (((is_bipartite)|(is_cycle))&(is_strongly_regular))->(is_hamiltonian)
#Run8
#add the "fish" k3 and c4 amalgamated at a vertex is a CE to 1st conjecture
fish = Graph([(0,1),(1,2),(2,3),(3,4),(4,5),(5,2),(2,0)])
fish.show()

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

False
theorem1(EH)

False
theorem1(k5_5)

True
#Run8
#add fish, c5_tail & theorem 1
graph_objects = [k3,pete,c5,k5_5,k3_4,EH,c7_chord,bow_tie,k5,p3,glasses,fish,c5_tail]

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]

property_of_interest = 0

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

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

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

(((is_triangle_free)|(is_eulerian))->(is_clique))->(is_hamiltonian) (((is_eulerian)->(is_bipartite))^(is_triangle_free))->(is_hamiltonian) (((is_triangle_free)|(is_eulerian))->((is_strongly_regular)&(is_bipartite)))->(is_hamiltonian)