Artifact for ParaProofa: A Certifying Parallel Cube-and-Conquer QBF-Solving Framework

ParaProofa: A Certifying Parallel Cube-and-Conquer QBF-Solving Framework Introduction This artifact contains all sources and test-data used in the evaluation of ParaProofa, a certifying parallel Cube-and-Conquer QBF-solving framework, to the end of making them publicly available. In the following we will describe the content of the artifact and how to set up ParaProofa. Disclaimer: The content of this artifact provides everything necessary to reproduce the experiments in the paper. However, the resource requirements of ParaProofa can not usually be met by a common work station. To reproduce the experiments in a feasible way, a cluster or distributed architecture where resource allocation can be managed is required. The experiments in this artifact are running one instance at a time and are meant to give an intuition as well as demonstrating the set-up of the framework. Version Log New in Version 2: Fixed bug in DepQBF messing with the order reductions of initial clauses are written Added more scripts and the original experiment data Contents The artifact is packaged in a docker container with the following contents:/|-- certified-paraqooba|-- depqbf-adv|-- experiments|-- gallery22|-- gallery23|-- iqrpc|-- original|-- output|-- runlim|-- scripts|-- simsala|-- zeek-iqrp-check Source files for ParaProofa certified-paraqooba: The source files for the modified ParaQooba version able to emit certificates. depqbf-adv: The source files for the modified DepQBF version. This is used in ParaQooba as sub-proof solver as well as for the DepQBF runs. iqrpc: The source files for iQRPcheck. zeek-iqrp-check: The source files of the prototype of iQRPcheck checking directly on seekable Zstandard. Experiments experiments: Contains scripts to test ParaProofa. More details in the dedicated section. gallery22: The instances of the QBFEval 2022. gallery23: The instances of the QBF Gallery 2023. original: The logfiles and plots of our original experiments output: A folder mounted by the host-file system to access the results produced by the experiments. scripts: A collection of parameterizable scripts to run different scenarios used by the experiments. Utils runlim: The source files for the runlim tool (only necessary for the experiments). simsala: The source files of simsala (only necessary for the experiments). How to use this artifact Docker We require a working docker installation on your side. The official documentation on how to set up docker can be found here. Note: If you encounter problems regarding permission, please check if your user is in the docker group. Run the artifact To run the docker container, execute the following commands.# Download paraproofa-artifact.zstdocker load < paraproofa-artifact.zstdocker run -v `pwd`/output:/output -itd --network none --name paraproofa-1 paraproofa-artifactdocker exec -it paraproofa-1 bash After execution, you are now connected to a running docker container and can execute ParaProofa. The folder output is mounted to your host system and contains the result of run experiments after running them. If you want to stop the container again, execute the following commands:exit # if you are still connected to the containerdocker stop paraproofa-1docker rm paraproofa-1 Alternative: Build the container yourself Instead of working with the pre-build image you can also build the docker container yourself. For this, download the paraproofa-artifact.tar.gz directory, unzip it and use it as the home directory of a new command line. Beside a Dockerfile building the artifact, we also provided scripts to make your life easier../build.sh # will take a while./run.sh./connect.shStopping the container works the same way as before, but we also provided the script ./cleanup.sh to execute it in one command. Experiments Disclaimer: As described in the artifact, one of ParaProofas bottlenecks are I/O operations. Thus, executing these experiments on a virtual machine (especially on a workstation) can heavily influence the runtimes. For this reason, we provided the results of our experiments in /original, which were conducted on a cluster with appropriate resources. Smoke Test To verify if the installation works, we provided /experiments/smoke.sh. It will execute DepQBF and ParaProofa with their full pipeline (solving with proof-generation and checking) on 61 fast samples. On our machine, this ran in ~1min30s. The results can be found in /output/depqbf_smoke.db, /output/depqbf_smoke.db and /output/smoke.png. Small Scope As the full scope is beyond the scope of testing the artifact, we provided small samples using around 100 formulas. You are expected to see the overhead the parallel solver has on smaller samples which was already stabilizing in our examples. The following table provides information about the small scope tests. Script Description Result approx. time /experiments/small/small-depqbf.sh depqbf-qrp (with checking) /output/small_depqbf.db 3min30s /experiments/small/small-paraq.sh paraq-iqrp-zstd (with checking) /output/small_paraq.db 3min30s /experiments/small/small-paraq-zeek.sh paraq-zeek-iqrp-zstd /output/small_paraq_zeek.db 3min30s For visualizing the result, just call /experiments/small/plot-small.sh to create /output/small.png. Full Scope We provided different scripts to run ParaProofa on the QBFEval 2022 and the QBF Gallery 2023. Each will produce a Sqlite database containing the data required to reconstruct the plots shown in the paper.The following table provides an overview of the available scripts Script Dataset Description Result /experiments/depqbf-run.sh qbfeval22 depqbf /output/depqbf_run.db /experiments/depqbf-proofgen.sh qbfeval22 depqbf-qrp /output/depqbf_proofgen.db /experiments/depqbf-proof-check.sh qbfeval22 depqbf-qrp (with checking) /output/depqbf_proofcheck.db /experiments/paraq-run.sh qbfeval22 paraq /output/paraq_run.db /experiments/paraq-proofgen.sh qbfeval22 paraq-iqrp-zstd /output/paraq_proofgen.db /experiments/paraq-proof-check.sh qbfeval22 paraq-iqrp-zstd (with checking) /output/paraq_proofcheck.db /experiments/paraq-zeek-proof-check.sh qbfeval22 paraq-zeek-iqrp-zstd (with checking) /output/paraq_zeek_proofcheck.db /experiments/gallery23-depqbf-run.sh gallery23 depqbf /output/gallery23_depqbf_run.db /experiments/gallery23-depqbf-proofgen.sh gallery23 depqbf-qrp /output/gallery23_depqbf_proofgen.db /experiments/gallery23-depqbf-proof-check.sh gallery23 depqbf-qrp (with checking) /output/gallery23_depqbf_proofcheck.db /experiments/gallery23-paraq-run.sh gallery23 paraq /output/gallery23_paraq_run.db /experiments/gallery23-paraq-proofgen.sh gallery23 paraq-iqrp-zstd /output/gallery23_paraq_proofgen.db /experiments/gallery23-paraq-proof-check.sh gallery23 paraq-iqrp-zstd (with checking) /output/gallery23_paraq_proofcheck.db Further, to compare those runs, a plotting script can be found in /scripts/plot.sh. For example, if the iqrp-checker should be compared against each other, the following command can be executed after finishing the runs:/scripts/plot.sh /output/paraq_proofcheck.db /output/paraq_zeek_proofcheck.db -o /output/checker-comparison.png Dependencies The following third-party sources are included in this artifact: ParaQooba (modified) DepQBF (modified) runlim simsala PyQBF The following dependencies are necessary to build the artifact (for a more detailed list we refer to the Dockerfile in paraproofa-artifact.tar.gz) GCC for C++ (g++) compiler CMake Zstandard curl boost PCRE2 and pkg-config rustup Python sqlite3 Perl DBI and Perl DBI sqlite3 driver Gnuplot Pandas