SAT-Inspired Eliminations for Superposition
收藏资源简介：
This archive contains the problems, raw evaluation results and scripts for<br> running the experiments described in the paper "SAT-Inspired Inprocessing for<br> Superposition" by Petar Vukmirovic, Jasmin Blanchette, and Marijn J.H. Heule<br> available at https://matryoshka-project.github.io/pubs/satelimsup_paper.pdf The problems we used are stored in the "problems/" subdirectory, together with<br> the required axioms (directory "Axioms"). They are separated in two groups,<br> "Theorems" and "Satisfiable", as in the paper. In the "results/" directory, there are 6 files with names of the form<br> "fD.csv", where D is a digit from 1 to 6. The digit corresponds to the<br> figure from the paper, and the corresponding file contains experiment results<br> for the figure labeled D. The columns give information about the results of the<br> experiment run for a given prover configuration (e.g., CPU time, reported<br> status, memory usage). Each row corresponds to one problem file, whose name is<br> given in the "prob_name" column. The "i_solver" column corresponds to a prover. The "i_configuration" column<br> corresponds to a configuration, where i is a natural number identifying a<br> prover-configuration combination. Files named "fDsummary.csv" contain concise summaries of evaluation runs<br> for a corresponding "fD.csv" file. Their columns are of the form<br> "{solver}_{configuration}", and rows contain different statistics described in<br> the "summary" column. The names of the configurations are self-explanatory and correspond to the ones<br> used in the paper. For BCE, SPE, and PPE, if the configuration has no<br> "inprocessing" in the name, the corresponding technique is used as<br> preprocessing. The "zipperposition/" directory contains the scripts that execute the provided<br> Zipperposition binary (compiled only for Linux) on a given problem using a<br> given configuration. To run Zipperposition on a single problem using some<br> configuration, you can use scripts with the name "run_*.sh", where * stands for<br> the configuration used in the evaluation. The configuration names match the<br> ones described in the files "fD.csv". The scripts take two arguments: (1) the path to the TPTP problem and (2) the<br> CPU timeout. For example, to run problem with the path "~/puzzling.p" using the<br> configuration "bce", execute ./run_bce.sh ~/puzzling.p 240 A working installation of python3 and bash is required. The source code for Zipperposition can be obtained from the<br> "wip-hlbe-unit-eqs-checkpoint" branch of the Zipperposition git repository:<br> git@github.com:sneeuwballen/zipperposition.git. The binary stored in "zipperposition/"<br> corresponds to compiled sources tagged with the commit hash<br> 41b3398647e243c8bf6911b3ee4ed4928b4e445d. Compilation instructions are as in<br> the "README.md" file contained in the git repository.
