View the Project on GitHub nvcleemp/conjecturing
The code in this repository is described in the following papers:
Examples of how the program can be used are given in:
Warning: in recent versions of Sage this approach to install conjecturing appears to be broken. We are looking into the issue, but as long as this is not fixed, you can best use conjecturing without installation.
First you need to locate the Sage installation into which you want to install conjecturing. In case this is the system installation of Sage, you can find the location using the command which sage.
$ sage --package fix-checksum conjecturing$ sage -i conjecturingOne easy way to work with Sage is by going to http://www.cocalc.com. Of course you can use our code on CoCalc. By default, however, it is not possible to install additional packages there, so we created a separate release of the conjecturing package which can easily be used on CoCalc.
~$ unzip conjecturing-0.13-CoCalc
~$ cd conjecturing-0.13-CoCalc
~/conjecturing-0.13-CoCalc$ make
expressions and conjecturing.py.You can check that the installation was successful by creating a worksheet, copying the code below and executing it. If everything went OK, you should see some conjectures.
load('conjecturing.py')
def max_degree(g):
return max(g.degree())
invariants = [Graph.size, Graph.order, max_degree]
objects = [graphs.CompleteGraph(n) for n in [3,4,5]]
conjecture(objects, invariants, 0)
To update to a newer version, you just repeat the steps above for the newer zip file.
You might want to use our code without going through the hassle of installing it within Sage. This might be the case if you do not have the correct priviliges to install conjecturing, or if you are using the Sage version from your distribution and you don't want to make changes to it. It is possible to do this, although it brings some limitations with it.
make command.expressions and conjecturing.py that were copied into your home directory.In case you use this setup, you will only be able to use conjecturing if Sage is started from your home directory. You can move the files expressions and conjecturing.py to another location, but then conjecturing will only work if Sage is started from that location.
To update to a newer version, you just repeat the steps above for the newer zip file.
See the directory spkg for instructions on how to build and install a Sage package containing the expressions program.
Once you have built and installed such a Sage package, you can use the Python files in the directory sage to interact
with the package.
Open the directory sage in a terminal window and start Sage. Usually this is done using the following command:
$ sage
Once Sage has started, you can load the file conjecturing.py:
sage: attach('conjecturing.py')
You can also choose to load any of the other files, but this is not necessary.
An example run might look like this:
sage: attach('conjecturing.py')
sage: attach('numbertheory.py')
sage: objects = [5, 10]
sage: conjecture(objects, invariants, 1)
Note that loading the file numbertheory.py sets the variable invariants to a list of invariants used in number theory.
The repository contains four directory:
c: this directory contains the code for the program expressions which is used to generate the expressions and conjectures. This program can also be used as a stand-alone program.spkg: this directory contains the scripts needed to install the C program as a package in Sage.sage: this directory contains the Python scripts which integrate the C program into Sage.examples: this directory contains several examples of how the code in this repository can be used.Once you have installed the Sage Package (either by downloading and installing it, or by building it yourself and then installing it), you can load the files in the directory sage to make conjectures within Sage. The most important file is conjecturing.py. This loads the code needed to make conjectures. The remaining files just provide utility methods to make conjectures for graph theory, matrix theory and number theory.
Simply start Sage from the directory sage and once Sage is started, give the following command:
sage: load('conjecturing.py')
This is all you need to do. From now on you can use the method conjecture to make conjectures. This method needs three arguments, and can take several additional optional arguments. The arguments that need to be provided are:
objects: the objects on which the conjectures will be based.invariants: the invariants that can appear in the conjectures.mainInvariant: the main invariant that will appear on the left-hand-side of the comparator.These three are sufficient to make conjectures:
sage: def max_degree(g):
....: return max(g.degree())
....:
sage: invariants = [Graph.size, Graph.order, max_degree]
sage: objects = [graphs.CompleteGraph(n) for n in [3,4,5]]
sage: conjecture(objects, invariants, 0)
[size(x) <= 2*order(x),
size(x) <= max degree(x)^2 - 1,
size(x) <= 1/2*order(x)*max degree(x)]
You can also make property-based conjectures:
sage: properties = [is_prime, is_even]
sage: objects = [3]
sage: propertyBasedConjecture(objects, properties, 0)
[(~(is_even))->(is_prime)]
The methods provide more detailed information together with several examples. You can access this information by running the following commands:
sage: help(conjecture)
sage: help(propertyBasedConjecture)or
sage: conjecture?
sage: propertyBasedConjecture?Each of the examples in the directory examples specify which files need to be loaded for the example to work. The examples are referred to from the paper. Most of the examples come in two versions: a short and a long version. The short version immediately should give the conjectures as they appear in the paper. Since in most cases the conjecturing is halted by the time limit, in some cases there might be a small discrepancy between the conjectures in the paper and the conjectures you get. The long version repeats the steps we took to produce the conjectures, i.e., start with a small set, generate conjectures, look for counterexamples, add them to the objects, generate conjectures, ... Note that these long versions sometimes take very long (some need multiple days!).
For example, to run the first example of goldbach conjectures, you proceed as follows. Start Sage in the directory examples. Execute the following commands:
sage: load('../sage/conjecturing.py')
sage: load('../sage/numbertheory.py')
sage: load('goldbach_conjectures1.py')
The conjectures are stored in the variable conjectures.
sage: conjectures
[goldbach(x) >= (1/digits10(x)), goldbach(x) >= digits10(x) - 1]
If you want to run the long version, then you load the file which has -long appended to the name:
sage: load('../sage/conjecturing.py')
sage: load('../sage/numbertheory.py')
sage: load('goldbach_conjectures1-long.py')
Starting with these objects:
4
Available invariants:
goldbach
prime_pi
euler_phi
number
digits10
digits2
sigma
count_divisors
next_prime
previous_prime
count_quadratic_residues
mertens
li
zeta
reciprocal_prime_sum
max_prime_divisor
prime_product
Found the following conjectures:
goldbach(x) >= digits10(x)
Step 1: Adding 12
Found the following conjectures:
goldbach(x) >= (1/digits10(x))
goldbach(x) >= digits10(x) - 1
No counterexample found
The conjectures are stored in the variable conjectures.
sage: conjectures
[goldbach(x) >= (1/digits10(x)), goldbach(x) >= digits10(x) - 1]
Note that this will take quite long to verify these two conjectures for all values it checks.
Building the C program is simple: just execute the command make in the directory c. This will build the program expressions. A detailed usage message for expressions can be obtained by executing the following command:
$ ./expressions -h
In the Sage code this program is used to generate the conjectures, but it can also be used to generate the intermediate structures.
To generate rooted binary trees with a 0 binary nodes (i.e., with two children) and with 1 unary node (i.e., with one child), you can use the following command:
$ ./expressions -u 1 0
Found 1 unlabeled trees.
To generate labeled rooted binary trees, you also have to specify the number of invariants (i.e., labels for the leaves):
$ ./expressions -l 1 0 2
Found 1 unlabeled trees.
Found 10 labeled trees.
To generate valid expressions, you need to input the values of invariants for all objects. Assume that the content of the file values.txt is this:
3 4 2
3
3
2
2
5
5
2
2
5
10
4
4
The first line tells us that there are 3 objects, 4 invariants and that the second invariant is the main invariant. This corresponds to the following situation:
Invariant 1 Invariant 2 Invariant 3 Invariant 4
object 1) 3.000000 3.000000 2.000000 2.000000
object 2) 5.000000 5.000000 2.000000 2.000000
object 3) 5.000000 10.000000 4.000000 4.000000
Now you can generate all valid expressions with one unary operator as follows:
$ ./expressions -e 1 0 --all-operators --print-valid-expressions < values.txt
I2 <= (I1) * 2
I2 <= (I1) ^ 2
Found 1 unlabeled trees.
Found 30 labeled trees.
Found 2 valid expressions.
Finally you can also generate conjectures using the same file:
$ ./expressions -c --all-operators --dalmatian < values.txt
Generation process was stopped by the conjecturing heuristic.
Found 5 unlabeled trees.
Found 410 labeled trees.
Found 53 valid expressions.
I2 <= (I1) * 2
I2 <= ((I1) / 2) * (I3)
I2 <= ((I3) ^ 2) + 1