Distribution-Aware Sampling and Weighted Model Counting for SAT
Authors: Supratik Chakraborty, Daniel Fremont, Kuldeep Meel, Sanjit Seshia, Moshe Vardi
AAAI 2014 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | To evaluate the performance of Weight Gen and Weight MC, we built prototype implementations and conducted an extensive set of experiments. |
| Researcher Affiliation | Academia | Supratik Chakraborty Indian Institute of Technology, Bombay Daniel J. Fremont University of California, Berkeley Kuldeep S. Meel Department of Computer Science, Rice University Sanjit A. Seshia University of California, Berkeley Moshe Y. Vardi Department of Computer Science, Rice University |
| Pseudocode | Yes | Algorithm 1 Weight MC(F, ε, δ, S, r), Algorithm 2 Weight MCCore(F, S, pivot, r, wmax), Algorithm 3 Bounded Weight SAT(F, pivot, r, wmax, S), Algorithm 4 Weight Gen(F, ε, r, S), Algorithm 5 Compute Kappa Pivot(ε), Algorithm 6 Partitioned Weight MC(F, ε, δ, S, L, H) |
| Open Source Code | No | The paper mentions external tools and references a technical report, but does not provide concrete access to the source code for the methodology described in this paper. |
| Open Datasets | Yes | The suite of benchmarks was made up of problems arising from various practical domains as well as problems of theoretical interest. Specifically, we used bit-level unweighted versions of constraints arising from grid networks, plan recognition, DQMR networks, bounded model checking of circuits, bit-blasted versions of SMT-LIB (SMT) benchmarks, and ISCAS89 (Brglez, Bryan, and Kozminski 1989) circuits with parity conditions on randomly chosen subsets of outputs and nextstate variables (Sang, Beame, and Kautz 2005; John and Chakraborty 2011). |
| Dataset Splits | No | The paper does not provide specific dataset split information (exact percentages, sample counts, citations to predefined splits, or detailed splitting methodology) for training or validation. The experiments evaluate algorithms on benchmark problems rather than training a model on a dataset with such splits. |
| Hardware Specification | Yes | We used a high performance cluster, with each experiment running on its own core. Each node of the cluster had two quad-core Intel Xeon processors with 4GB of main memory. |
| Software Dependencies | No | The paper mentions 'Crypto Mini SAT' and 'C++11' but does not provide specific version numbers for software dependencies or libraries. |
| Experiment Setup | Yes | Unless mentioned otherwise, our experiments for Weight MC reported in this paper used r = 5, ε = 0.8, and δ = 0.2, while our experiments for Weight Gen used r = 5 and ε = 16. ... We used 2500 seconds as the timeout of each invocation of Bounded Weight SAT and 20 hours as the overall timeout for Weight Gen and Weight MC. |