An Approximate Skolem Function Counter
Authors: Arijit Shaw, Brendan Juba, Kuldeep S. Meel
AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We conducted a thorough evaluation of the performance and accuracy of results of the Skolem FC algorithm by implementing a functional prototype in C++. |
| Researcher Affiliation | Academia | Arijit Shaw1,2, Brendan Juba3, Kuldeep S. Meel4 1 Chennai Mathematical Institute, India 2 IAI, TCG-CREST, Kolkata, India 3 Washington University in St. Louis, USA 4 University of Toronto, Canada |
| Pseudocode | Yes | Algorithm 1: Stopping Rule (ε, δ), Algorithm 2: Skolem FC(F(X, Y ), ε, δ), Algorithm 3: Baseline(F(X, Y )) |
| Open Source Code | Yes | Source code: https://github.com/meelgroup/skolemfc/ |
| Open Datasets | Yes | All benchmarks and experimental data are available at https://doi.org/10.5281/zenodo.10404174 |
| Dataset Splits | No | The paper mentions using two sets of benchmarks (609 efficiency instances and 158 correctness instances) but does not specify how these instances are split into training, validation, or test sets. |
| Hardware Specification | Yes | All experiments were carried out on a cluster of nodes consisting of AMD EPYC 7713 CPUs running with 2x64 real cores. |
| Software Dependencies | No | The paper mentions using 'Uni Samp', 'Approx MC', 'Ganak (latest version)', and 'Crypto Mini Sat' but does not provide specific version numbers for these software dependencies. |
| Experiment Setup | Yes | Skolem FC was tested with ε = 0.8 and δ = 0.4. That gave the following values to error and tolerance parameters for model counting and sampling oracles. The almost uniform sampling oracle Uni Samp is run with εs = 0.16. The approximate model counting oracle Approx MC in line 7 was run with εc = 4 and δc = 0.32/ms, where s comes from the algorithm, based on input (ε, δ) and m is number of output variables in the specification. |