girth-theta-conjecture-investigation.sagews

#IDEA: find lower bounds for alpha using girth-theta-conjecture as theory
#get conjectured lower bounds {n_i}
#prove alpha >= n_i for each i
#and max(n_i) >= girth-theta-bound for each i
#this gives a "conjectured proof" of alpha >= girth-theta bound

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

loaded graph dc1024 loaded graph dc2048 loaded graph properties data file loaded graph invariants data file

graph_objects = [paw, kite, p4, dart, k3, k4, k5, c6ee, c5chord, graphs.DodecahedralGraph(), c8chorded, c8chords, graphs.ClebschGraph(),  prismy, c24, c26, c60, c6xc6, holton_mckay, sixfour, c4, graphs.PetersenGraph(), p2, graphs.TutteGraph(), non_ham_over, throwing, throwing2, throwing3, kratsch_lehel_muller, graphs.BlanusaFirstSnarkGraph(), graphs.BlanusaSecondSnarkGraph(), graphs.FlowerSnark(), s3, ryan3, k10, graphs.MycielskiGraph(5), c3mycielski, s13e, ryan2, s22e, difficult11, graphs.BullGraph(), graphs.ChvatalGraph(), graphs.ClawGraph(), graphs.DesarguesGraph(), graphs.DiamondGraph(), graphs.FlowerSnark(), graphs.FruchtGraph(), graphs.HoffmanSingletonGraph(), graphs.HouseGraph(), graphs.OctahedralGraph(), graphs.ThomsenGraph(), pete , graphs.PappusGraph(), graphs.GrotzschGraph(), graphs.GrayGraph(), graphs.HeawoodGraph(), graphs.HerschelGraph(), graphs.CoxeterGraph(), graphs.BrinkmannGraph(), graphs.TutteCoxeterGraph(), graphs.TutteGraph(), graphs.RobertsonGraph(), graphs.FolkmanGraph(), graphs.Balaban10Cage(), graphs.PappusGraph(), graphs.TietzeGraph(), graphs.SylvesterGraph(), graphs.SzekeresSnarkGraph(), graphs.MoebiusKantorGraph(), ryan, inp, c4c4, regular_non_trans, bridge, p10k4, c100, starfish, c5k3, k5pendant, graphs.ShrikhandeGraph(), sylvester, fork, edge_critical_5, edge_critical_11_1, edge_critical_11_2, pete_minus, c5, bow_tie, pepper_residue_graph, barrus_graph, p5, c6, c9, ce3, ce4, ce5, k4e2split, flower_with_3_petals, flower_with_4_petals, paw_x_paw, graphs.WagnerGraph(), houseX, ce7, triangle_star, ce8, ce9, ce10, p3, binary_octahedron, ce11, prism, ce12, ce13, ce14] + alpha_critical_easy

graph_objects

#load the database of precomputed invariant values
load("objects-invariants-properties/gt_precomputed_database.sage")
db = os.environ['HOME'] +'/objects-invariants-properties/gt_precomputed_database.db'
#now get a table out of the precomputed database that can be used by the invariant-relation conjecturing program
precomputed_invs = precomputed_invariants_for_conjecture(database=db)

#note each of the folling theorems *is* either an invariant (and could be precomputed) or
#some just_defined number that's an integer
#so there's no possibility of rounding-error numerical instability

def get_value(invariant, o):
    precomputed_value = None
    o_key = precomputed_invs[1](o)
    i_key = precomputed_invs[2](invariant)
    if precomputed_invs:
        if o_key in precomputed_invs[0]:
            if i_key in precomputed_invs[0][o_key]:
                precomputed_value = precomputed_invs[0][o_key][i_key]
    if precomputed_value is None:
        return invariant(o)
    else:
        return precomputed_value

girth_theta_bound = lambda g: min(g.girth(),floor(get_value(Graph.lovasz_theta,g)))

theorems = [girth_theta_bound]
#use get_value so that conjecture program uses precomputed value in theory calculation instead of recomputing (maybe incorrectly)
####min_theorem = lambda g: floor(min(get_value(f, g) for f in theorems))
#for this to work each "theorem" that has a potential numerical error needs to be precomputed and included in the db

#there is a problem with a fiedler number computation, removing fiedler (35 in the list) from invariants
#efficiently_computable_invariants.pop(35)
invariants = [independence_number] + efficiently_computable_invariants

objects = graph_objects

#no results after the default 5 seconds
#so there could be a bug - or no significant conjecture yet - increasing the time *may* help
conjs = conjecture(objects, invariants, invariants.index(independence_number), upperBound = False, theory = theorems, precomputed = precomputed_invs, time = 100)
for c in conjs:
    print c

independence_number(x) >= average_distance(x) independence_number(x) >= radius(x) independence_number(x) >= residue(x) independence_number(x) >= max_even_minus_even_horizontal(x) independence_number(x) >= critical_independence_number(x) independence_number(x) >= max_degree(x) - number_of_triangles(x) independence_number(x) >= -average_distance(x) + ceil(lovasz_theta(x)) independence_number(x) >= min_degree(x) - number_of_triangles(x) independence_number(x) >= diameter(x)/different_degrees(x) independence_number(x) >= ceil(order(x)/brooks(x)) independence_number(x) >= minimum(max_degree(x), floor(lovasz_theta(x))) independence_number(x) >= -max_common_neighbors(x) + min_degree(x) independence_number(x) >= max_degree(x) - order_automorphism_group(x) independence_number(x) >= -card_periphery(x) + matching_number(x) independence_number(x) >= minimum(min_degree(x), floor(lovasz_theta(x))) independence_number(x) >= matching_number(x) - sigma_2(x) - 1 independence_number(x) >= matching_number(x) - order_automorphism_group(x) - 1 independence_number(x) >= -10^different_degrees(x) + matching_number(x) independence_number(x) >= card_negative_eigenvalues(x) - sigma_2(x) independence_number(x) >= floor(lovasz_theta(x))/vertex_con(x) independence_number(x) >= 2*floor(arccosh(lovasz_theta(x))) independence_number(x) >= minimum(floor(lovasz_theta(x)), tan(spanning_trees_count(x))) independence_number(x) >= floor(tan(barrus_bound(x) - 1)) independence_number(x) >= floor(arccosh(lovasz_theta(x)))^2 independence_number(x) >= minimum(card_positive_eigenvalues(x), 2*card_zero_eigenvalues(x)) independence_number(x) >= barrus_bound(x) - maximum(card_center(x), card_positive_eigenvalues(x)) independence_number(x) >= -1/2*diameter(x) + lovasz_theta(x) independence_number(x) >= floor(tan(floor(gutman_energy(x)))) independence_number(x) >= minimum(floor(lovasz_theta(x)), max_even_minus_even_horizontal(x) + 1)

count = 0
for g in graph_objects:
    x = independence_number(g)
    y = girth_theta_bound(g)

    if x > y:
        print count, x, y, g.name()
        count += 1

0 8 5 Dodecahedron 1 5 4 Clebsch graph 2 9 5 c24 3 11 5 c26 4 24 5 c60 5 18 4 c6xc6 6 10 4 holton_mckay 7 4 3 sixfour 8 19 4 Tutte Graph 9 4 3 non_ham_over 10 4 3 throwing 11 4 3 throwing2 12 4 3 throwing3 13 8 5 Blanusa First Snark Graph 14 7 5 Blanusa Second Snark Graph 15 9 5 Flower Snark 16 11 4 Mycielski Graph 5 17 12 3 s13e 18 25 4 circulant_50_1_3 19 21 3 s22e 20 4 3 difficult11 21 10 6 Desargues Graph 22 9 5 Flower Snark 23 5 3 Frucht graph 24 15 5 Hoffman-Singleton graph 25 9 6 Pappus Graph 26 5 4 Grotzsch graph 27 27 8 Gray graph 28 7 6 Heawood graph 29 6 4 Herschel graph 30 12 7 Coxeter Graph 31 7 5 Brinkmann graph 32 15 8 Tutte-Coxeter graph 33 19 4 Tutte Graph 34 7 5 Robertson Graph 35 10 4 Folkman Graph 36 35 10 Balaban 10-cage 37 9 6 Pappus Graph 38 5 3 Tietze Graph 39 12 5 Sylvester Graph 40 21 5 Szekeres Snark Graph 41 8 6 Moebius-Kantor Graph 42 8 3 ryan 43 4 3 inp 44 6 3 p10k4 45 43 5 c100 46 10 3 starfish 47 4 3 Shrikhande graph 48 7 3 sylvester 49 5 3 edge_critical_11_1 50 5 3 edge_critical_11_2 51 6 3 pepper_residue_graph 52 5 3 ce5 53 4 3 flower_with_4_petals 54 6 3 paw_x_paw 55 6 3 triangle_star 56 5 3 ce8 57 6 3 ce10 58 5 3 binary_octahedron

#add the proven results to theorems to get new conjectures - that simplify investigation
#load the database of precomputed invariant values
load("objects-invariants-properties/gt_precomputed_database.sage")
db = os.environ['HOME'] +'/objects-invariants-properties/gt_precomputed_database.db'
#now get a table out of the precomputed database that can be used by the invariant-relation conjecturing program
precomputed_invs = precomputed_invariants_for_conjecture(database=db)

#note each of the folling theorems *is* either an invariant (and could be precomputed) or
#some just_defined number that's an integer
#so there's no possibility of rounding-error numerical instability

def get_value(invariant, o):
    precomputed_value = None
    o_key = precomputed_invs[1](o)
    i_key = precomputed_invs[2](invariant)
    if precomputed_invs:
        if o_key in precomputed_invs[0]:
            if i_key in precomputed_invs[0][o_key]:
                precomputed_value = precomputed_invs[0][o_key][i_key]
    if precomputed_value is None:
        return invariant(o)
    else:
        return precomputed_value

girth_theta_bound = lambda g: min(g.girth(),floor(get_value(Graph.lovasz_theta,g)))

max_degree_minus_triangles = lambda g: max_degree(g) - number_of_triangles(g)

order_brooks_bound = lambda x: ceil(order(x)/brooks(x))

theorems = [girth_theta_bound, average_distance, Graph.radius, residue, max_even_minus_even_horizontal, critical_independence_number, max_degree_minus_triangles, order_brooks_bound]

#use get_value so that conjecture program uses precomputed value in theory calculation instead of recomputing (maybe incorrectly)
max_theorem = lambda g: ceil(max(get_value(f, g) for f in theorems))
#for this to work each "theorem" that has a potential numerical error needs to be precomputed and included in the db

#there is a problem with a fiedler number computation, removing fiedler (35 in the list) from invariants
#efficiently_computable_invariants.pop(35)
invariants = [independence_number] + efficiently_computable_invariants

objects = graph_objects

#no results after the default 5 seconds
#so there could be a bug - or no significant conjecture yet - increasing the time *may* help
conjs = conjecture(objects, invariants, invariants.index(independence_number), upperBound = False, theory = [max_theorem], precomputed = precomputed_invs, time = 100)
for c in conjs:
    print c

independence_number(x) >= -average_distance(x) + ceil(lovasz_theta(x)) independence_number(x) >= 1/2*cvetkovic(x) independence_number(x) >= diameter(x)/different_degrees(x) independence_number(x) >= order(x)/brooks(x) independence_number(x) >= order(x)/szekeres_wilf(x) independence_number(x) >= -max_common_neighbors(x) + min_degree(x) independence_number(x) >= max_degree(x) - order_automorphism_group(x) independence_number(x) >= -card_periphery(x) + matching_number(x) independence_number(x) >= minimum(min_degree(x), floor(lovasz_theta(x))) independence_number(x) >= minimum(diameter(x), lovasz_theta(x)) independence_number(x) >= lovasz_theta(x)/radius(x) independence_number(x) >= maximum(max_even_minus_even_horizontal(x), 1/2*lovasz_theta(x)) independence_number(x) >= maximum(critical_independence_number(x), 1/2*lovasz_theta(x)) independence_number(x) >= matching_number(x) - order_automorphism_group(x) - 1 independence_number(x) >= ceil(1/2*cvetkovic(x)) independence_number(x) >= card_positive_eigenvalues(x) - lovasz_theta(x) independence_number(x) >= card_negative_eigenvalues(x) - sigma_2(x) independence_number(x) >= minimum(max_degree(x), floor(lovasz_theta(x))) independence_number(x) >= floor(1/2*card_positive_eigenvalues(x)) independence_number(x) >= minimum(lovasz_theta(x), tan(order(x))) independence_number(x) >= maximum(residue(x), 1/2*lovasz_theta(x)) independence_number(x) >= floor(lovasz_theta(x))/vertex_con(x) independence_number(x) >= matching_number(x) - sigma_2(x) - 1 independence_number(x) >= -10^different_degrees(x) + matching_number(x) independence_number(x) >= 2*floor(arccosh(lovasz_theta(x))) independence_number(x) >= minimum(floor(lovasz_theta(x)), tan(spanning_trees_count(x))) independence_number(x) >= floor(arccosh(lovasz_theta(x)))^2 independence_number(x) >= minimum(card_positive_eigenvalues(x), 2*card_zero_eigenvalues(x)) independence_number(x) >= ceil(order(x)/brooks(x)) independence_number(x) >= -1/2*diameter(x) + lovasz_theta(x) independence_number(x) >= floor(tan(barrus_bound(x) - 1)) independence_number(x) >= barrus_bound(x) - maximum(card_center(x), card_positive_eigenvalues(x)) independence_number(x) >= floor(tan(floor(gutman_energy(x)))) independence_number(x) >= minimum(floor(lovasz_theta(x)), max_even_minus_even_horizontal(x) + 1)

conjs[3]

independence_number(x) >= order(x)/brooks(x)

for g in graph_objects:
    if order_brooks_bound(g) < conjs[3](g):
        print order_brooks_bound(g), conjs[3](g), g.name()

#investigate wilf-szekeres theorem: what's in gt
#this can also be modified to an alpha bound

load("gt.sage")

loaded graph dc1024 loaded graph dc2048 loaded graph properties data file loaded graph invariants data file

#investigate lemma: alpha >= diameter for regular graphs
load("conjecturing.py")
load("gt.sage")

#load the database of precomputed invariant values
load("objects-invariants-properties/gt_precomputed_database.sage")
db = os.environ['HOME'] +'/objects-invariants-properties/gt_precomputed_database.db'
#now get a table out of the precomputed database that can be used by the invariant-relation conjecturing program
precomputed_invs = precomputed_invariants_for_conjecture(database=db)

#note each of the folling theorems *is* either an invariant (and could be precomputed) or
#some just_defined number that's an integer
#so there's no possibility of rounding-error numerical instability

def get_value(invariant, o):
    precomputed_value = None
    o_key = precomputed_invs[1](o)
    i_key = precomputed_invs[2](invariant)
    if precomputed_invs:
        if o_key in precomputed_invs[0]:
            if i_key in precomputed_invs[0][o_key]:
                precomputed_value = precomputed_invs[0][o_key][i_key]
    if precomputed_value is None:
        return invariant(o)
    else:
        return precomputed_value

girth_theta_bound = lambda g: min(g.girth(),floor(get_value(Graph.lovasz_theta,g)))

theorems = [Graph.diameter]
#use get_value so that conjecture program uses precomputed value in theory calculation instead of recomputing (maybe incorrectly)
####min_theorem = lambda g: floor(min(get_value(f, g) for f in theorems))
#for this to work each "theorem" that has a potential numerical error needs to be precomputed and included in the db

#there is a problem with a fiedler number computation, removing fiedler (35 in the list) from invariants
#efficiently_computable_invariants.pop(35)
invariants = [independence_number] + efficiently_computable_invariants

objects = [g for g in graph_objects if g.is_regular()]

#no results after the default 5 seconds
#so there could be a bug - or no significant conjecture yet - increasing the time *may* help
conjs = conjecture(objects, invariants, invariants.index(independence_number), upperBound = False, theory = theorems, precomputed = precomputed_invs, time = 100)
for c in conjs:
    print c

loaded graph dc1024 loaded graph dc2048 loaded graph properties data file loaded graph invariants data file independence_number(x) >= residue(x) independence_number(x) >= max_even_minus_even_horizontal(x) independence_number(x) >= floor(tan(barrus_bound(x) - 1)) independence_number(x) >= min_degree(x) - number_of_triangles(x) independence_number(x) >= -diameter(x) + 2*residue(x) independence_number(x) >= -max_common_neighbors(x) + min_degree(x) independence_number(x) >= -card_periphery(x) + matching_number(x) independence_number(x) >= maximum(diameter(x), residue(x)) independence_number(x) >= matching_number(x) - sigma_2(x) - 1 independence_number(x) >= lovasz_theta(x)/vertex_con(x) independence_number(x) >= matching_number(x) - order_automorphism_group(x) - 1 independence_number(x) >= -10^different_degrees(x) + matching_number(x) independence_number(x) >= card_negative_eigenvalues(x) - sigma_2(x) independence_number(x) >= card_periphery(x) - maximum(card_center(x), max_even_minus_even_horizontal(x)) independence_number(x) >= -1/2*diameter(x) + lovasz_theta(x) independence_number(x) >= 1/2*card_center(x) - 1/2*order_automorphism_group(x) independence_number(x) >= floor(arcsinh(lovasz_theta(x)))^2 independence_number(x) >= minimum(floor(lovasz_theta(x)), tan(spanning_trees_count(x))) independence_number(x) >= minimum(card_positive_eigenvalues(x), 2*card_zero_eigenvalues(x)) independence_number(x) >= minimum(floor(lovasz_theta(x)), max_even_minus_even_horizontal(x) + 1)

objects = [g for g in graph_objects if g.is_regular()]

len(objects)

73

for g in objects:
    print independence_number(g), g.diameter(), g.name()

1 1 k3 1 1 k4 1 1 k5 8 5 Dodecahedron 3 3 c8chorded 5 2 Clebsch graph 9 5 c24 11 6 c26 24 9 c60 18 6 c6xc6 10 6 holton_mckay 4 4 sixfour 2 2 c4 4 2 Petersen graph 1 1 p2 19 8 Tutte Graph 4 4 throwing 4 4 throwing2 4 4 throwing3 8 4 Blanusa First Snark Graph 7 4 Blanusa Second Snark Graph 9 4 Flower Snark 3 3 ryan3 1 1 k10 25 9 circulant_50_1_3 4 2 Chvatal graph 10 5 Desargues Graph 9 4 Flower Snark 5 4 Frucht graph 15 2 Hoffman-Singleton graph 2 2 Octahedron 3 2 Thomsen graph 4 2 Petersen graph 9 4 Pappus Graph 27 6 Gray graph 7 3 Heawood graph 12 4 Coxeter Graph 7 3 Brinkmann graph 15 4 Tutte-Coxeter graph 19 8 Tutte Graph 7 3 Robertson Graph 10 4 Folkman Graph 35 6 Balaban 10-cage 9 4 Pappus Graph 5 3 Tietze Graph 12 3 Sylvester Graph 21 7 Szekeres Snark Graph 8 4 Moebius-Kantor Graph 8 8 ryan 3 3 regular_non_trans 43 12 c100 4 2 Shrikhande graph 7 6 sylvester 2 2 c5 3 3 c6 4 4 c9 4 3 ce3 5 2 ce5 3 2 Wagner Graph 5 4 binary_octahedron 2 2 prism 1 1 alpha_critical_A_ 1 1 alpha_critical_Bw 1 1 alpha_critical_C~ 2 2 alpha_critical_Dhc 1 1 alpha_critical_D~{ 1 1 alpha_critical_E~~w 3 3 alpha_critical_FhCKG 1 1 alpha_critical_F~~~w 2 2 alpha_critical_GbMmvG 1 1 alpha_critical_G~~~~{ 4 4 alpha_critical_HhCGGE@ 1 1 alpha_critical_H~~~~~~

"""
independence_number(x) >= -average_distance(x) + ceil(lovasz_theta(x))
CE: Graph('epCpih@K}gSGIZfc?Rkf{EWtVKJTmJtWYl_IoDOKOikwDSKtbH\fi_g`affO\|Agq`WcLoakSLNPaWZ@PQhCh?ylTR\tIR?WfoJNYJ@B{GiOWMUZX_puFP?')

independence_number(x) >= ceil(1/2*cvetkovic(x))
independence_number(x) >= 1/2*cvetkovic(x)
CE: Graph('Gvz~r{')

independence_number(x) >= -max_common_neighbors(x) + min_degree(x)
CE: Graph('eLvnv~yv{yJ~rlB^Mn|v^nz~V]mwVji}^vZf{\\nqZLfVBze}y[ym|jevvt~NNucret|~ejj~rz}Q\~^an}XzTV~t]a]v}nx\u]n{}~ffqjn`~e}lZvV]t_')

independence_number(x) >= max_degree(x) - order_automorphism_group(x)
CE: Graph('ETzw')

independence_number(x) >= -card_periphery(x) + matching_number(x)
CE: Graph('I~~~}~~~w')

independence_number(x) >= lovasz_theta(x)/radius(x)
CE: Graph('~?@A~~~~~~z~~~~~~~~^~~~~~z~~~~~~~~~~~~~~~v~~~v~~~~~~~~~~z~~~~~~~~^~~~~~~~~~}\~~}v~^~~}~~^~~~~~~~~~~~~^~~~~~~~~V~~~n~~n~~~~~~}~~|~}~~~~~~~~~~~~~~~~~~~~~vv~|~~~~~~~~~~~~~~~~~z~~w~~~~~~~~~~~~~~~~n~~~|~~~~~~~v~|~~~~~~~~~~}~|~r~V~~~n~~~~~~~~z~~}}~}~~~~vz~~z~~~z}~~~n~~~~~~~~~~~~n~~~~~~~z~~~~~~~~~~~~~~^~~~~~~~~~n~~]~~~~~n~~~}~~~~~~~~~~^~^~~~~}~~~~~~~~~~~z~~~~^~~~~~~w')

independence_number(x) >= matching_number(x) - order_automorphism_group(x) - 1
CE: Graph('I~~Lt~\Nw')

independence_number(x) >= card_positive_eigenvalues(x) - lovasz_theta(x)
CE: Graph('N^nN~~}Z~|}~~\~]zzw')

independence_number(x) >= card_negative_eigenvalues(x) - sigma_2(x)
CE: Graph('IOilnemjG')
"""

#adding NB counterexamples to above conjectures
#generating new round of girth-theta lemma conjectures
load("conjecturing.py")
load("gt.sage")

#add the proven results to theorems to get new conjectures - that simplify investigation
#load the database of precomputed invariant values
load("objects-invariants-properties/gt_precomputed_database.sage")
db = os.environ['HOME'] +'/objects-invariants-properties/gt_precomputed_database.db'
#now get a table out of the precomputed database that can be used by the invariant-relation conjecturing program
precomputed_invs = precomputed_invariants_for_conjecture(database=db)

#note each of the folling theorems *is* either an invariant (and could be precomputed) or
#some just_defined number that's an integer
#so there's no possibility of rounding-error numerical instability

def get_value(invariant, o):
    precomputed_value = None
    o_key = precomputed_invs[1](o)
    i_key = precomputed_invs[2](invariant)
    if precomputed_invs:
        if o_key in precomputed_invs[0]:
            if i_key in precomputed_invs[0][o_key]:
                precomputed_value = precomputed_invs[0][o_key][i_key]
    if precomputed_value is None:
        return invariant(o)
    else:
        return precomputed_value

girth_theta_bound = lambda g: min(g.girth(),floor(get_value(Graph.lovasz_theta,g)))

max_degree_minus_triangles = lambda g: max_degree(g) - number_of_triangles(g)

order_brooks_bound = lambda x: ceil(get_value(order, x)/get_value(brooks,x))

theorems = [girth_theta_bound, average_distance, Graph.radius, residue, max_even_minus_even_horizontal, critical_independence_number, max_degree_minus_triangles, order_brooks_bound]

#use get_value so that conjecture program uses precomputed value in theory calculation instead of recomputing (maybe incorrectly)
max_theorem = lambda g: ceil(max(get_value(f, g) for f in theorems))
#for this to work each "theorem" that has a potential numerical error needs to be precomputed and included in the db

#there is a problem with a fiedler number computation, removing fiedler (35 in the list) from invariants
#efficiently_computable_invariants.pop(35)
invariants = [independence_number] + efficiently_computable_invariants

nb1=Graph('epCpih@K}gSGIZfc?Rkf{EWtVKJTmJtWYl_IoDOKOikwDSKtbH\\fi_g`affO\\|Agq`WcLoakSLNPaWZ@PQhCh?ylTR\\tIR?WfoJNYJ@B{GiOWMUZX_puFP?')
nb2=Graph('Gvz~r{')
nb3=Graph('eLvnv~yv{yJ~rlB^Mn|v^nz~V]mwVji}^vZf{\\\\nqZLfVBze}y[ym|jevvt~NNucret|~ejj~rz}Q\\~^an}XzTV~t]a]v}nx\\u]n{}~ffqjn`~e}lZvV]t_')
nb4=Graph('ETzw')
nb5=Graph('~?@A~~~~~~z~~~~~~~~^~~~~~z~~~~~~~~~~~~~~~v~~~v~~~~~~~~~~z~~~~~~~~^~~~~~~~~~}\~~}v~^~~}~~^~~~~~~~~~~~~^~~~~~~~~V~~~n~~n~~~~~~}~~|~}~~~~~~~~~~~~~~~~~~~~~vv~|~~~~~~~~~~~~~~~~~z~~w~~~~~~~~~~~~~~~~n~~~|~~~~~~~v~|~~~~~~~~~~}~|~r~V~~~n~~~~~~~~z~~}}~}~~~~vz~~z~~~z}~~~n~~~~~~~~~~~~n~~~~~~~z~~~~~~~~~~~~~~^~~~~~~~~~n~~]~~~~~n~~~}~~~~~~~~~~^~^~~~~}~~~~~~~~~~~z~~~~^~~~~~~w')
nb6=Graph('I~~Lt~\Nw')
nb7=Graph('N^nN~~}Z~|}~~\~]zzw')
nb8=Graph('IOilnemjG')
nb9=Graph('Hx~\\rnV')
nb10=Graph('z@M@E?OYOSCPBTp?mOWaP_?W[OG[abE_?P[@?@REt?ggAAOH?N@?CATE\oE?WO@GOKu?LJ_??SDP@CIA?AFHCC?kZQMo@CkOGoiJSs`?g?oDJqC?S?qJSqA?GN]?OPd?cGHE?AOpE_c_O@kC_?DF@HGgJ?ygAACdcCMPA[d`SHE@?PqRE?CO_?CWO?H_b_EBoOKI@CWAadQ?eOO?oT_@STAWCCCMOK?A@?TsBoJa@?PGQ_CiKPC_@_iE_hL@ACAIJQDgOSG?G[cG_D[A_CbDKO[goBH_?S?')

objects = graph_objects + [nb1,nb2,nb3,nb4,nb5,nb6,nb7,nb8,nb9,nb10]

#no results after the default 5 seconds
#so there could be a bug - or no significant conjecture yet - increasing the time *may* help
conjs = conjecture(objects, invariants, invariants.index(independence_number), upperBound = False, theory = [max_theorem], precomputed = precomputed_invs, time = 100)
for c in conjs:
    print c

couldn't load dc1024_g6string.sobj couldn't load dc2048_g6string.sobj can't load graph properties sobj file can't load graph invariant sobj file independence_number(x) >= maximum(residue(x), 1/2*lovasz_theta(x)) independence_number(x) >= ceil(1/2*lovasz_theta(x)) independence_number(x) >= order(x)/szekeres_wilf(x) independence_number(x) >= welsh_powell(x)/card_periphery(x) independence_number(x) >= floor(tan(log(barrus_bound(x))/log(10))) independence_number(x) >= maximum(max_even_minus_even_horizontal(x), 1/2*lovasz_theta(x)) independence_number(x) >= -card_center(x) + floor(lovasz_theta(x)) independence_number(x) >= (barrus_bound(x) - 1)/card_periphery(x) independence_number(x) >= maximum(critical_independence_number(x), 1/2*lovasz_theta(x)) independence_number(x) >= -10^max_common_neighbors(x) + matching_number(x) independence_number(x) >= barrus_bound(x) - maximum(card_center(x), card_positive_eigenvalues(x)) independence_number(x) >= (residue(x) - 1)^min_common_neighbors(x) independence_number(x) >= floor(lovasz_theta(x))/vertex_con(x) independence_number(x) >= floor(tan(barrus_bound(x) - 1)) independence_number(x) >= -brinkmann_steffen(x) + card_negative_eigenvalues(x) independence_number(x) >= matching_number(x) - sigma_2(x) - 1 independence_number(x) >= -max_common_neighbors(x) + min_degree(x) - 1 independence_number(x) >= floor(sqrt(barrus_bound(x))) independence_number(x) >= ceil(log(barrus_bound(x))) independence_number(x) >= 2*floor(arccosh(lovasz_theta(x))) independence_number(x) >= sqrt(szeged_index(x))/gutman_energy(x) independence_number(x) >= maximum(radius(x), 1/2*lovasz_theta(x)) independence_number(x) >= minimum(floor(lovasz_theta(x)), tan(spanning_trees_count(x))) independence_number(x) >= floor(arccosh(lovasz_theta(x)))^2 independence_number(x) >= -card_periphery(x) + min_degree(x) - 1 independence_number(x) >= -min_common_neighbors(x) + 1/2*min_degree(x) independence_number(x) >= sqrt(cycle_space_dimension(x)) - number_of_triangles(x) independence_number(x) >= 2*fractional_alpha(x)/szekeres_wilf(x) independence_number(x) >= minimum(sum_temperatures(x), card_negative_eigenvalues(x) - number_of_triangles(x)) independence_number(x) >= 1/2*card_negative_eigenvalues(x) - max_common_neighbors(x) independence_number(x) >= -number_of_triangles(x)^average_vertex_temperature(x) + max_degree(x) independence_number(x) >= -2*card_center(x) + cvetkovic(x) independence_number(x) >= ceil(1/2*lovasz_theta(x) + 1/2) independence_number(x) >= ceil(log(lovasz_theta(x)^2)) independence_number(x) >= -(card_negative_eigenvalues(x) - card_positive_eigenvalues(x))*card_zero_eigenvalues(x) independence_number(x) >= floor(tan(floor(gutman_energy(x)))) independence_number(x) >= floor(tan(e^card_positive_eigenvalues(x))) independence_number(x) >= minimum(floor(lovasz_theta(x)), max_even_minus_even_horizontal(x) + 1)

nb1

nb1=Graph('epCpih@K}gSGIZfc?Rkf{EWtVKJTmJtWYl_IoDOKOikwDSKtbH\\fi_g`affO\\|Agq`WcLoakSLNPaWZ@PQhCh?ylTR\\tIR?WfoJNYJ@B{GiOWMUZX_puFP?')

nb2=Graph('Gvz~r{')
nb4=Graph('ETzw')

nb3=Graph('eLvnv~yv{yJ~rlB^Mn|v^nz~V]mwVji}^vZf{\\\\nqZLfVBze}y[ym|jevvt~NNucret|~ejj~rz}Q\\~^an}XzTV~t]a]v}nx\\u]n{}~ffqjn`~e}lZvV]t_')

nb5=Graph('~?@A~~~~~~z~~~~~~~~^~~~~~z~~~~~~~~~~~~~~~v~~~v~~~~~~~~~~z~~~~~~~~^~~~~~~~~~}\~~}v~^~~}~~^~~~~~~~~~~~~^~~~~~~~~V~~~n~~n~~~~~~}~~|~}~~~~~~~~~~~~~~~~~~~~~vv~|~~~~~~~~~~~~~~~~~z~~w~~~~~~~~~~~~~~~~n~~~|~~~~~~~v~|~~~~~~~~~~}~|~r~V~~~n~~~~~~~~z~~}}~}~~~~vz~~z~~~z}~~~n~~~~~~~~~~~~n~~~~~~~z~~~~~~~~~~~~~~^~~~~~~~~~n~~]~~~~~n~~~}~~~~~~~~~~^~^~~~~}~~~~~~~~~~~z~~~~^~~~~~~w')

nb6=Graph('I~~Lt~\Nw')
nb7=Graph('N^nN~~}Z~|}~~\~]zzw')
nb8=Graph('IOilnemjG')

for g in [nb2,nb4,nb5,nb6,nb7,nb8]:
    g.show()

nb5.order()

66

independence_number(nb5)

2

nb5.lovasz_theta()

2.236068

#investigate lemma: alpha >= diameter for regular graphs
#ROUND 2: adding NB graphs and theoretical knowledge
load("conjecturing.py")
load("gt.sage")

#load the database of precomputed invariant values
load("objects-invariants-properties/gt_precomputed_database.sage")
db = os.environ['HOME'] +'/objects-invariants-properties/gt_precomputed_database.db'
#now get a table out of the precomputed database that can be used by the invariant-relation conjecturing program
precomputed_invs = precomputed_invariants_for_conjecture(database=db)

#note each of the folling theorems *is* either an invariant (and could be precomputed) or
#some just_defined number that's an integer
#so there's no possibility of rounding-error numerical instability

def get_value(invariant, o):
    precomputed_value = None
    o_key = precomputed_invs[1](o)
    i_key = precomputed_invs[2](invariant)
    if precomputed_invs:
        if o_key in precomputed_invs[0]:
            if i_key in precomputed_invs[0][o_key]:
                precomputed_value = precomputed_invs[0][o_key][i_key]
    if precomputed_value is None:
        return invariant(o)
    else:
        return precomputed_value

girth_theta_bound = lambda g: min(g.girth(),floor(get_value(Graph.lovasz_theta,g)))

max_degree_minus_triangles = lambda g: max_degree(g) - number_of_triangles(g)

order_brooks_bound = lambda x: ceil(order(x)/brooks(x))

theorems = [Graph.diameter, average_distance, Graph.radius, residue, max_even_minus_even_horizontal, critical_independence_number, max_degree_minus_triangles, order_brooks_bound]

#use get_value so that conjecture program uses precomputed value in theory calculation instead of recomputing (maybe incorrectly)
max_theorem = lambda g: ceil(max(get_value(f, g) for f in theorems))
#for this to work each "theorem" that has a potential numerical error needs to be precomputed and included in the db

#use get_value so that conjecture program uses precomputed value in theory calculation instead of recomputing (maybe incorrectly)
####min_theorem = lambda g: floor(min(get_value(f, g) for f in theorems))
#for this to work each "theorem" that has a potential numerical error needs to be precomputed and included in the db

#there is a problem with a fiedler number computation, removing fiedler (35 in the list) from invariants
#efficiently_computable_invariants.pop(35)
invariants = [independence_number] + efficiently_computable_invariants

objects = [g for g in graph_objects if g.is_regular()]

#no results after the default 5 seconds
#so there could be a bug - or no significant conjecture yet - increasing the time *may* help
conjs = conjecture(objects, invariants, invariants.index(independence_number), upperBound = False, theory = [max_theorem], precomputed = precomputed_invs, time = 100)
for c in conjs:
    print c

loaded graph dc1024 loaded graph dc2048 loaded graph properties data file loaded graph invariants data file independence_number(x) >= maximum(max_even_minus_even_horizontal(x), 1/2*lovasz_theta(x)) independence_number(x) >= 1/2*cvetkovic(x) independence_number(x) >= sqrt(barrus_bound(x)) independence_number(x) >= order(x)/brooks(x) independence_number(x) >= -max_common_neighbors(x) + min_degree(x) independence_number(x) >= -card_periphery(x) + matching_number(x) independence_number(x) >= -1/2*diameter(x) + lovasz_theta(x) independence_number(x) >= lovasz_theta(x)/vertex_con(x) independence_number(x) >= -diameter(x) + 2*residue(x) independence_number(x) >= matching_number(x) - order_automorphism_group(x) - 1 independence_number(x) >= minimum(cvetkovic(x), inverse_degree(x)) independence_number(x) >= card_positive_eigenvalues(x) - lovasz_theta(x) independence_number(x) >= card_negative_eigenvalues(x) - sigma_2(x) independence_number(x) >= minimum(lovasz_theta(x), tan(order(x))) independence_number(x) >= ceil(sqrt(barrus_bound(x))) independence_number(x) >= ceil(1/2*cvetkovic(x)) independence_number(x) >= -card_periphery(x) + 2*diameter(x) independence_number(x) >= matching_number(x) - sigma_2(x) - 1 independence_number(x) >= -10^different_degrees(x) + matching_number(x) independence_number(x) >= card_periphery(x) - maximum(card_center(x), max_even_minus_even_horizontal(x)) independence_number(x) >= 1/2*card_center(x) - 1/2*order_automorphism_group(x) independence_number(x) >= floor(tan(barrus_bound(x) - 1)) independence_number(x) >= floor(arcsinh(lovasz_theta(x)))^2 independence_number(x) >= minimum(floor(lovasz_theta(x)), tan(spanning_trees_count(x))) independence_number(x) >= minimum(card_positive_eigenvalues(x), 2*card_zero_eigenvalues(x)) independence_number(x) >= minimum(floor(lovasz_theta(x)), max_even_minus_even_horizontal(x) + 1)

for g in [g for g in graph_objects if g.is_regular()]:
    print order(g)/brooks(g), order_brooks_bound(g), g.name()

1 1 k3 1 1 k4 1 1 k5 6 6 Dodecahedron 2 2 c8chorded 3 3 Clebsch graph 8 8 c24 8 8 c26 20 20 c60 9 9 c6xc6 8 8 holton_mckay 3 3 sixfour 2 2 c4 3 3 Petersen graph 1 1 p2 15 15 Tutte Graph 2 2 throwing 3 3 throwing2 3 3 throwing3 6 6 Blanusa First Snark Graph 6 6 Blanusa Second Snark Graph 6 6 Flower Snark 2 2 ryan3 1 1 k10 12 12 circulant_50_1_3 3 3 Chvatal graph 6 6 Desargues Graph 6 6 Flower Snark 4 4 Frucht graph 7 7 Hoffman-Singleton graph 1 1 Octahedron 2 2 Thomsen graph 3 3 Petersen graph 6 6 Pappus Graph 18 18 Gray graph 4 4 Heawood graph 9 9 Coxeter Graph 5 5 Brinkmann graph 10 10 Tutte-Coxeter graph 15 15 Tutte Graph 4 4 Robertson Graph 5 5 Folkman Graph 23 23 Balaban 10-cage 6 6 Pappus Graph 4 4 Tietze Graph 7 7 Sylvester Graph 16 16 Szekeres Snark Graph 5 5 Moebius-Kantor Graph 8 8 ryan 2 2 regular_non_trans 33 33 c100 2 2 Shrikhande graph 5 5 sylvester 5/3 2 c5 3 3 c6 3 3 c9 2 2 ce3 3 3 ce5 2 2 Wagner Graph 3 3 binary_octahedron 2 2 prism 1 1 alpha_critical_A_ 1 1 alpha_critical_Bw 1 1 alpha_critical_C~ 5/3 2 alpha_critical_Dhc 1 1 alpha_critical_D~{ 1 1 alpha_critical_E~~w 7/3 3 alpha_critical_FhCKG 1 1 alpha_critical_F~~~w 2 2 alpha_critical_GbMmvG 1 1 alpha_critical_G~~~~{ 3 3 alpha_critical_HhCGGE@ 1 1 alpha_critical_H~~~~~~

theorems = [Graph.diameter, average_distance, Graph.radius, residue, max_even_minus_even_horizontal, critical_independence_number, max_degree_minus_triangles, order_brooks_bound]

for g in [g for g in graph_objects if g.is_regular()]:
    if independence_number(g) != max_theorem(g):
        print independence_number(g), max_theorem(g), g.name()

8 7 Dodecahedron 9 8 c24 11 9 c26 24 21 c60 4 3 Petersen graph 19 17 Tutte Graph 8 7 Blanusa First Snark Graph 7 6 Blanusa Second Snark Graph 15 7 Hoffman-Singleton graph 4 3 Petersen graph 12 10 Coxeter Graph 7 5 Brinkmann graph 19 17 Tutte Graph 7 4 Robertson Graph 12 7 Sylvester Graph 21 19 Szekeres Snark Graph 43 40 c100 4 3 Shrikhande graph 5 3 ce5 5 4 binary_octahedron

#add szekeres-wilf theoretical knowledge

#adding NB counterexamples to above conjectures
#generating new round of girth-theta lemma conjectures
load("conjecturing.py")
load("gt.sage")

#add the proven results to theorems to get new conjectures - that simplify investigation
#load the database of precomputed invariant values
load("objects-invariants-properties/gt_precomputed_database.sage")
db = os.environ['HOME'] +'/objects-invariants-properties/gt_precomputed_database.db'
#now get a table out of the precomputed database that can be used by the invariant-relation conjecturing program
precomputed_invs = precomputed_invariants_for_conjecture(database=db)

#note each of the folling theorems *is* either an invariant (and could be precomputed) or
#some just_defined number that's an integer
#so there's no possibility of rounding-error numerical instability

def get_value(invariant, o):
    precomputed_value = None
    o_key = precomputed_invs[1](o)
    i_key = precomputed_invs[2](invariant)
    if precomputed_invs:
        if o_key in precomputed_invs[0]:
            if i_key in precomputed_invs[0][o_key]:
                precomputed_value = precomputed_invs[0][o_key][i_key]
    if precomputed_value is None:
        return invariant(o)
    else:
        return precomputed_value

girth_theta_bound = lambda g: min(g.girth(),floor(get_value(Graph.lovasz_theta,g)))

max_degree_minus_triangles = lambda g: max_degree(g) - number_of_triangles(g)

order_brooks_bound = lambda x: ceil(order(x)/brooks(x))

szekeres_wilf_bound = lambda x: ceil(order(x)/szekeres_wilf(x))

theorems = [girth_theta_bound, average_distance, Graph.radius, residue, max_even_minus_even_horizontal, critical_independence_number, max_degree_minus_triangles, order_brooks_bound, szekeres_wilf_bound]

#use get_value so that conjecture program uses precomputed value in theory calculation instead of recomputing (maybe incorrectly)
max_theorem = lambda g: ceil(max(get_value(f, g) for f in theorems))
#for this to work each "theorem" that has a potential numerical error needs to be precomputed and included in the db

#there is a problem with a fiedler number computation, removing fiedler (35 in the list) from invariants
#efficiently_computable_invariants.pop(35)
invariants = [independence_number] + efficiently_computable_invariants

nb1=Graph('epCpih@K}gSGIZfc?Rkf{EWtVKJTmJtWYl_IoDOKOikwDSKtbH\\fi_g`affO\\|Agq`WcLoakSLNPaWZ@PQhCh?ylTR\\tIR?WfoJNYJ@B{GiOWMUZX_puFP?')
nb2=Graph('Gvz~r{')
nb3=Graph('eLvnv~yv{yJ~rlB^Mn|v^nz~V]mwVji}^vZf{\\\\nqZLfVBze}y[ym|jevvt~NNucret|~ejj~rz}Q\\~^an}XzTV~t]a]v}nx\\u]n{}~ffqjn`~e}lZvV]t_')
nb4=Graph('ETzw')
nb5=Graph('~?@A~~~~~~z~~~~~~~~^~~~~~z~~~~~~~~~~~~~~~v~~~v~~~~~~~~~~z~~~~~~~~^~~~~~~~~~}\~~}v~^~~}~~^~~~~~~~~~~~~^~~~~~~~~V~~~n~~n~~~~~~}~~|~}~~~~~~~~~~~~~~~~~~~~~vv~|~~~~~~~~~~~~~~~~~z~~w~~~~~~~~~~~~~~~~n~~~|~~~~~~~v~|~~~~~~~~~~}~|~r~V~~~n~~~~~~~~z~~}}~}~~~~vz~~z~~~z}~~~n~~~~~~~~~~~~n~~~~~~~z~~~~~~~~~~~~~~^~~~~~~~~~n~~]~~~~~n~~~}~~~~~~~~~~^~^~~~~}~~~~~~~~~~~z~~~~^~~~~~~w')
nb6=Graph('I~~Lt~\Nw')
nb7=Graph('N^nN~~}Z~|}~~\~]zzw')
nb8=Graph('IOilnemjG')
nb9=Graph('Hx~\\rnV')
nb10=Graph('z@M@E?OYOSCPBTp?mOWaP_?W[OG[abE_?P[@?@REt?ggAAOH?N@?CATE\oE?WO@GOKu?LJ_??SDP@CIA?AFHCC?kZQMo@CkOGoiJSs`?g?oDJqC?S?qJSqA?GN]?OPd?cGHE?AOpE_c_O@kC_?DF@HGgJ?ygAACdcCMPA[d`SHE@?PqRE?CO_?CWO?H_b_EBoOKI@CWAadQ?eOO?oT_@STAWCCCMOK?A@?TsBoJa@?PGQ_CiKPC_@_iE_hL@ACAIJQDgOSG?G[cG_D[A_CbDKO[goBH_?S?')

objects = graph_objects + [nb1,nb2,nb3,nb4,nb5,nb6,nb7,nb8,nb9,nb10]

#no results after the default 5 seconds
#so there could be a bug - or no significant conjecture yet - increasing the time *may* help
conjs = conjecture(objects, invariants, invariants.index(independence_number), upperBound = False, theory = [max_theorem], precomputed = precomputed_invs, time = 100)
for c in conjs:
    print c

loaded graph dc1024 loaded graph dc2048 loaded graph properties data file loaded graph invariants data file independence_number(x) >= maximum(max_even_minus_even_horizontal(x), 1/2*lovasz_theta(x)) independence_number(x) >= floor(tan(log(barrus_bound(x))/log(10))) independence_number(x) >= diameter(x)/different_degrees(x) independence_number(x) >= order(x)/brooks(x) independence_number(x) >= (barrus_bound(x) - 1)/card_periphery(x) independence_number(x) >= minimum(diameter(x), lovasz_theta(x)) independence_number(x) >= -card_center(x) + floor(lovasz_theta(x)) independence_number(x) >= -10^max_common_neighbors(x) + matching_number(x) independence_number(x) >= maximum(critical_independence_number(x), 1/2*lovasz_theta(x)) independence_number(x) >= (residue(x) - 1)^min_common_neighbors(x) independence_number(x) >= barrus_bound(x) - maximum(card_center(x), card_positive_eigenvalues(x)) independence_number(x) >= floor(tan(barrus_bound(x) - 1)) independence_number(x) >= -brinkmann_steffen(x) + card_negative_eigenvalues(x) independence_number(x) >= minimum(floor(lovasz_theta(x)), tan(spanning_trees_count(x))) independence_number(x) >= -max_common_neighbors(x) + min_degree(x) - 1 independence_number(x) >= maximum(residue(x), 1/2*lovasz_theta(x)) independence_number(x) >= floor(lovasz_theta(x))/vertex_con(x) independence_number(x) >= minimum(lovasz_theta(x), tan(order(x))) independence_number(x) >= 2*floor(arccosh(lovasz_theta(x))) independence_number(x) >= sqrt(szeged_index(x))/gutman_energy(x) independence_number(x) >= minimum(welsh_powell(x), card_negative_eigenvalues(x)) - number_of_triangles(x) independence_number(x) >= -card_periphery(x) + min_degree(x) - 1 independence_number(x) >= -min_common_neighbors(x) + 1/2*min_degree(x) independence_number(x) >= sqrt(cycle_space_dimension(x)) - number_of_triangles(x) independence_number(x) >= matching_number(x) - sigma_2(x) - 1 independence_number(x) >= floor(arccosh(lovasz_theta(x)))^2 independence_number(x) >= -2*card_center(x) + cvetkovic(x) independence_number(x) >= 1/2*card_negative_eigenvalues(x) - max_common_neighbors(x) independence_number(x) >= -number_of_triangles(x)^average_vertex_temperature(x) + max_degree(x) independence_number(x) >= ceil(order(x)/brooks(x)) independence_number(x) >= ceil(log(lovasz_theta(x)^2)) independence_number(x) >= -(card_negative_eigenvalues(x) - card_positive_eigenvalues(x))*card_zero_eigenvalues(x) independence_number(x) >= floor(tan(floor(gutman_energy(x)))) independence_number(x) >= floor(tan(e^card_positive_eigenvalues(x))) independence_number(x) >= minimum(floor(lovasz_theta(x)), max_even_minus_even_horizontal(x) + 1)

nb11=Graph('I~~Z~nnnw')

nb11.is_regular()

True

#adding counterexample to 1/2 cvetkovic conjecture
#Graph('I~~Z~nnnw')

#investigate lemma: alpha >= diameter for regular graphs
#ROUND 3: adding NB graphs and theoretical knowledge
load("conjecturing.py")
load("gt.sage")

#load the database of precomputed invariant values
load("objects-invariants-properties/gt_precomputed_database.sage")
db = os.environ['HOME'] +'/objects-invariants-properties/gt_precomputed_database.db'
#now get a table out of the precomputed database that can be used by the invariant-relation conjecturing program
precomputed_invs = precomputed_invariants_for_conjecture(database=db)

#note each of the folling theorems *is* either an invariant (and could be precomputed) or
#some just_defined number that's an integer
#so there's no possibility of rounding-error numerical instability

def get_value(invariant, o):
    precomputed_value = None
    o_key = precomputed_invs[1](o)
    i_key = precomputed_invs[2](invariant)
    if precomputed_invs:
        if o_key in precomputed_invs[0]:
            if i_key in precomputed_invs[0][o_key]:
                precomputed_value = precomputed_invs[0][o_key][i_key]
    if precomputed_value is None:
        return invariant(o)
    else:
        return precomputed_value

girth_theta_bound = lambda g: min(g.girth(),floor(get_value(Graph.lovasz_theta,g)))

max_degree_minus_triangles = lambda g: max_degree(g) - number_of_triangles(g)

order_brooks_bound = lambda x: ceil(order(x)/brooks(x))

szekeres_wilf_bound = lambda x: ceil(order(x)/szekeres_wilf(x))

theorems = [Graph.diameter, average_distance, Graph.radius, residue, max_even_minus_even_horizontal, critical_independence_number, max_degree_minus_triangles, order_brooks_bound, szekeres_wilf_bound]

#use get_value so that conjecture program uses precomputed value in theory calculation instead of recomputing (maybe incorrectly)
max_theorem = lambda g: ceil(max(get_value(f, g) for f in theorems))
#for this to work each "theorem" that has a potential numerical error needs to be precomputed and included in the db

#use get_value so that conjecture program uses precomputed value in theory calculation instead of recomputing (maybe incorrectly)
####min_theorem = lambda g: floor(min(get_value(f, g) for f in theorems))
#for this to work each "theorem" that has a potential numerical error needs to be precomputed and included in the db

#there is a problem with a fiedler number computation, removing fiedler (35 in the list) from invariants
#efficiently_computable_invariants.pop(35)
invariants = [independence_number] + efficiently_computable_invariants

nb11=Graph('I~~Z~nnnw')

objects = [g for g in graph_objects if g.is_regular()] + [nb11]

#no results after the default 5 seconds
#so there could be a bug - or no significant conjecture yet - increasing the time *may* help
conjs = conjecture(objects, invariants, invariants.index(independence_number), upperBound = False, theory = [max_theorem], precomputed = precomputed_invs, time = 100)
for c in conjs:
    print c

loaded graph dc1024 loaded graph dc2048 loaded graph properties data file loaded graph invariants data file independence_number(x) >= maximum(max_even_minus_even_horizontal(x), 1/2*lovasz_theta(x)) independence_number(x) >= sqrt(barrus_bound(x)) independence_number(x) >= order(x)/brooks(x) independence_number(x) >= -max_common_neighbors(x) + min_degree(x) independence_number(x) >= -card_periphery(x) + matching_number(x) independence_number(x) >= -1/2*diameter(x) + lovasz_theta(x) independence_number(x) >= 1/2*card_center(x) - 1/2*order_automorphism_group(x) independence_number(x) >= lovasz_theta(x)/vertex_con(x) independence_number(x) >= -diameter(x) + 2*residue(x) independence_number(x) >= matching_number(x) - order_automorphism_group(x) - 1 independence_number(x) >= minimum(cvetkovic(x), inverse_degree(x)) independence_number(x) >= card_positive_eigenvalues(x) - lovasz_theta(x) independence_number(x) >= card_negative_eigenvalues(x) - sigma_2(x) independence_number(x) >= minimum(lovasz_theta(x), tan(order(x))) independence_number(x) >= residue(x) independence_number(x) >= ceil(sqrt(barrus_bound(x))) independence_number(x) >= -card_periphery(x) + 2*diameter(x) independence_number(x) >= matching_number(x) - sigma_2(x) - 1 independence_number(x) >= -10^different_degrees(x) + matching_number(x) independence_number(x) >= card_periphery(x) - maximum(card_center(x), max_even_minus_even_horizontal(x)) independence_number(x) >= floor(arcsinh(lovasz_theta(x)))^2 independence_number(x) >= floor(tan(barrus_bound(x) - 1)) independence_number(x) >= minimum(floor(lovasz_theta(x)), tan(spanning_trees_count(x))) independence_number(x) >= minimum(card_positive_eigenvalues(x), 2*card_zero_eigenvalues(x)) independence_number(x) >= minimum(floor(lovasz_theta(x)), max_even_minus_even_horizontal(x) + 1)

load("gt.sage")

loaded graph dc1024 loaded graph dc2048 loaded graph properties data file loaded graph invariants data file

for g in graph_objects:
    if g.is_regular():
        print independence_number(g), g.diameter(), g.name()

1 1 k3 1 1 k4 1 1 k5 8 5 Dodecahedron 3 3 c8chorded 5 2 Clebsch graph 9 5 c24 11 6 c26 24 9 c60 18 6 c6xc6 10 6 holton_mckay 4 4 sixfour 2 2 c4 4 2 Petersen graph 1 1 p2 19 8 Tutte Graph 4 4 throwing 4 4 throwing2 4 4 throwing3 8 4 Blanusa First Snark Graph 7 4 Blanusa Second Snark Graph 9 4 Flower Snark 3 3 ryan3 1 1 k10 25 9 circulant_50_1_3 4 2 Chvatal graph 10 5 Desargues Graph 9 4 Flower Snark 5 4 Frucht graph 15 2 Hoffman-Singleton graph 2 2 Octahedron 3 2 Thomsen graph 4 2 Petersen graph 9 4 Pappus Graph 27 6 Gray graph 7 3 Heawood graph 12 4 Coxeter Graph 7 3 Brinkmann graph 15 4 Tutte-Coxeter graph 19 8 Tutte Graph 7 3 Robertson Graph 10 4 Folkman Graph 35 6 Balaban 10-cage 9 4 Pappus Graph 5 3 Tietze Graph 12 3 Sylvester Graph 21 7 Szekeres Snark Graph 8 4 Moebius-Kantor Graph 8 8 ryan 3 3 regular_non_trans 43 12 c100 4 2 Shrikhande graph 7 6 sylvester 2 2 c5 3 3 c6 4 4 c9 4 3 ce3 5 2 ce5 3 2 Wagner Graph 5 4 binary_octahedron 2 2 prism 1 1 alpha_critical_A_ 1 1 alpha_critical_Bw 1 1 alpha_critical_C~ 2 2 alpha_critical_Dhc 1 1 alpha_critical_D~{ 1 1 alpha_critical_E~~w 3 3 alpha_critical_FhCKG 1 1 alpha_critical_F~~~w 2 2 alpha_critical_GbMmvG 1 1 alpha_critical_G~~~~{ 4 4 alpha_critical_HhCGGE@ 1 1 alpha_critical_H~~~~~~

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


#add the proven results to theorems to get new conjectures - that simplify investigation
#load the database of precomputed invariant values
load("objects-invariants-properties/gt_precomputed_database.sage")
db = os.environ['HOME'] +'/objects-invariants-properties/gt_precomputed_database.db'
#now get a table out of the precomputed database that can be used by the invariant-relation conjecturing program
precomputed_invs = precomputed_invariants_for_conjecture(database=db)

#note each of the folling theorems *is* either an invariant (and could be precomputed) or
#some just_defined number that's an integer
#so there's no possibility of rounding-error numerical instability

def get_value(invariant, o):
    precomputed_value = None
    o_key = precomputed_invs[1](o)
    i_key = precomputed_invs[2](invariant)
    if precomputed_invs:
        if o_key in precomputed_invs[0]:
            if i_key in precomputed_invs[0][o_key]:
                precomputed_value = precomputed_invs[0][o_key][i_key]
    if precomputed_value is None:
        return invariant(o)
    else:
        return precomputed_value

girth_theta_bound = lambda g: min(g.girth(),floor(get_value(Graph.lovasz_theta,g)))

max_degree_minus_triangles = lambda g: max_degree(g) - number_of_triangles(g)

order_brooks_bound = lambda x: ceil(order(x)/brooks(x))

theorems = [girth_theta_bound, average_distance, Graph.radius, residue, max_even_minus_even_horizontal, critical_independence_number, max_degree_minus_triangles, order_brooks_bound]

#use get_value so that conjecture program uses precomputed value in theory calculation instead of recomputing (maybe incorrectly)
max_theorem = lambda g: ceil(max(get_value(f, g) for f in theorems))
#for this to work each "theorem" that has a potential numerical error needs to be precomputed and included in the db

#there is a problem with a fiedler number computation, removing fiedler (35 in the list) from invariants
#efficiently_computable_invariants.pop(35)
invariants = [independence_number] + efficiently_computable_invariants

nb1=Graph('epCpih@K}gSGIZfc?Rkf{EWtVKJTmJtWYl_IoDOKOikwDSKtbH\\fi_g`affO\\|Agq`WcLoakSLNPaWZ@PQhCh?ylTR\\tIR?WfoJNYJ@B{GiOWMUZX_puFP?')
nb2=Graph('Gvz~r{')
nb3=Graph('eLvnv~yv{yJ~rlB^Mn|v^nz~V]mwVji}^vZf{\\\\nqZLfVBze}y[ym|jevvt~NNucret|~ejj~rz}Q\\~^an}XzTV~t]a]v}nx\\u]n{}~ffqjn`~e}lZvV]t_')
nb4=Graph('ETzw')
nb5=Graph('~?@A~~~~~~z~~~~~~~~^~~~~~z~~~~~~~~~~~~~~~v~~~v~~~~~~~~~~z~~~~~~~~^~~~~~~~~~}\~~}v~^~~}~~^~~~~~~~~~~~~^~~~~~~~~V~~~n~~n~~~~~~}~~|~}~~~~~~~~~~~~~~~~~~~~~vv~|~~~~~~~~~~~~~~~~~z~~w~~~~~~~~~~~~~~~~n~~~|~~~~~~~v~|~~~~~~~~~~}~|~r~V~~~n~~~~~~~~z~~}}~}~~~~vz~~z~~~z}~~~n~~~~~~~~~~~~n~~~~~~~z~~~~~~~~~~~~~~^~~~~~~~~~n~~]~~~~~n~~~}~~~~~~~~~~^~^~~~~}~~~~~~~~~~~z~~~~^~~~~~~w')
nb6=Graph('I~~Lt~\Nw')
nb7=Graph('N^nN~~}Z~|}~~\~]zzw')
nb8=Graph('IOilnemjG')
nb9=Graph('Hx~\\rnV')
nb10=Graph('z@M@E?OYOSCPBTp?mOWaP_?W[OG[abE_?P[@?@REt?ggAAOH?N@?CATE\oE?WO@GOKu?LJ_??SDP@CIA?AFHCC?kZQMo@CkOGoiJSs`?g?oDJqC?S?qJSqA?GN]?OPd?cGHE?AOpE_c_O@kC_?DF@HGgJ?ygAACdcCMPA[d`SHE@?PqRE?CO_?CWO?H_b_EBoOKI@CWAadQ?eOO?oT_@STAWCCCMOK?A@?TsBoJa@?PGQ_CiKPC_@_iE_hL@ACAIJQDgOSG?G[cG_D[A_CbDKO[goBH_?S?')
nb11=Graph('I~~Z~nnnw')
ce93 = Graph('_t???CA???_B?E?@??WAB?G??_GA?W?????@???W??B???A???BA??@__???G??@A???LA???AW???@_???G')
ce93.name(new = "ce93")

objects = graph_objects + [nb1,nb2,nb3,nb4,nb5,nb6,nb7,nb8,nb9,nb10,nb11,ce93]

#no results after the default 5 seconds
#so there could be a bug - or no significant conjecture yet - increasing the time *may* help
conjs = conjecture(objects, invariants, invariants.index(independence_number), upperBound = False, theory = [max_theorem], precomputed = precomputed_invs, time = 100)
for c in conjs:
    print c

couldn't load dc1024_g6string.sobj couldn't load dc2048_g6string.sobj can't load graph properties sobj file can't load graph invariant sobj file independence_number(x) >= (barrus_bound(x) - 1)/card_periphery(x) independence_number(x) >= minimum(diameter(x), card_periphery(x)) independence_number(x) >= diameter(x) - different_degrees(x) independence_number(x) >= order(x)/brooks(x) independence_number(x) >= order(x)/szekeres_wilf(x) independence_number(x) >= minimum(floor(lovasz_theta(x)), tan(spanning_trees_count(x))) independence_number(x) >= maximum(max_even_minus_even_horizontal(x), 1/2*lovasz_theta(x)) independence_number(x) >= -card_center(x) + floor(lovasz_theta(x)) independence_number(x) >= maximum(critical_independence_number(x), 1/2*lovasz_theta(x)) independence_number(x) >= -10^max_common_neighbors(x) + matching_number(x) independence_number(x) >= cos(spanning_trees_count(x))*floor(lovasz_theta(x)) independence_number(x) >= welsh_powell(x)/card_periphery(x) independence_number(x) >= (residue(x) - 1)^min_common_neighbors(x) independence_number(x) >= -max_common_neighbors(x) + min_degree(x) - 1 independence_number(x) >= -brinkmann_steffen(x) + card_negative_eigenvalues(x) independence_number(x) >= minimum(welsh_powell(x), card_negative_eigenvalues(x)) - number_of_triangles(x) independence_number(x) >= maximum(residue(x), 1/2*lovasz_theta(x)) independence_number(x) >= minimum(matching_number(x), diameter(x) - 1) independence_number(x) >= minimum(fractional_alpha(x), diameter(x) - 1) independence_number(x) >= floor(tan(barrus_bound(x) - 1)) independence_number(x) >= minimum(lovasz_theta(x), tan(order(x))) independence_number(x) >= floor(lovasz_theta(x))/vertex_con(x) independence_number(x) >= sqrt(szeged_index(x))/gutman_energy(x) independence_number(x) >= 2*floor(arccosh(lovasz_theta(x))) independence_number(x) >= floor(tan(floor(gutman_energy(x)))) independence_number(x) >= -card_periphery(x) + min_degree(x) - 1 independence_number(x) >= -min_common_neighbors(x) + 1/2*min_degree(x) independence_number(x) >= sqrt(cycle_space_dimension(x)) - number_of_triangles(x) independence_number(x) >= matching_number(x) - sigma_2(x) - 1 independence_number(x) >= floor(arccosh(lovasz_theta(x)))^2 independence_number(x) >= 2*fractional_alpha(x)/szekeres_wilf(x) independence_number(x) >= ceil(order(x)/brooks(x)) independence_number(x) >= 1/2*card_negative_eigenvalues(x) - max_common_neighbors(x) independence_number(x) >= -number_of_triangles(x)^average_vertex_temperature(x) + max_degree(x) independence_number(x) >= -2*card_center(x) + cvetkovic(x) independence_number(x) >= ceil(log(lovasz_theta(x)^2)) independence_number(x) >= -(card_negative_eigenvalues(x) - card_positive_eigenvalues(x))*card_zero_eigenvalues(x) independence_number(x) >= floor(tan(e^card_positive_eigenvalues(x))) independence_number(x) >= floor(tan(log(barrus_bound(x))/log(10))) independence_number(x) >= minimum(floor(lovasz_theta(x)), max_even_minus_even_horizontal(x) + 1)

ce93 = Graph('_t???CA???_B?E?@??WAB?G??_GA?W?????@???W??B???A???BA??@__???G??@A???LA???AW???@_???G')
ce93.name(new = "ce93")
ce93.order()

32

conjs[2]

independence_number(x) >= diameter(x) - different_degrees(x)

conjs[2](ce93)

True

#a * b = |a|*|b|*cos(angle)
cos(pi/3)

1/2

c=1/sqrt(5)

A=matrix(5,7,[1,1,0,0,0,1,c,1,0,1,1,0,0,c,0,1,0,0,1,0,c,1,0,1,0,0,1,c,0,0,0,1,1,0,c])

A

[ 1 1 0 0 0 1 1/5*sqrt(5)] [ 1 0 1 1 0 0 1/5*sqrt(5)] [ 0 1 0 0 1 0 1/5*sqrt(5)] [ 1 0 1 0 0 1 1/5*sqrt(5)] [ 0 0 0 1 1 0 1/5*sqrt(5)]

A.rref()

[ 1 0 0 0 0 2 1/5*sqrt(5)] [ 0 1 0 0 0 -1 0] [ 0 0 1 0 0 -1 0] [ 0 0 0 1 0 -1 0] [ 0 0 0 0 1 1 1/5*sqrt(5)]

A2=matrix(6,7,[1,1,0,0,0,1,c,1,0,1,1,0,0,c,0,1,0,0,1,0,c,1,0,1,0,0,1,c,0,0,0,1,1,0,c,1,1,1,1,1,1,1])

A2.rref()

[ 1 0 0 0 0 0 sqrt(5) - 2] [ 0 1 0 0 0 0 -2/5*sqrt(5) + 1] [ 0 0 1 0 0 0 -2/5*sqrt(5) + 1] [ 0 0 0 1 0 0 -2/5*sqrt(5) + 1] [ 0 0 0 0 1 0 3/5*sqrt(5) - 1] [ 0 0 0 0 0 1 -2/5*sqrt(5) + 1]

A3=matrix(RR,6,6,[1,1,0,0,0,1,1,0,1,1,0,0,0,1,0,0,1,0,1,0,1,0,0,1,0,0,0,1,1,0,1,1,1,1,1,1])

b=matrix(RR,6,1,[c,c,c,c,c,1])

A3.solve_right(b)

[0.236067977499790] [0.105572809000084] [0.105572809000084] [0.105572809000084] [0.341640786499874] [0.105572809000084]