Approximate Probabilistic Inference via Word-Level Counting
Authors: Supratik Chakraborty, Kuldeep Meel, Rakesh Mistry, Moshe Vardi
AAAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Empirical evaluation over an extensive suite of benchmarks demonstrates the promise of the approach. To illustrate the practical utility of SMTApprox MC, we implemented a prototype and evaluated it on a suite of benchmarks. |
| Researcher Affiliation | Academia | Supratik Chakraborty Indian Institute of Technology, Bombay Kuldeep S. Meel Department of Computer Science, Rice University Rakesh Mistry Indian Institute of Technology, Bombay Moshe Y. Vardi Department of Computer Science, Rice University |
| Pseudocode | Yes | The pseudocode for SMTApprox MC is presented in Algorithm 1. The pseudocode for SMTApprox MCCore is shown in Algorithm 2. |
| Open Source Code | No | The paper mentions a technical report available at http://arxiv.org/abs/1511.07663, but this is a PDF document, not a link to source code for the methodology described in the paper. No other links or explicit statements about code availability are provided. |
| Open Datasets | Yes | Our suite of benchmarks consisted of more than 150 problems arising from diverse domains such as reasoning about circuits, planning, program synthesis and the like. |
| Dataset Splits | No | The paper discusses using a 'suite of benchmarks' and 'selected a subset of benchmarks' for evaluation, but it does not specify any explicit training, validation, or test dataset splits (e.g., percentages, counts, or references to predefined splits). |
| Hardware Specification | Yes | Every experiment was conducted on a single core of high-performance computer cluster, where each node had a 20-core, 2.20 GHz Intel Xeon processor, with 3.2GB of main memory per core. |
| Software Dependencies | No | The paper states 'Both used Boolector, a state-of-the-art SMT solver for fixed-width words (Brummayer and Biere 2009)' and 'We employed the Mersenne Twister to generate pseudo-random numbers, and each thread was seeded independently using the Python random library.' While software is mentioned, specific version numbers for Boolector or the Python random library are not provided, only the publication year for Boolector's introduction. |
| Experiment Setup | Yes | Both model counters used an overall timeout of 12 hours per benchmark, and a Bounded SMT timeout of 2400 seconds per call. All experiments used ε = 0.8 and δ = 0.2. |