Verbosity: Not always a bad thing!

It appears that we need to set very_verbose to get the prover to output clauses generated by factorisation, etc. Without this, we get only 5 clauses from LCL403 instead of the nearly 30000 expected.

Playing with the dumps from SET012, it becomes apparent that using clustered subgraphs may be useful. When a large inter-rank gap is used with clustered subgraphs for iterations, the resultant plot is almost understandable. Further experiments to try include:

• creating edges between a given clause and its cluster of children (rather than a given clause and every child);
• collapsing nodes introduced by 'factor' into their parents; and
• correctly ordering the iteration clusters with respect to each other.
  

Creating "given" edges to clusters (instead of to all children) appears to be of some value. Perhaps it might be interesting to represent this differently in an animation: e.g. highlighting the current "given clause" during those frames that comprise an iteration.

Data, Data, Everywhere

The amount of data produced by the problems may pose a problem. LCL005 for example, produces more than 600M of output and generates over 6,000,000 events.

Processing this data into a graph description is the next phase of the project. Some fairly trivial (and very naive) shell scripts have been created to split these files into a list of events for each iteration of the given clause loop. These are however, excruciatingly slow and will need to be rewritten in something a little faster. A few more scripts were created to produce some event statistics and plot them using Gnuplot. These also will need to be re-written in a language that has decent text processing facilities (so as to remove the need to call three cat|grep's per file). Awk may be a good choice.

I seem to be missing some proportion of KEPT clauses. A trace of LCL403 for instance does not list any KEPT clauses (except for those that form part of the theory) whereas the statistics say that 29208 clauses were kept. Most confusing.

Graphviz, Dot, Large Graphs and Crashing!

I came in this morning to discover that the Graphviz run with LCL005 consumed some nine and one quarter hours of real time and was killed, I can only assume, due to memory usage. Hacked up a simple C program to replace the shell script in converting "^clause" lines from runtime_data.dump to 'dot'. It removes duplicate parents, outputs them in ascending id order, etc. It's also a lot quicker than the shell script.

One of the smaller problems (SET012) ran in a rather short amount of time, and generated a graph that renders to 19616x809px in PNG. It will probably be a good idea to keep working with this problem due to its smaller graph. GRP024 also runs much quicker than LCL005 (though it still takes quite a lot longer than SET012).

Approaches may be:

• Assign explicit ranks based on the iteration the clause was generated in then try to find a radial layout filter;
• Have a style=invis central node, with edges to every other node, where each edge is weighted inversely proportionally to the iteration the clause was generated in (higher weights tend to shorter and straighter).

Explicitly setting node ranks to the iteration number seems "cleaner" to me. Another alternative is to "declare" all nodes to be in clusters, then define the edges between them. It would then be possible to use the cluster ranking options to let Graphviz have more control over the layout.

Another problem is that the prover does not appear to be able to provide enough information for my purposes. It does not appear to expose individual events (clause creation and deletion) or any information on clauses beyond the clause selected as "given" during each iteration.

Later:

I have added some code to the prover (and a flag to control it) that will output deleted clauses, though it does not (for reasons I have yet to determine) print a clauses ID. Once this problem is solved and the output is amended to output reasons for deletions, it should be possible to generate a data model for an animation, even if the animation itself is not yet possible.

Later still:

It looks like proc_gen() is breaking clauses before we get them. For example, the parents of a clause are printed (very_verbose), followed by a message "Subsumed by ?", then out "** DELETED" message no longer has access to the clauses parents. The problem was caused by using a copy of the clause that was made before being passed to proc_gen() which has the side affect, apparently, of adding the parents list to the clause structure.

Even Later:

A trace of proving the theorem SET012 with the appropriate options enabled (print_kept, print_deleted, etc) is 2.3M in total, of which all but 32K is useful event data.

Graphviz, Dot and Large Graphs.

Today I started looking at transforming the data dumped by the theorem prover into 'dot', the language used by Graphviz (and a number of other packages). A quick and extremely dirty script translated the data into 'dot' and I, foolishly as it turns out, started a test run going of LCL005, to see just how big a graph it is. When I went home for the day, it was still running.

I need to find an easy way to determine the iteration in which clauses are generated so that I can play silly buggers with weighted edges, explicit rankings, etc.