SAT-Inspired Eliminations for Superposition

This archive contains the problems, raw evaluation results and scripts for running the experiments described in the paper "SAT-Inspired Inprocessing for Superposition" by Petar Vukmirovic, Jasmin Blanchette, and Marijn J.H. Heule available at https://matryoshka-project.github.io/pubs/satelimsup_paper.pdf The problems we used are stored in the "problems/" subdirectory, together with the required axioms. They are separated in two groups, "Theorems" and "SatisfiableOrOpen", as in the paper. In the "results/" directory, there are 5 files with names of the form "figD[a|b].csv", where D is a digit from 1 to 5. The digit corresponds to the figure from the paper, and the corresponding file contains experiment results for the figure labeled D. The columns give information about the results of the experiment run for a given prover configuration (e.g., CPU time, reported status, memory usage). Each row corresponds to one problem file, whose name is given in the "prob_name" column. The "i_solver" column corresponds to a prover. The "i_configuration" column corresponds to a configuration, where i is a natural number identifying a prover-configuration combination. Files named "fD[a|b]summary.csv" contain concise summaries of evaluation runs for a corresponding "fD[a|b].csv" file. Their columns are of the form "{solver}_{configuration}", and rows contain different statistics described in the "summary" column. The names of the configurations are self-explanatory and correspond to the ones used in the paper. For BCE, SPE, and PPE, if the configuration has no "inprocessing" in the name, the corresponding technique is used as preprocessing. The "zipperposition/" directory contains the scripts that execute the 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, you can use scripts with the name "run_*.sh", where * stands for the configuration used in the evaluation. The configuration names match the ones described in the files "fD[a|b].csv". The scripts take two arguments: (1) the path to the TPTP problem and (2) the CPU timeout. For example, to run problem with the path "~/puzzling.p" using the 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 "wip-pred-elim-hlt-congruence" branch of the Zipperposition git repository: git@github.com:sneeuwballen/zipperposition.git. The binary stored in "scripts/" corresponds to compiled sources tagged with the commit hash c21457e0f0578a728a3779033bce28066bd85a2a. Compilation instructions are as in the "README.md" file contained in the git repository. Disclosure: Shortly before the CADE submission deadline, we noticed that there is a bug with HLBE implementation that caused Zipperposition to wrongly reach saturation on some unsatisfiable problems. This issue is now resolved in the git repository (starting with 22194f27327568fc5183ff63f70d7fb6e362f7e3). Due to lack of time, we could not redo the evaluation. For the evaluation on theorems, the issue affected Zipperposition negatively for all HLBE-enabled modes, and we expect to obtain better results with the new version. For the evaluation on satisfiable or unknown problems HLBE was disabled, so the results are not affected