OxiDD: A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in Rust

This artifact complements our paper "OxiDD: A Safe, Concurrent, Modular, and Performant Decision Diagram Framework in Rust," allowing to reproduce our evaluation results. It consists of multiple parts:

• The source code of the OxiDD framework itself
• A modified version of BDD Benchmark, which we used for benchmarking our (C)BDD and ZBDD implementations
• Benchmarking results obtained using BDD Benchmark, both as raw log files and post-processed tables and figures. This is the data the evaluation section of our paper is based on.
• Scripts that automate benchmark execution and post-processing of the log files

As a decision diagram framework, OxiDD can be (re)used in the various applications of BDDs, ZBDDs, etc., and be extended to support further kinds of decision diagrams.

For more in-depth description, please read README.html or README.md contained in the .zip file.

This is the second revision of the artifact, for which we included Biodivine/LibBDD in the comparison. LibBDD is a notable BDD implementation written in Rust and to the best of our knowledge the only one that supports existential and universal quantification. The question of how previous Rust libraries, specifically LibBDD, compare to OxiDD came up during the review process of our paper. While we added LibBDD on the one hand, we removed the external memory library CAL from the figures on the other hand. Our initial benchmarks showed that in general, CAL cannot compete with performance, moreover the scope of this library is somewhat different. The raw benchmarking data is still included. While the initial version of the artifact passed the review process, there has not been an additional peer review for this revision.

This artifact is created for the TACAS 23 Artifact Evaluation VM.