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. They are separated in two groups, "Theorems" and<br> "SatisfiableOrOpen", as in the paper. In the "results/" directory, there are 5 files with names of the form<br> "figD[a|b].csv", where D is a digit from 1 to 5. 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 "fD[a|b]summary.csv" contain concise summaries of evaluation runs<br> for a corresponding "fD[a|b].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[a|b].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-pred-elim-hlt-congruence" branch of the Zipperposition git repository:<br> [e-mail]:sneeuwballen/zipperposition.git. The binary stored in "scripts/"<br> corresponds to compiled sources tagged with the commit hash<br> c21457e0f0578a728a3779033bce28066bd85a2a. Compilation instructions are as in<br> the "README.md" file contained in the git repository. Disclosure: Shortly before the CADE submission deadline, we noticed that there<br> is a bug with HLBE implementation that caused Zipperposition to wrongly reach<br> saturation on some unsatisfiable problems. This issue is now resolved in the<br> git repository (starting with 22194f27327568fc5183ff63f70d7fb6e362f7e3). Due to<br> lack of time, we could not redo the evaluation. For the evaluation on theorems,<br> the issue affected Zipperposition negatively for all HLBE-enabled modes, and we<br> expect to obtain better results with the new version. For the evaluation on<br> satisfiable or unknown problems HLBE was disabled, so the results are not<br> affected.