PyQBF: A Python Framework for Solving Quantified Boolean Formulas

PyQBF: A Python Framework for Solving Quantified Boolean Formulas

Introduction

This artifact was submitted by Mark Peyrer, Maximilian Heisinger and Martina Seidl for the iFM 2024 with the submission number 2625 aiming for Available, Functional and Reusable badges. It contains everything necessary to reproduce the experiments shown in the corresponding paper. In the following sections you will learn everything you need to know about this artifact and how to reproduce the experiments.

In order to make this artifact as accessible as possible, we divided the experiments into three tracks:

The small track contains only a fraction of the experiments. It requires little time and memory usage compared to the whole track, producing only a rough overview of the desired data accordingly.

The medium track gives a good overview and trend on how the data will look while remaining somewhere reasonable with time resources.

The all track fully reproduces the experiment as shown in the original paper. Note that this track does not include formulas which ran out of resources for both solver and pyqbf in the original experiment.

The artifact was published under the following DOI: 10.5281/zenodo.13341211

Artifact Requirements

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

Resource consumption in the original experiment was restricted (as it also is in this artifact) on 1hr as well as 8000MB per instance.

Outer-Counter Experiment

small: Approximately 1min30s with a maximum memory usage of 65MB

medium: Approximately 1h with a maximum memory usage of 270MB

all: Approximately 7hrs with a maximum memory usage of 425MB

Caqe Comparison Experiment

small: Approximately 1min with a maximum memory usage of 400MB

medium: Approximately 1h15min with a maximum memory usage of 2500MB

all: Approximately 12hrs30min with a maximum memory usage of 4000MB

DepQBF Comparison Experiment

small: Approximately 1min45s with a maximum memory usage of 500MB

medium: Approximately 40min with a maximum memory usage of 2500MB

all: Approximately 25hrs30min with a maximum memory usage of 8000MB

QFun Comparison Experiment

small: Approximately 1min with a maximum memory usage of 325MB

medium: Approximately 1h15min with a maximum memory usage of 820MB

all: Approximately 12hrs with a maximum memory usage of 4000MB

Qute Comparison Experiment

small: Approximately 1min with a maximum memory usage of 90MB

medium: Approximately 2hrs with a maximum memory usage of 425MB

all: Approximately 22hrs with a maximum memory usage of 3200MB

RAReQS Comparison Experiment

small: Approximately 1min with a maximum memory usage of 150MB

medium: Approximately 2hrs with a maximum memory usage of 7500MB

all: Approximately 17hrs with a maximum memory usage of 8000MB

Structure and Content

For running the artifact, the following structure is relevant for the experiments:

/
|-- expected
|-- experiments
| |-- outer-counter
| |-- compare-caqe
| |-- compare-depqbf
| |-- compare-qfun
| |-- compare-qute
| |-- compare-rareqs
|-- gallery23
|-- output
| |-- plots
|-- scripts

expected contains the runs of the experiments conducted with this artifact on our machine for reference and the long runs

experiments contains the scripts and runtime data when running the experiments. Each experiment has their own folder

gallery23 contains the complete testset of our experiments, i.e. the QBF-Gallery 2023 QDIMACS track. A complete list of the instances with absolute paths can be found in /experiments/targets.txt

output is the target of the results from the experiments, thus containing plots and sqlite-databases once executed. Furthermore, this folder is mounted by the host machine for comfortable access

scripts is a collection of python-scripts used by the experiments

Furthermore, there are folders containing the necessary tools used by the experiments. Those are not relevant when running the experiments but for extending the artifact.

/
|-- executables
|-- outer-count
|-- pyqbf
|-- runlim
|-- simsala
|-- solvers
| |-- caqe
| |-- depqbf
| |-- qfun
| |-- qute
| |-- rareqs

executables contains the executables of the solvers used in the experiments. They were built from the sources (except caqe) during the building-step of the docker image

outer-count is the cloned repository containing the outer-count tool for counting models

pyqbf contains all sources of our framework. Note that it is already installed into Python as a module such that import pyqbf is sufficient for any python script in the docker container

runlim is the cloned repository containing the runlim tool for benchmarking

simsala is the cloned repository containing the perl-scripts used for working with slurm. This was used to run the original experiments of the paper.

solvers contains the sources of the solvers their executables are build from. You can furthermore find their licences in there

How to use this artifact

1. Setup Docker

We require you to have a working docker environment installed on your machine. In order to set-up the docker container, run the following commands

# download pyqbf-artifact.zst from zenodo
docker load < pyqbf-artifact.zst
docker run -v `pwd`/output:/output -itd --network none --name pyqbf_artifact1 pyqbf-artifact
docker exec -it pyqbf_artifact1 bash

The first line loads the docker-image from the the export, the second will create a container using the image and the last connects your current terminal to the container.

In order to leave the container, just execute exit. Furthermore, you can call

docker stop pyqbf_artifact1
docker rm pyqbf_artifact1

to stop and delete the running container.

Important: Please ensure to have a working docker setup, with your user added to the docker group. This can be verified using docker ps. If there are no errors, your environment should be in working order.

2. Run the desired experiments

Reproduces figure 4, partwise.

Outer Counter (right part of figure 4)

small: /experiments/outer-counter/run-outer-small-seq.sh

medium:: /experiments/outer-counter/run-outer-medium-seq.sh

all: /experiments/outer-counter/run-outer-all-seq.sh

Comparison of Caqe executable with its PyQBF version (partial left part of figure 4)

small: /experiments/compare-caqe/run-caqe-small.sh

medium:: /experiments/compare-caqe/run-caqe-medium.sh

all: /experiments/compare-caqe/run-caqe-all.sh

Comparison of DepQBF executable with its PyQBF version (partial left part of figure 4)

small: /experiments/compare-depqbf/run-depqbf-small.sh

medium:: /experiments/compare-depqbf/run-depqbf-medium.sh

all: /experiments/compare-depqbf/run-depqbf-all.sh

Comparison of QFun executable with its PyQBF version (partial left part of figure 4)

small: /experiments/compare-qfun/run-qfun-small.sh

medium:: /experiments/compare-qfun/run-qfun-medium.sh

all: /experiments/compare-qfun/run-qfun-all.sh

Comparison of Qute executable with its PyQBF version (partial left part of figure 4)

small: /experiments/compare-qute/run-qute-small.sh

medium:: /experiments/compare-qute/run-qute-medium.sh

all: /experiments/compare-qute/run-qute-all.sh

Comparison of RAReQS executable with its PyQBF version (partial left part of figure 4)

small: /experiments/compare-rareqs/run-rareqs-small.sh

medium:: /experiments/compare-rareqs/run-rareqs-medium.sh

all: /experiments/compare-rareqs/run-rareqs-all.sh

All of the scripts will show verbose output when called.

3. Check the results

The results are copied automatically to the /output folder, which is mounted by a local ./output folder, such that after running the scripts the results will be available on your host machine.

Furthermore, the results produced by us running the artifact can be found in the /expected folder in the docker container.

In /output/plots (or /expected/plots respectively) you can find a logarithmic scatter plot with a corresponding name to the experiment produced by the data retrieved from the current run.

Using the script /scripts/diff-all.sh you can check all available databases in the /output folder for differences in the result-code.

Also the raw data is available directly in the /output folder as sqlite-databases. Those can either be looked at by a tool (we recommend DB Browser for sqlite) or by the command sqlite3 .db. The latter will open the database and allows queries on the data. Note: Both variants require a working sqlite installation on your host machine (e.g. apt-get install sqlite3)

Functional Badge

In the paper, we claimed that using our framework only comes with small overhead in comparison to using the executables. In particular, we showed a state-of-the-art implementation of an outer-model counter and compared it to a scripted version using PyQBF.

These claims can be replicated using this artifact. The all-track of each experiment will produce the necessary data to check this claim on the current machine on the same instances as seen in the paper. The other tracks (small and medium) will show a trend by evaluating a subset. By producing a scatter plot comparing a state-of-the-art instance to a scripted instance using PyQBF, it is trivial to see whether the claim holds.

There is no direct evaluation script as the datapoints are too dependent on external factors to produce the same results. However, the result codes of the solver can be compared using the /scripts/diff-all.sh script.

In order to check the code, we refer to the verbose of each of the experiments, where it is logged which executable is compared to which script. All sources of used tools are available within the artifact. Please check the Structure and Content section for further details.

Reusable badge

PyQBF is released under the GPLv3 licence and can be found publicly here. Furthermore, an extensive documentation can be found here.

This artifact can be used in numberous ways beyond the paper. The full potential of PyQBF is at one's disposal with a simple import pyqbf. Let it be a new algorithm using QBF-solvers or simple tasks like negating a QCNF formula - the framework allows easy prototyping with minimal overhead. Another example is the comparison of solvers against each other. The script /scripts/produce_scatter.py can be used to compare the data of any two sqlite-databases generated by such experiments and plot an overview of by linking the problems by their names. Finally, also PyQBF itself can be extended by e.g. more solvers. While this requires some particular knowledge about the architecture and building-pipeline, the already existing solvers will serve as a good example on how to implement such task - no matter if used by an interface or as a library. If just using a solver is sufficient, it can be directly bound into the PyQBF framework using QuAPI without needing to extend PyQBF (this only works if the command line interface is compatible with QuAPI).

At the current state, we support PyQBF for linux-based operating systems. Windows is not and will not be supported. Support for MacOS is currently in development.

Dependencies

The following core-dependencies are required by 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, where the whole artifact can be reproduced from scratch.

PyQBF (Commit 6a6cd1b535597d60895efd4971c7725f16e66eef):

PySAT

Caqe v4.0.1

DepQBF v6.03

QFun v1.0

Qute v1.1

RAReQS v1.1

QuAPI

Bloqqer

Needed for building PyQBF:

GCC for C++ (g++) compiler

ZeroMQ

ZLib

CMake

Python3 and Pip

Needed for the Test-Environment:

outer-count

Sqlite3

Runlim

Simsala

Gnuplot

QBF Gallery 2023