Posts tagged srp

Summer Project

A Radial Layout

My first approach at generating a radial layout of the graph data logged by the theorem prover.

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 30,000 expected.

Data, Data, Everywhere

The amount of data produced by the problems may pose a problem. LCL005 produces more than 600MB of output and generates over 6,000,000 events. Processing this data into a graph description is the next phase of the project.

Graphviz, Dot, Large Graphs and Crashing!

Running Graphviz on my generated dot files exhausts memory and dies. I'll need to either use a smaller problem, or another visualisation tool.

Graphviz, Dot and Large Graphs

Notes on my graph visualisation project.