Model Counting and Sampling via Semiring Extensions
Authors: Andreas Goral, Joachim Giesen, Mark Blacher, Christoph Staudt, Julien Klaus
AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We have implemented the model counting and sampling extensions. Experiments show that our generic approach is competitive with the state of the art in model counting and model sampling. For the experimental evaluation of our generic model counting and sampling framework, we have implemented the semiring extension and used it together with a vanilla tensor network contraction algorithm. We evaluated the performance of MCSSE on the 200 problems of the 2022 Model Counting Competition for Boolean formulas in conjunctive normal form (CNF). We preprocessed the problems with Arjun (Soos and Meel 2022), which renders 23 of them trivial. We compared our semiring extension to the direct MPF model counting query from the MPF queries section, and to three state-of-the-art model counting softwares, namely, Sharp SAT-TD (Korhonen and Järvisalo 2021, 2023), the Python model counter Py SDD (Darwiche 2011), and D4 (Lagniez and Marquis 2017). |
| Researcher Affiliation | Academia | Friedrich Schiller University Jena, Germany {andreas.goral,joachim.giesen,mark.blacher,christoph.staudt,julien.klaus}@uni-jena.de |
| Pseudocode | No | The paper provides mathematical definitions, theorems, and proofs but no pseudocode or algorithm blocks. |
| Open Source Code | Yes | The code and more details about the experiments are provided in the supplement. |
| Open Datasets | Yes | We evaluated the performance of MCSSE on the 200 problems of the 2022 Model Counting Competition for Boolean formulas in conjunctive normal form (CNF)1. We preprocessed the problems with Arjun (Soos and Meel 2022), which renders 23 of them trivial. For the comparison we used a data set of 773 CNF formulas, which has been constructed by Gupta et al. (2019) from a wide range of publicly available benchmarks. |
| Dataset Splits | No | The paper mentions datasets used for evaluation but does not specify any training, validation, or test splits. It refers to 'problems' and 'data set' which were used for evaluation, implying the entire set was used for testing or the split information is not provided. |
| Hardware Specification | Yes | The experiments were performed on an Intel i9-10980XE 18-core processor machine running Ubuntu 20.04.1 LTS with 128 GB of RAM. Each core has a base frequency of 3.0 GHz, a max turbo frequency of 4.6 GHz, and supports the AVX-512 vector instruction set. |
| Software Dependencies | Yes | We implemented the semiring extension as a stand-alone datatype in Python 3.9 and Cython 3.0. In our implementation, tensors are represented by Num Py 1.25.1 nd-arrays, and the contraction order of the tensors is computed by opt_einsum 3.3.0 (Smith and Gray 2018). |
| Experiment Setup | No | The paper mentions using 'default settings for these softwares' (referring to state-of-the-art baselines) and a 'time limit of 30 seconds' for sampling experiments. However, it does not provide specific hyperparameter values or detailed system-level training settings for its own proposed method. |