Notice: The reproducibility variables underlying each score are classified using an automated LLM-based pipeline, validated against a manually labeled dataset. LLM-based classification introduces uncertainty and potential bias; scores should be interpreted as estimates. Full accuracy metrics and methodology are described in [1].
Solving Satisfiability Modulo Counting Exactly with Probabilistic Circuits
Authors: Jinzhao Li, Nan Jiang, Yexiang Xue
ICML 2025 | Venue PDF | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | In the experiment, we compare KOCO-SMC with currently available approximate and exact SMC solvers on large-scale datasets and real-world applications. The proposed KOCO-SMC finds exact solutions with much less time. |
| Researcher Affiliation | Academia | 1Department of Computer Science, Purdue University, IN, USA. |
| Pseudocode | Yes | A high-level overview is provided in Algorithm 1. |
| Open Source Code | Yes | 1Code implementation is available at: https://github. com/jil016/koco-smc |
| Open Datasets | Yes | For the weighted function f, we use benchmark instances from the partition function task in the Uncertainty in Artificial Intelligence (UAI) Challenges, held between 2010 and 2022. We retain 50 instances defined over binary variables and group them into six categories: Alchemy (1 model), CSP (3 models), DBN (6 models), Grids (2 models), Promedas (32 models), and Segmentation (6 models). |
| Dataset Splits | No | Unless noted otherwise, each task uses three thresholds q obtained by multiplying the model s partition function by 10 20, 10 10, and 10 1. This yields 1,350 data points in total. For the Boolean formula ϕ, we generate 9 random 3-coloring map problems using CNFgen (Lauria et al., 2017). These instances involve binary encodings with variable counts ranging from 75 to 675. |
| Hardware Specification | Yes | All experiments are executed on two 64-core AMD Epyc 7662 Rome processors with 16 GB of memory. |
| Software Dependencies | Yes | We implement our method based on Mini SAT version 2.2.02. |
| Experiment Setup | Yes | Unless noted otherwise, each task uses three thresholds q obtained by multiplying the model s partition function by 10 20, 10 10, and 10 1. This yields 1,350 data points in total. |