Technische Universität München, Fakultät für Informatik
Lehrstuhl Informatik IV, Research Group Automated Reasoning

Grounding near-propositional CNF formulae

This page points to sources for the eground version used for the experiments in my paper A Comparison of Different Techniques for Grounding Near-Propositional CNF Formulae. It also has the full experimental data and some remarks on our later work on this topic.

The program

The grounding procedure, eground, is available as part of the distribution of the equational theorem prover E. Since the deadline for the paper did not correlate with any planned full release, the program is based on an intermediate version. Follow the normal installation instructions in the README file to build all programs. You will find eground as CLIB/PROVER/eground in the installation directory. Note that for serious work I suggest that you download the latest version of E, and use the corresponding version of eground. This version has been significantly enhanced, and also been used to build GrAnDe, a decision procedure for near-propositional CNF formulae.

The problems

All test problems were taken from TPTP-2.4.1, and were translated for eground with tptp2X -f tptp. Here are the 4 problems discussed individually in the paper:

The results

We performed more experiments than we could include into the paper. For each experiment, we give a short description of the strategy. The exact command line can be found as a comment at the beginning of the result files. For help with the options, run eground -h.

Results are presented line by line, lines starting with a # are comments, and the format of non-comment lines is as follows:

Name    Status    Time   Reason    Clauses    Literals

Results referenced in the paper

Other results

All results have been measured with a memory limit of 128 MB on a Sun Ultra 10/300.
Stephan Schulz,, 29.10.2001