From Weighted to Unweighted Model Counting
Authors: Supratik Chakraborty, Dror Fried, Kuldeep S. Meel, Moshe Y. Vardi
IJCAI 2015 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments with weighted model counters built using our reduction indicate that these counters performs much better than a state-of-the-art weighted model counter. |
| Researcher Affiliation | Academia | Supratik Chakraborty Indian Institute of Technology, Bombay Dror Fried, Kuldeep S. Meel, Moshe Y. Vardi Department of Computer Science, Rice University |
| Pseudocode | No | The paper describes reductions and algorithms in text and through theorems but does not include structured pseudocode or algorithm blocks. |
| Open Source Code | No | The paper states that the authors "implemented our WMC-to-UMC module" and developed "Weight Count" but does not provide any link or explicit statement about making their own code publicly available. |
| Open Datasets | No | The paper mentions the types of benchmarks used, such as "problems arising from probablistic inference in grid networks, synthetic grid-structured random interaction Ising models...", but it does not provide concrete access information (e.g., specific links, DOIs, or citations with authors/year) for these datasets. |
| Dataset Splits | No | The paper does not provide specific details on training, validation, or test dataset splits, percentages, or cross-validation methodology. |
| Hardware Specification | Yes | Each node of the cluster had a 12-core 2.83 GHz Intel Xeon processor, with 4GB of main memory, and each of our experiments was run on a single core. |
| Software Dependencies | No | The paper mentions using "sharp SAT and DSharp as the underlying exact UMC solver" and comparing with "SDD", but it does not specify any version numbers for these software tools or libraries. |
| Experiment Setup | Yes | To allow speciļ¬cation of probabilities with a precision of up to to two decimal places, we rounded off the weights such that all weights were of the form k/2i (1 i 7). A uniform timeout of 5 hours was used for all tools in our experiments. |