Description
This archive contains the raw evaluation results and scripts for running the
experiments described in the article Superposition with First-Class Booleans
and Inprocessing Clausification and the associated technical report.
Zipperposition is available at https://github.com/sneeuwballen/zipperposition. The configurations used in the evaluation are explained below and in the archive.
The problems are stored in problems/ directory and divided in four
subdirectories, one for each category of the problem. Subdirectory Axioms/ holds
the axioms shared by TPTP problems. The subdirectory tptp-ho/ corresponds to
the benchmark set "TPTP Bool" of the paper.
The results/ directory has subdirectories of the same name as the problems/
directory, each containting res.csv file with the raw evaluation results for the
given problem category.
The result files are organized as follows: The columns give information about
the results of the experiment run for a given prover configuration (e.g., CPU
time, reported status, memory usage, etc.). Each row corresponds to one problem
file, whose name is given in the "prob_name" column.
The "i_solver" column corresponds to a prover, whereas the "i_configuration"
column corresponds to a configuration, where i is a natural number identifying a
prover-configuration combination.
Files ending with "summary.csv" contain concise summaries of evaluation runs for
a corresponding results file. Columns of these files are of the form
"{solver}_{configuration}", and rows contain different statistics described in
the "summary" column.
Names of the solvers and configurations are self-explanatory, and follow the
nomenclature from the paper. Additionally, for Sledgehammer category of
benchmarks, there is additional set of configurations with names ending with
_tptp. Those configurations are the same as regular ones, but fix the input
syntax to TPTP. This is necessary since Sledgehammer files have no extensions.
In the zipperposition/ directory you can find the scripts that run provided
Zipperposition binary (compiled only for Linux) on a given problem using a given
configuration. To run Zipperposition on a single problem using some
configuration use scripts with the name run_*.sh where * stands for the
configuration used in the evaluation. Configuration names match the ones used in
the result files.
All scripts accept two arguments: 1) path to the problem 2) CPU timeout. For
example, to run problem with the path ~/problem.p using base configuration with
the time limit of 240 s execute
./run_base.sh ~/problem.p 240
Working installation of python3 and bash is required.
Source code for Zipperposition can be obtained from the wip-bool-calculi branch
of Zipperposition git repository:
[email protected]:sneeuwballen/zipperposition.git. The binary stored under scripts/
directory corresponds to compiled sources tagged with commit hash
b81ca9905c774212819afc004a6a17297fc070b6. Compilation instructions are as in
README.md file contained in the git repository.
experiments described in the article Superposition with First-Class Booleans
and Inprocessing Clausification and the associated technical report.
Zipperposition is available at https://github.com/sneeuwballen/zipperposition. The configurations used in the evaluation are explained below and in the archive.
The problems are stored in problems/ directory and divided in four
subdirectories, one for each category of the problem. Subdirectory Axioms/ holds
the axioms shared by TPTP problems. The subdirectory tptp-ho/ corresponds to
the benchmark set "TPTP Bool" of the paper.
The results/ directory has subdirectories of the same name as the problems/
directory, each containting res.csv file with the raw evaluation results for the
given problem category.
The result files are organized as follows: The columns give information about
the results of the experiment run for a given prover configuration (e.g., CPU
time, reported status, memory usage, etc.). Each row corresponds to one problem
file, whose name is given in the "prob_name" column.
The "i_solver" column corresponds to a prover, whereas the "i_configuration"
column corresponds to a configuration, where i is a natural number identifying a
prover-configuration combination.
Files ending with "summary.csv" contain concise summaries of evaluation runs for
a corresponding results file. Columns of these files are of the form
"{solver}_{configuration}", and rows contain different statistics described in
the "summary" column.
Names of the solvers and configurations are self-explanatory, and follow the
nomenclature from the paper. Additionally, for Sledgehammer category of
benchmarks, there is additional set of configurations with names ending with
_tptp. Those configurations are the same as regular ones, but fix the input
syntax to TPTP. This is necessary since Sledgehammer files have no extensions.
In the zipperposition/ directory you can find the scripts that run provided
Zipperposition binary (compiled only for Linux) on a given problem using a given
configuration. To run Zipperposition on a single problem using some
configuration use scripts with the name run_*.sh where * stands for the
configuration used in the evaluation. Configuration names match the ones used in
the result files.
All scripts accept two arguments: 1) path to the problem 2) CPU timeout. For
example, to run problem with the path ~/problem.p using base configuration with
the time limit of 240 s execute
./run_base.sh ~/problem.p 240
Working installation of python3 and bash is required.
Source code for Zipperposition can be obtained from the wip-bool-calculi branch
of Zipperposition git repository:
[email protected]:sneeuwballen/zipperposition.git. The binary stored under scripts/
directory corresponds to compiled sources tagged with commit hash
b81ca9905c774212819afc004a6a17297fc070b6. Compilation instructions are as in
README.md file contained in the git repository.
| Date made available | 2021 |
|---|---|
| Publisher | Zenodo |