QSOLE: Automatic QBF Equivalence Checking Introduction This artifact was submitted by Peter Pfeiffer, Mark Peyrer, Daniel Große and Martina Seidl for the TACAS 2026 with the submission number 9062 aiming for Available, Functional and Reusable badges. It contains everything necessary to reproduce the examples shown in the corresponding paper alongside testcases to demonstrate basic functionality. In the following sections you will learn everything you need to know about this artifact and how to reproduce the experiments. The input formulas used by tests are divided into four categories: atleast contains at-least-k cardinality constraints with randomly generated quantifier prefixes and different encodings (km-totalizer and sequential counters). eq contains equals-k cardinality constraints with randomly generated quantifier prefixes and different encodings (km-totalizer and sequential counters). hein features Hein puzzles expressed with different encoding techniques from SQval. paper contains the examples presented in the corresponding paper. gt contains a larger sample set of at-least-k cardinality constraints. The artifact was published under the following DOI: 10.5281/zenodo.17356608 Structure and Content The artifact has the following structure:/|-- expected|-- output|-- qsole|-- scripts|-- tests expected contains the log-files of the experiments conducted with this artifact on our machine output is the target of the results from the experiments and is connected to a local folder with the same name on the host-machine. The logfiles from the runs can be found there qsole contains the c++ source code and build-environment for the QSOLE tool scripts is a collection of bash-scripts in order to run the experiments. The one relevant for you are listed in the next section tests contains the input formulas as well as the pcount for each check Running the artifact 1. Setup Docker A working docker environment installed on your machine is required. The docker container can be setup the following way:# download qsole-artifact.zst from zenododocker load specifies the check to be made (skent|sole|psole|skeq) [default: skent] --ouput outputs the encoding to the specified path --models if specified, models will be printed if suitable --subsumption if specified, eliminate subsumptions before encoding --noskip if specified, all checks will be done even if the result is already clear --quiet does not print any logging messages, not even errors --info increases verbosity level to "info"[QSOLE] [INF] Skolem Entailment f1 |=SK f2 resulted in 10[QSOLE] [INF] Skolem Entailment f2 |=SK f1 resulted in 20[QSOLE] [INF] Skolem Entailment !f1 |=SK !f2 resulted in 10[QSOLE] [INF] Skolem Entailment !f2 |=SK !f1 resulted in 10[QSOLE] [INF] Solution Equivalence (f1 SOL f2) resulted in 20 3. Run the Experiment While connected, you can run one of the following scripts to generate log-files.The output can be found in the output folder. The following requirements were measured on a host machine for the docker container with the following specifications: Intel Core i7-1355U Prozessor 32 GB RAM Intel Iris Xe GPU Script Description est. time /scripts/atleast_psole.sh Solution Equivalence of atleast ~150ms /scripts/atleast_full.sh All checks of atleast ~350ms /scripts/eq_psole.sh Solution Equivalence of eq > 3h /scripts/eq_full.sh All checks of eq > 3h /scripts/gt_psole.sh Solution Equivalence of gt > 3h /scripts/gt_full.sh All checks of gt > 3h /scripts/hein_psole.sh Solution Equivalence of hein ~45s /scripts/hein_full.sh All checks of hein ~150s /scripts/paper_psole.sh Solution Equivalence of paper ex. <10ms /scripts/paper_full.sh All checks of paper ex. ~20ms /scripts/all.sh All checks of this artifact ~200s Dependencies The following core-dependencies are required to run this artifact.Note that this is soley for information purpose, those do not have to be installed manually.For a more detailed list we want to refer to the Dockerfile in the sources, where the whole artifact can be reproduced from scratch.Each of the used tool has a licence within its source files. Third Party Tools used by QSOLE: DepQBF v6.03 CaDiCaL v2.1.3 Nenofex v1.1 (Included in DepQBF) Picosat v965 (Included in DepQBF) Needed for Building: Docker image ubuntu:24.04 GCC for C++ (g++) compiler CMake