CoCalc -- Day6.sagews

Project: GBP-Hamiltonicity-2018

Views: ¹¹⁵

#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()
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)

5

gould.show()

is_van_den_heuvel(gould)

True

matching_robust(gould)

True

is_class1(gould)

True


#Run 3 of Day 5 RERUN
#add the theorem

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)

hoffman = graphs.HoffmanGraph()
current_graph_objects.append(hoffman)
robertson = graphs.RobertsonGraph()
current_graph_objects.append(robertson)

current_graph_objects.append(folkman)
current_graph_objects.append(house)
current_graph_objects.append(subdivided_k5)

#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]
#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_regular)->(is_planar))->(is_anti_tutte2))
(is_hamiltonian)->((~(is_independence_irreducible))^(is_anti_tutte2))
(is_hamiltonian)->((is_cubic)->(is_heliotropic_plant))

#Run1 on Day6, necessary conditions
#adding gould graph from gt.sage

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)
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)

#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]
#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)->(is_chvatal_erdos))
(is_hamiltonian)->((is_claw_free)|(is_three_connected))
(is_hamiltonian)->((is_cubic)->(is_anti_tutte))
(is_hamiltonian)->((has_perfect_matching)->(has_lovasz_theta_equals_cc))

Graph.is_weakly_chordal?

File: /ext/sage/sage-8.1/src/sage/graphs/weakly_chordal.pyx
Signature : Graph.is_weakly_chordal(g, certificate=False)
Docstring :
Tests whether the given graph is weakly chordal, i.e., the graph
and its complement have no induced cycle of length at least 5.

INPUT:

* "certificate" -- Boolean value (default: "False") whether to
  return a certificate. If "certificate = False", return "True" or
  "False" according to the graph. If "certificate = True", return

  * "(False, forbidden_subgraph)" when the graph contains a
    forbidden subgraph H, this graph is returned.

  * "(True, [])" when the graph is weakly chordal.

       For this case, it is not known how to provide a certificate.

ALGORITHM:

This algorithm checks whether the graph "g" or its complement
contain an induced cycle of length at least 5.

Using is_long_hole_free() and is_long_antihole_free() yields a run
time of O(m^2) (where m is the number of edges of the graph).

EXAMPLES:

The Petersen Graph is not weakly chordal and contains a hole:

   sage: g = graphs.PetersenGraph()
   sage: r,s = g.is_weakly_chordal(certificate = True)
   sage: r
   False
   sage: l = len(s.vertices())
   sage: s.is_isomorphic( graphs.CycleGraph(l) )
   True

conjs[1]

(is_hamiltonian)->((is_claw_free)|(is_three_connected))

g=graphs.Grid2dGraph(2,3)
g.show()

#run 2 of Day 6, necessary conditions
#2x3 grid graph is a CE to: (is_hamiltonian)->((is_claw_free)|(is_three_connected)

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)
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)

#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]
#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)->((has_perfect_matching)->(has_lovasz_theta_equals_cc))
(is_hamiltonian)->((has_kite)^(is_van_den_heuvel))
(is_hamiltonian)->((is_cubic)->(is_anti_tutte))
(is_hamiltonian)->((has_paw)->(is_heliotropic_plant))

is_ore(gould)

False

#Run3 of Day 6
#Return to Sufficient Condition Conjectures
#using all graph objects so far
#using ore and dirac theorems

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)

property_of_interest = properties.index(Graph.is_hamiltonian)

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

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

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

(is_cartesian_product)->(is_hamiltonian)
((has_paw)&(is_three_connected))->(is_hamiltonian)
((is_distance_regular)&(is_bipartite))->(is_hamiltonian)
(is_chvatal_erdos)->(is_hamiltonian)
((is_gallai_tree)^(is_chordal))->(is_hamiltonian)
((is_three_connected)&(is_eulerian))->(is_hamiltonian)

grid_3_3_3 = graphs.GridGraph([3,3,3])
grid_3_3_3.show()
grid_3_3_3.is_hamiltonian()

False

#Run 4 of Day 6
#Return to Sufficient Condition Conjectures
#using all graph objects so far
#adding erdos_chvatal theorem
#sarah notes 3-3-3-cube is a cartyesian product that is not 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)

property_of_interest = properties.index(Graph.is_hamiltonian)

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

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

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

((is_three_connected)&(is_eulerian))->(is_hamiltonian)
((has_paw)&(is_three_connected))->(is_hamiltonian)
((is_cartesian_product)&(is_planar))->(is_hamiltonian)
((is_distance_regular)&(is_bipartite))->(is_hamiltonian)
((is_gallai_tree)^(is_chordal))->(is_hamiltonian)
((is_ore)|(is_overfull))->(is_hamiltonian)

grid_3_3 = graphs.Grid2dGraph(3,3)
grid_3_3.show()
grid_3_3.is_hamiltonian()

False

#Run 5 of Day 6
#Return to Sufficient Condition Conjectures
#using all graph objects so far
#sarah & neal note 3X3 grid is a cartyesian product that is not 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)

property_of_interest = properties.index(Graph.is_hamiltonian)

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

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

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

((is_three_connected)&(is_eulerian))->(is_hamiltonian)
((has_paw)&(is_three_connected))->(is_hamiltonian)
((is_cartesian_product)&(is_circular_planar))->(is_hamiltonian)
((is_distance_regular)&(is_bipartite))->(is_hamiltonian)
((is_gallai_tree)^(is_chordal))->(is_hamiltonian)
((is_ore)|(is_overfull))->(is_hamiltonian)

tutte.is_eulerian()

False

Graph.is_gallai_tree??

   File: /ext/sage/sage-8.1/local/lib/python2.7/site-packages/sage/graphs/generic_graph.py
   Source:
       def is_gallai_tree(self):
        r"""
        Returns whether the current graph is a Gallai tree.

        A graph is a Gallai tree if and only if it is
        connected and its `2`-connected components are all
        isomorphic to complete graphs or odd cycles.

        A connected graph is not degree-choosable if and
        only if it is a Gallai tree [erdos1978choos]_.

        REFERENCES:

        .. [erdos1978choos] Erdos, P. and Rubin, A.L. and Taylor, H.
          Proc. West Coast Conf. on Combinatorics
          Graph Theory and Computing, Congressus Numerantium
          vol 26, pages 125--157, 1979

        EXAMPLES:

        A complete graph is, or course, a Gallai Tree::

            sage: g = graphs.CompleteGraph(15)
            sage: g.is_gallai_tree()
            True

        The Petersen Graph is not::

            sage: g = graphs.PetersenGraph()
            sage: g.is_gallai_tree()
            False

        A Graph built from vertex-disjoint complete graphs
        linked by one edge to a special vertex `-1` is a
        ''star-shaped'' Gallai tree ::

            sage: g = 8 * graphs.CompleteGraph(6)
            sage: g.add_edges([(-1,c[0]) for c in g.connected_components()])
            sage: g.is_gallai_tree()
            True
        """
        self._scream_if_not_simple()
        if not self.is_connected():
            return False

        for c in self.blocks_and_cut_vertices()[0]:
            gg = self.subgraph(c)
            #                    is it an odd cycle ?              a complete graph ?
            if not ( (len(c)%2 == 1 and gg.size() == len(c)+1) or gg.is_clique() ):
                return False

        return True

c7_chord.is_gallai_tree()

True

c5_tail.show()

c5_tail.blocks_and_cut_vertices()

([[0, 1, 2, 3, 4], [0, 5]], [0])

k2.is_clique()

True

glasses.is_circular_planar()

True

Graph.is_circular_planar?

File: /ext/sage/sage-8.1/local/lib/python2.7/site-packages/sage/graphs/generic_graph.py
Signature : Graph.is_circular_planar(self, on_embedding=None, kuratowski=False, set_embedding=True, boundary=None, ordered=False, set_pos=False)
Docstring :
Tests whether the graph is circular planar (outerplanar)

A graph is circular planar if it has a planar embedding in which
all vertices can be drawn in order on a circle. This method can
also be used to check the existence of a planar embedding in which
the vertices of a specific set (the *boundary*) can be drawn on a
circle, all other vertices being drawn inside of the circle. An
order can be defined on the vertices of the boundary in order to
define how they are to appear on the circle.

INPUT:

* "kuratowski" (boolean) - if set to True, returns a tuple with
  boolean first entry and the Kuratowski subgraph (i.e. an edge
  subdivision of K_5 or K_{3,3}) as the second entry (see OUTPUT
  below). It is set to "False" by default.

* "on_embedding" (boolean) - the embedding dictionary to test
  planarity on. (i.e.: will return "True" or "False" only for the
  given embedding). It is set to "False" by default.

* "set_embedding" (boolean) - whether or not to set the instance
  field variable that contains a combinatorial embedding (clockwise
  ordering of neighbors at each vertex). This value will only be
  set if a circular planar embedding is found. It is stored as a
  Python dict: "v1: [n1,n2,n3]" where "v1" is a vertex and
  "n1,n2,n3" are its neighbors. It is set to "True" by default.

* "boundary" - a set of vertices that are required to be drawn on
  the circle, all others being drawn inside of it. It is set to
  "None" by default, meaning that *all* vertices should be drawn on
  the boundary.

* "ordered" (boolean) - whether or not to consider the order of
  the boundary. It is set to "False" by default, and required
  "boundary" to be defined.

* "set_pos" - whether or not to set the position dictionary (for
  plotting) to reflect the combinatorial embedding.  Note that this
  value will default to False if set_emb is set to False. Also, the
  position dictionary will only be updated if a circular planar
  embedding is found.

OUTPUT:

The method returns "True" if the graph is circular planar, and
"False" if it is not.

If "kuratowski" is set to "True", then this function will return a
tuple, whose first entry is a boolean and whose second entry is the
Kuratowski subgraph (i.e. an edge subdivision of K_5 or K_{3,3})
isolated by the Boyer-Myrvold algorithm. Note that this graph might
contain a vertex or edges that were not in the initial graph. These
would be elements referred to below as parts of the wheel and the
star, which were added to the graph to require that the boundary
can be drawn on the boundary of a disc, with all other vertices
drawn inside (and no edge crossings).

ALGORITHM:

This is a linear time algorithm to test for circular planarity. It
relies on the edge-addition planarity algorithm due to Boyer-
Myrvold. We accomplish linear time for circular planarity by
modifying the graph before running the general planarity algorithm.

REFERENCE:

[BM04] John M. Boyer and Wendy J. Myrvold, On the Cutting
       Edge: Simplified O(n) Planarity by Edge Addition. Journal of
       Graph Algorithms and Applications, Vol. 8, No. 3, pp.
       241-273, 2004.

EXAMPLES:

   sage: g439 = Graph({1:[5,7], 2:[5,6], 3:[6,7], 4:[5,6,7]})
   sage: g439.show()
   sage: g439.is_circular_planar(boundary = [1,2,3,4])
   False
   sage: g439.is_circular_planar(kuratowski=True, boundary = [1,2,3,4])
   (False, Graph on 8 vertices)
   sage: g439.is_circular_planar(kuratowski=True, boundary = [1,2,3])
   (True, None)
   sage: g439.get_embedding()
   {1: [7, 5],
   2: [5, 6],
   3: [6, 7],
   4: [7, 6, 5],
   5: [1, 4, 2],
   6: [2, 4, 3],
   7: [3, 4, 1]}

Order matters:

   sage: K23 = graphs.CompleteBipartiteGraph(2,3)
   sage: K23.is_circular_planar(boundary = [0,1,2,3])
   True
   sage: K23.is_circular_planar(ordered=True, boundary = [0,1,2,3])
   False

With a different order:

   sage: K23.is_circular_planar(set_embedding=True, boundary = [0,2,1,3])
   True

#is_hamiltonian)->((is_weakly_chordal)->(is_chvatal_erdos))
pyramid.is_hamiltonian()
pyramid.is_weakly_chordal()
is_chvatal_erdos(pyramid)
independence_number(pyramid)
vertex_con(pyramid)
pyramid.show()

True
True
False
3
2

##run 6 of Day 6, necessary conditions
#pyramid graph is a (is_hamiltonian)->((is_weakly_chordal)->(is_chvatal_erdos))

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(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]
#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)->((has_perfect_matching)->(has_lovasz_theta_equals_cc))
(is_hamiltonian)->((has_kite)^(is_van_den_heuvel))
(is_hamiltonian)->((is_cubic)->(is_anti_tutte))
(is_hamiltonian)->((has_paw)->(is_heliotropic_plant))

#problem in is_gallai_tree
"""
 self._scream_if_not_simple()
        if not self.is_connected():
            return False

        for c in self.blocks_and_cut_vertices()[0]:
            gg = self.subgraph(c)
            #                    is it an odd cycle ?              a complete graph ?
            if not ( (len(c)%2 == 1 and gg.size() == len(c)+1) or gg.is_clique() ):
                return False
        return True
"""
def is_gallai_tree(g):
    g._scream_if_not_simple()
    if not g.is_connected():
        return False

    for c in g.blocks_and_cut_vertices()[0]:
        gg = g.subgraph(c)
        #                    is it an odd cycle ?              a complete graph ?
        if not ( (len(c)%2 == 1 and gg.size() == len(c)) or gg.is_clique() ):
            return False
    return True

def is_gallai_tree(g):
    g._scream_if_not_simple()
    if not g.is_connected():
        return False

    for c in g.blocks_and_cut_vertices()[0]:
        gg = g.subgraph(c)
        #                    is it an odd cycle ?              a complete graph ?
        if not ( (len(c)%2 == 1 and gg.size() == len(c)) or gg.is_clique() ):
            return False
    return True

pet

Graph.is_w

#Run 7 of Day 6
#Return to Sufficient Condition Conjectures
#using all graph objects so far
#sarah notes K_4_6 is not hamiltonian, but is 3-connected, eulerian, so a CE to eulerian, 3-connected => 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)

property_of_interest = properties.index(Graph.is_hamiltonian)

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

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

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_cartesian_product)&(is_circular_planar))->(is_hamiltonian)
((is_distance_regular)&(is_bipartite))->(is_hamiltonian)
((is_gallai_tree)^(is_chordal))->(is_hamiltonian)
((is_ore)|(is_overfull))->(is_hamiltonian)
((~(is_weakly_chordal))&(is_eulerian))->(is_hamiltonian)

for g in graph_objects:
    if g.is_overfull() and not g.is_hamiltonian():
        print g
        g.show()

throwing

non_ham_over

binary_octahedron

for g in current_graph_objects:
    print g, is_ore(g), g.is_overfull(), g.is_hamiltonian()

Complete graph True True True
Petersen graph False False False
Cycle graph False True True
Complete bipartite graph True False True
Complete bipartite graph False False False
Ellingham-Horton 54-graph False False False
Cycle graph False False True
Graph on 5 vertices False False False
Complete graph True True True
Path graph False False False
Graph on 7 vertices False False False
Graph on 6 vertices False False False
Cycle graph False False False
Complete graph False False False
Blanusa Second Snark Graph False False False
Frucht graph False False True
Heawood graph False False True
Graph on 10 vertices False False False
Graph on 6 vertices False False False
Tutte Graph False False False
Hoffman Graph False False True
Robertson Graph False True True
Folkman Graph False False True
House Graph False False True
Complete graph True False True
gould False False False
2D Grid Graph for [2, 3] False False True
Grid Graph for [3, 3, 3] False False False
2D Grid Graph for [3, 3] False False False
Complete bipartite graph False False False

k3_4_edge=graphs.CompleteBipartiteGraph(3,4)
k3_4_edge.add_edge(0,1)
k3_4_edge.show()

p3.is_cartesian_product()

False

#Run 8 of Day 6
#Return to Sufficient Condition Conjectures
#using all graph objects so far
#sarah notes k_3_3 edge has an induced paw, 3-connected but not hamiltonian
#add k_3_3_edge

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)
                             
property_of_interest = properties.index(Graph.is_hamiltonian)

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

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

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

((is_heliotropic_plant)&(is_regular))->(is_hamiltonian)
((is_cartesian_product)&(is_circular_planar))->(is_hamiltonian)
((~(is_weakly_chordal))&(is_eulerian))->(is_hamiltonian)
((is_gallai_tree)^(is_chordal))->(is_hamiltonian)
((is_ore)|(is_overfull))->(is_hamiltonian)

#an outerplanar cartesian product is a 2Xsomething grid graph and this outerplanar
#Proposition: cartesian product & outerplanar implies hamiltonian
#Sarah's proof generalizes to: K_2_3-minor-free & outerplanar implies hamiltonian
#uses characterization of outerplanar: K_2_3-minor-free and K_4-minor-free implies hamiltonian
#add to theorems!

#vinay has a CE to: (is_heliotropic_plant)&(is_regular))->(is_hamiltonian)
#sent a g6 string