Maximum Model Counting
Authors: Daniel Fremont, Markus Rabe, Sanjit Seshia
AAAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Through several experiments we show that our approach can be successfully applied to interesting problems. |
| Researcher Affiliation | Academia | University of California, Berkeley Email: {dfremont,rabe,sseshia}@berkeley.edu |
| Pseudocode | Yes | Algorithm 2 MAXCOUNT(ϕ(X, Y, Z), ϵ, δ) k 2|X|/ log2(1 + ϵ) n 34 ln(2/δ) s1, . . . , sn SAMPLE(ϕk(X, Y , Z), X Y , n, 17) for all i {1, . . . , n} do (xi, yi) si ci COUNT(ϕ(xi, Y, Z), Y, 1 + ϵ, δ/2n) end for i arg maxi ci return (ci, xi) |
| Open Source Code | No | The paper states: "In our tool we use an improved implementation of these algorithms by Mate Soos and Kuldeep Meel, which is pending publication." This indicates a future release or an unreleased implementation, not concrete access to open-source code for the methodology at the time of publication. |
| Open Datasets | Yes | We tested this encoding with benchmarks from the 2016 Max SAT competition. ... Several actual vulnerabilities in the Linux kernel were studied by Heusser and Malacaria (2010). ... see the Appendix in the full version of the paper (Fremont, Rabe, and Seshia 2016) for benchmark details. ... In Table 1 we summarize a set of program synthesis tasks from the Sketch performance benchmarks. |
| Dataset Splits | No | The paper discusses experiments on benchmarks but does not specify the exact percentages, sample counts, or methodology for training, validation, and test splits. |
| Hardware Specification | Yes | all performed on identical machines with Intel Core i7 3.1GHz processors. |
| Software Dependencies | No | The paper mentions using an "improved implementation of these algorithms by Mate Soos and Kuldeep Meel, which is pending publication" but does not specify any software dependencies with version numbers (e.g., Python version, library versions). |
| Experiment Setup | Yes | k 2|X|/ log2(1 + ϵ) n 34 ln(2/δ) ... The parameters ϵ and δ specify the desired tolerance and failure probability. ... Figure 1. ... Experiments with n = 20 samples and counting tolerance ϵ = 1. |