lower-bound-conjecture-run-1-with-data-and-theory.sagews

#load concecturing program
load("conjecturing.py")

#load all pre-defined graphs and invariants
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
theorems = [Graph.radius, residue, max_even_minus_even_horizontal]

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

#the get_value function keeps the theory from re-computing (possible wrongly) values of invariants that are correctly computed in the db
max_theorem = lambda g: ceil(max(get_value(f,g) for f in theorems))

objects = graph_objects

invariants = efficiently_computable_invariants + [independence_number]

#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) >= critical_independence_number(x) independence_number(x) >= max_degree(x) - number_of_triangles(x) independence_number(x) >= 1/2*cvetkovic(x) independence_number(x) >= minimum(diameter(x), lovasz_theta(x)) independence_number(x) >= sqrt(card_positive_eigenvalues(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) >= matching_number(x) - order_automorphism_group(x) - 1 independence_number(x) >= min_degree(x) - number_of_triangles(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) >= -average_distance(x) + ceil(lovasz_theta(x)) independence_number(x) >= minimum(girth(x), floor(lovasz_theta(x))) independence_number(x) >= lovasz_theta(x)/edge_con(x) independence_number(x) >= matching_number(x) - sigma_2(x) - 1 independence_number(x) >= maximum(residue(x), critical_independence_number(x)) independence_number(x) >= -10^different_degrees(x) + matching_number(x) independence_number(x) >= card_negative_eigenvalues(x) - sigma_2(x) independence_number(x) >= maximum(max_even_minus_even_horizontal(x), critical_independence_number(x)) independence_number(x) >= floor(lovasz_theta(x))/vertex_con(x) independence_number(x) >= minimum(max_degree(x), floor(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) >= floor(tan(barrus_bound(x) - 1)) 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)

#ROUND 2: adding more known theory

#load concecturing program
load("conjecturing.py")

#load all pre-defined graphs and invariants
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
max_degree_minus_dmax_degree(x) - number_of_triangles(x)
theorems = [Graph.radius, residue, max_even_minus_even_horizontal, critical_independence_number]

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

#the get_value function keeps the theory from re-computing (possible wrongly) values of invariants that are correctly computed in the db
max_theorem = lambda g: ceil(max(get_value(f,g) for f in theorems))

objects = graph_objects

invariants = efficiently_computable_invariants + [independence_number]

#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