Conjecturing

View the Project on GitHub nvcleemp/conjecturing

Quickstart

Layout of the repository

Usage

C program

Installing in Sage

Making conjectures in Sage

Running the examples

Conjecturing on SageMathCloud ™

Conjecturing for Sage

This repository contains the code described in the paper C. E. Larson and N. Van Cleemput, Automated Conjecturing I: Fajtlowicz's Dalmatian Heuristic Revisited, Artificial Intelligence 231 (2016) 17-38.

Quickstart

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.

Layout of the repository

The repository contains four directory:

Usage

C program

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

Installing in Sage

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.

Making conjectures in Sage

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:

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?

Running the examples

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.

Conjecturing on SageMathCloud ™

One easy way to work with Sage is by going to http://cloud.sagemath.com. Of course you can use our code on SageMathCloud ™. 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 SMC.

~$ unzip conjecturing-0.11.1-SMC
~$ cd conjecturing-0.11.1-SMC
~/conjecturing-0.11.1-SMC$ make

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.