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
- Name is the name of the problem as generated by
tptp2X.
- Status is either S for success or F for
failure.
- Time is the CPU time until termination in seconds.
- Reason is the reason for termination. In this case, it
is either success for success, or maxmem for running
out of memory.
- Clauses is the number of clauses in the generated ground
formula (or 0 in the case of failure).
- Literals is the number of literals in the generated
formula.
Results referenced in the paper
- Naive grounding (no special refinements)
- Conventional (only standard contraction)
- Constraints (uses structural constraints)
- Splitting (uses clause splitting)
- Combined (uses all three techniques)
Other results
All results have been measured with a memory limit of 128 MB on a Sun
Ultra 10/300.
Stephan
Schulz,schulz@informatik.tu-muenchen.de, 29.10.2001