Find research datasets worth reusing
Search datasets from major research repositories and use ShareScore to quickly assess how well each record supports discovery, access, and reuse.
2
datasets available to search
ShareScore release 0.9.0
Dataset results
2 results for “Quantified Formulas”
Artifacts for Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching
<p>This zip file contains the artifacts for the paper:</p> <p>J. Hoenicke and T. Schindler, <em>Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching, </em>VMCAI 2021, Springer</p> <p>The artifact is tested to work in the VMCAI 2021 virtual machine: <a href="https://doi.org/10.5281/zenodo.4017292">https://doi.org/10.5281/zenodo.4017292</a>.</p>
PyQBF: A Python Framework for Solving Quantified Boolean Formulas
<h1>PyQBF: A Python Framework for Solving Quantified Boolean Formulas</h1> <h2>Introduction</h2> <p>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.</p> <p>In order to make this artifact as accessible as possible, we divided the experiments into three tracks:</p> <ul> <li>The <strong>small</strong> 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.</li> <li>The <strong>medium</strong> track gives a good overview and trend on how the data will look while remaining somewhere reasonable with time resources.</li> <li>The <strong>all</strong> track fully reproduces the experiment as shown in the original paper. Note that this track <strong>does not include formulas which ran out of resources for both solver and pyqbf in the original experiment</strong>.</li> </ul> <p>The artifact was published under the following DOI: <a href="../qbf/pyqbf-artifact/-/blob/master/10.5281/zenodo.13341211">10.5281/zenodo.13341211</a></p> <h2>Artifact Requirements</h2> <p>The following requirements were measured on a host machine for the docker container with the following specifications:</p> <ul> <li><a href="https://www.intel.de/content/www/de/de/products/sku/232160/intel-core-i71355u-processor-12m-cache-up-to-5-00-ghz/specifications.html" target="_blank" rel="nofollow noreferrer noopener">Intel Core i7-1355U Prozessor</a></li> <li>32 GB RAM</li> <li>Intel Iris Xe GPU</li> </ul> <p>Resource consumption in the original experiment was restricted (as it also is in this artifact) on 1hr as well as 8000MB per instance.</p> <p><strong>Outer-Counter Experiment</strong></p> <ul> <li><strong>small</strong>: Approximately 1min30s with a maximum memory usage of 65MB</li> <li><strong>medium</strong>: Approximately 1h with a maximum memory usage of 270MB</li> <li><strong>all</strong>: Approximately 7hrs with a maximum memory usage of 425MB</li> </ul> <p><strong>Caqe Comparison Experiment</strong></p> <ul> <li><strong>small</strong>: Approximately 1min with a maximum memory usage of 400MB</li> <li><strong>medium</strong>: Approximately 1h15min with a maximum memory usage of 2500MB</li> <li><strong>all</strong>: Approximately 12hrs30min with a maximum memory usage of 4000MB</li> </ul> <p><strong>DepQBF Comparison Experiment</strong></p> <ul> <li><strong>small</strong>: Approximately 1min45s with a maximum memory usage of 500MB</li> <li><strong>medium</strong>: Approximately 40min with a maximum memory usage of 2500MB</li> <li><strong>all</strong>: Approximately 25hrs30min with a maximum memory usage of 8000MB</li> </ul> <p><strong>QFun Comparison Experiment</strong></p> <ul> <li><strong>small</strong>: Approximately 1min with a maximum memory usage of 325MB</li> <li><strong>medium</strong>: Approximately 1h15min with a maximum memory usage of 820MB</li> <li><strong>all</strong>: Approximately 12hrs with a maximum memory usage of 4000MB</li> </ul> <p><strong>Qute Comparison Experiment</strong></p> <ul> <li><strong>small</strong>: Approximately 1min with a maximum memory usage of 90MB</li> <li><strong>medium</strong>: Approximately 2hrs with a maximum memory usage of 425MB</li> <li><strong>all</strong>: Approximately 22hrs with a maximum memory usage of 3200MB</li> </ul> <p><strong>RAReQS Comparison Experiment</strong></p> <ul> <li><strong>small</strong>: Approximately 1min with a maximum memory usage of 150MB</li> <li><strong>medium</strong>: Approximately 2hrs with a maximum memory usage of 7500MB</li> <li><strong>all</strong>: Approximately 17hrs with a maximum memory usage of 8000MB</li> </ul> <h2>Structure and Content</h2> <p>For running the artifact, the following structure is relevant for the experiments:</p> <div> <pre><code>/ |-- expected |-- experiments | |-- outer-counter | |-- compare-caqe | |-- compare-depqbf | |-- compare-qfun | |-- compare-qute | |-- compare-rareqs |-- gallery23 |-- output | |-- plots |-- scripts</code></pre> </div> <ul> <li><code>expected</code> contains the runs of the experiments conducted with this artifact on our machine for reference and the long runs</li> <li><code>experiments</code> contains the scripts and runtime data when running the experiments. Each experiment has their own folder</li> <li><code>gallery23</code> contains the complete testset of our experiments, i.e. the <a href="https://qbf23.pages.sai.jku.at/gallery/" target="_blank" rel="nofollow noreferrer noopener">QBF-Gallery 2023</a> QDIMACS track. A complete list of the instances with absolute paths can be found in <code>/experiments/targets.txt</code></li> <li><code>output</code> 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</li> <li><code>scripts</code> is a collection of python-scripts used by the experiments</li> </ul> <p>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.</p> <div> <pre><code>/ |-- executables |-- outer-count |-- pyqbf |-- runlim |-- simsala |-- solvers | |-- caqe | |-- depqbf | |-- qfun | |-- qute | |-- rareqs</code></pre> </div> <ul> <li><code>executables</code> 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</li> <li><code>outer-count</code> is the <a href="https://github.com/marseidl/outer-count" target="_blank" rel="nofollow noreferrer noopener">cloned repository</a> containing the outer-count tool for counting models</li> <li><code>pyqbf</code> contains all sources of our framework. Note that it is already installed into Python as a module such that <code>import pyqbf</code> is sufficient for any python script in the docker container</li> <li><code>runlim</code> is the <a href="https://github.com/arminbiere/runlim" target="_blank" rel="nofollow noreferrer noopener">cloned repository</a> containing the runlim tool for benchmarking</li> <li><code>simsala</code> is the <a href="https://gitlab.sai.jku.at/simsala/simsala">cloned repository</a> containing the perl-scripts used for working with slurm. This was used to run the original experiments of the paper.</li> <li><code>solvers</code> contains the sources of the solvers their executables are build from. You can furthermore find their licences in there</li> </ul> <h2>How to use this artifact</h2> <h3>1. Setup Docker</h3> <p>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</p> <div> <pre><code># 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</code></pre> </div> <p>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.</p> <p>In order to leave the container, just execute <code>exit</code>. Furthermore, you can call</p> <div> <pre><code>docker stop pyqbf_artifact1 docker rm pyqbf_artifact1</code></pre> </div> <p>to stop and delete the running container.</p> <p><strong>Important:</strong> Please ensure to have a working docker setup, with your user added to the <code>docker</code> group. This can be verified using <code>docker ps</code>. If there are no errors, your environment should be in working order.</p> <h3>2. Run the desired experiments</h3> <p>Reproduces figure 4, partwise.</p> <p><strong>Outer Counter</strong> (right part of figure 4)</p> <ul> <li><strong>small:</strong> <code>/experiments/outer-counter/run-outer-small-seq.sh</code></li> <li><strong>medium:</strong>: <code>/experiments/outer-counter/run-outer-medium-seq.sh</code></li> <li><strong>all:</strong> <code>/experiments/outer-counter/run-outer-all-seq.sh</code></li> </ul> <p><strong>Comparison of Caqe executable with its PyQBF version</strong> (partial left part of figure 4)</p> <ul> <li><strong>small:</strong> <code>/experiments/compare-caqe/run-caqe-small.sh</code></li> <li><strong>medium:</strong>: <code>/experiments/compare-caqe/run-caqe-medium.sh</code></li> <li><strong>all:</strong> <code>/experiments/compare-caqe/run-caqe-all.sh</code></li> </ul> <p><strong>Comparison of DepQBF executable with its PyQBF version</strong> (partial left part of figure 4)</p> <ul> <li><strong>small:</strong> <code>/experiments/compare-depqbf/run-depqbf-small.sh</code></li> <li><strong>medium:</strong>: <code>/experiments/compare-depqbf/run-depqbf-medium.sh</code></li> <li><strong>all:</strong> <code>/experiments/compare-depqbf/run-depqbf-all.sh</code></li> </ul> <p><strong>Comparison of QFun executable with its PyQBF version</strong> (partial left part of figure 4)</p> <ul> <li><strong>small:</strong> <code>/experiments/compare-qfun/run-qfun-small.sh</code></li> <li><strong>medium:</strong>: <code>/experiments/compare-qfun/run-qfun-medium.sh</code></li> <li><strong>all:</strong> <code>/experiments/compare-qfun/run-qfun-all.sh</code></li> </ul> <p><strong>Comparison of Qute executable with its PyQBF version</strong> (partial left part of figure 4)</p> <ul> <li><strong>small:</strong> <code>/experiments/compare-qute/run-qute-small.sh</code></li> <li><strong>medium:</strong>: <code>/experiments/compare-qute/run-qute-medium.sh</code></li> <li><strong>all:</strong> <code>/experiments/compare-qute/run-qute-all.sh</code></li> </ul> <p><strong>Comparison of RAReQS executable with its PyQBF version</strong> (partial left part of figure 4)</p> <ul> <li><strong>small:</strong> <code>/experiments/compare-rareqs/run-rareqs-small.sh</code></li> <li><strong>medium:</strong>: <code>/experiments/compare-rareqs/run-rareqs-medium.sh</code></li> <li><strong>all:</strong> <code>/experiments/compare-rareqs/run-rareqs-all.sh</code></li> </ul> <p>All of the scripts will show verbose output when called.</p> <h3>3. Check the results</h3> <p>The results are copied automatically to the <code>/output</code> folder, which is mounted by a local <code>./output</code> folder, such that after running the scripts the results will be available on your host machine.</p> <p>Furthermore, the results produced by us running the artifact can be found in the <code>/expected</code> folder in the docker container.</p> <p>In <code>/output/plots</code> (or <code>/expected/plots</code> respectively) you can find a logarithmic scatter plot with a corresponding name to the experiment produced by the data retrieved from the current run.</p> <p>Using the script <code>/scripts/diff-all.sh</code> you can check all available databases in the <code>/output</code> folder for differences in the result-code.</p> <p>Also the raw data is available directly in the <code>/output</code> folder as sqlite-databases. Those can either be looked at by a tool (we recommend <a href="https://sqlitebrowser.org/dl/" target="_blank" rel="nofollow noreferrer noopener">DB Browser for sqlite</a>) or by the command <code>sqlite3 <name>.db</code>. The latter will open the database and allows queries on the data. <strong>Note:</strong> Both variants require a working sqlite installation on your host machine (e.g. <code>apt-get install sqlite3</code>)</p> <h2>Functional Badge</h2> <p>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.</p> <p>These claims can be replicated using this artifact. The <strong>all</strong>-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 (<strong>small</strong> and <strong>medium</strong>) 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.</p> <p>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 <code>/scripts/diff-all.sh</code> script.</p> <p>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 <em>Structure and Content</em> section for further details.</p> <h2>Reusable badge</h2> <p>PyQBF is released under the GPLv3 licence and can be found publicly <a href="https://gitlab.sai.jku.at/qbf/pyqbf/">here</a>. Furthermore, an extensive documentation can be found <a href="https://gitlab.sai.jku.at/qbf/pyqbf/">here</a>.</p> <p>This artifact can be used in numberous ways beyond the paper. The full potential of PyQBF is at one's disposal with a simple <code>import pyqbf</code>. 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 <code>/scripts/produce_scatter.py</code> 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 <a href="https://github.com/maximaximal/QuAPI" target="_blank" rel="nofollow noreferrer noopener">QuAPI</a> without needing to extend PyQBF (this only works if the command line interface is compatible with QuAPI).</p> <p>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.</p> <h2>Dependencies</h2> <p>The following core-dependencies are required by this artifact. Note that this is <strong>soley for information purpose, those do not have to be installed manually</strong>. For a more detailed list we want to refer to the <a href="../qbf/pyqbf-artifact/-/blob/master/Dockerfile">Dockerfile</a>, where the whole artifact can be reproduced from scratch.</p> <p><strong>PyQBF (<a href="https://gitlab.sai.jku.at/qbf/pyqbf/-/tree/6a6cd1b535597d60895efd4971c7725f16e66eef">Commit 6a6cd1b535597d60895efd4971c7725f16e66eef</a>):</strong></p> <ul> <li><a href="https://pysathq.github.io/" target="_blank" rel="nofollow noreferrer noopener">PySAT</a></li> <li><a href="https://github.com/ltentrup/caqe" target="_blank" rel="nofollow noreferrer noopener">Caqe v4.0.1</a></li> <li><a href="https://github.com/lonsing/depqbf" target="_blank" rel="nofollow noreferrer noopener">DepQBF v6.03</a></li> <li><a href="https://github.com/MikolasJanota/qfun" target="_blank" rel="nofollow noreferrer noopener">QFun v1.0</a></li> <li><a href="https://github.com/fslivovsky/qute" target="_blank" rel="nofollow noreferrer noopener">Qute v1.1</a></li> <li><a href="https://sat.inesc-id.pt/~mikolas/sw/areqs/" target="_blank" rel="nofollow noreferrer noopener">RAReQS v1.1</a></li> <li><a href="https://github.com/maximaximal/QuAPI" target="_blank" rel="nofollow noreferrer noopener">QuAPI</a></li> <li><a href="https://fmv.jku.at/bloqqer/" target="_blank" rel="nofollow noreferrer noopener">Bloqqer</a></li> </ul> <p><strong>Needed for building PyQBF:</strong></p> <ul> <li>GCC for C++ (<a href="https://gcc.gnu.org/" target="_blank" rel="nofollow noreferrer noopener">g++</a>) compiler</li> <li><a href="https://zeromq.org/" target="_blank" rel="nofollow noreferrer noopener">ZeroMQ</a></li> <li><a href="https://www.zlib.net/" target="_blank" rel="nofollow noreferrer noopener">ZLib</a></li> <li><a href="https://cmake.org/" target="_blank" rel="nofollow noreferrer noopener">CMake</a></li> <li><a href="https://www.python.org/downloads/" target="_blank" rel="nofollow noreferrer noopener">Python3</a> and Pip</li> </ul> <p><strong>Needed for the Test-Environment:</strong></p> <ul> <li><a href="https://github.com/marseidl/outer-count" target="_blank" rel="nofollow noreferrer noopener">outer-count</a></li> <li><a href="https://www.sqlite.org/" target="_blank" rel="nofollow noreferrer noopener">Sqlite3</a></li> <li><a href="https://github.com/arminbiere/runlim" target="_blank" rel="nofollow noreferrer noopener">Runlim</a></li> <li><a href="https://gitlab.sai.jku.at/simsala/simsala/-/tree/main">Simsala</a></li> <li><a href="http://www.gnuplot.info/" target="_blank" rel="nofollow noreferrer noopener">Gnuplot</a></li> <li><a href="https://qbf23.pages.sai.jku.at/gallery/" target="_blank" rel="nofollow noreferrer noopener">QBF Gallery 2023</a></li> </ul>
ScienceDex guides
Understand access before you commit
These curated guides explain access requirements, typical timelines, costs, and reuse considerations for widely used research datasets.
Allen Brain Atlas
Allen Brain Atlas is an Allen Institute collection of brain map atlases, datasets, APIs, and analysis tools covering mouse, human, and non-human primate brain resources.
Annotated Behaviour and Observability Dataset (ABODe)
ABODe is a University of Edinburgh DataShare dataset for behavior classification in group-housed mice using home-cage video, identities, bounding boxes, ground-plate positions, and annotator labels.
DANDI Archive for NWB datasets
DANDI is a BRAIN Initiative archive for publishing and sharing neurophysiology data, including electrophysiology, optophysiology, and behavioral data packaged as NWB and related standards.
International Brain Laboratory public data
The International Brain Laboratory public data releases expose standardized mouse decision-making experiments, including Neuropixels recordings, widefield calcium imaging, behavior, and session metadata accessed through the ONE API.
OpenNeuro
OpenNeuro is a free, open platform for sharing neuroimaging datasets, with public search, dataset pages, and download paths for web, S3, DataLad, and the OpenNeuro CLI.