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. The corresponding paper was submitted to the 29th International Conference on Theory and Applications of Satisfiability Testing (SAT26). 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. Contents The artifact is packaged in a docker container with the following contents:/|-- certified-paraqooba|-- depqbf-adv|-- experiments|-- gallery22|-- gallery23|-- iqrpc|-- 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. 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 We require a working docker installation on your side. 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 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