Approximate Integer Solution Counts over Linear Arithmetic Constraints
Authors: Cunjing Ge
AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experiments on extensive benchmarks show that our algorithm could solve polytopes with dozens of dimensions, which significantly outperforms state-of-the-art counters. |
| Researcher Affiliation | Academia | National Key Laboratory for Novel Software Technology, Nanjing University, China School of Artificial Intelligence, Nanjing University, China |
| Pseudocode | Yes | Algorithm 1: Sample() Algorithm 2: Subdivision() Algorithm 3: Approximate Lattice Counts |
| Open Source Code | Yes | Source code of ALC and experimental data including benchmarks can be found at https://github.com/bearben/ALC. |
| Open Datasets | Yes | The benchmark set consists of three parts: Random Polytopes: We generated 726 random polytopes... Rotated Thin Rectangles: To evaluate the quality of approximations on thin polytopes, 180 n-dimensional rectangles... Application Instances: We adopted 4131 benchmarks (Ge and Biere 2021) from program analysis and simple temporal planning. |
| Dataset Splits | No | The paper evaluates an algorithm for counting integer solutions on benchmark sets and does not involve training, validation, and test splits in the context of machine learning model development. No explicit split percentages or counts are provided for the benchmark sets. |
| Hardware Specification | Yes | Experiments were conducted on Intel(R) Xeon(R) Gold 6248 @ 2.50GHz CPUs with a time limit of 3600 seconds and memory limit of 4 GB per benchmark. |
| Software Dependencies | No | The paper states 'We implemented a prototype tool called APPROXLATCOUNT (ALC) 1 in C++', but does not provide specific version numbers for any software dependencies or compilers. |
| Experiment Setup | Yes | The setting of parameters in Algorithm 1, 2 and 3 are listed with explanations as the following: ϵ = 0.2 and δ = 0.1. They determine the bounds of counts computed by our approach. ... w = n. ... s = 2/(δ ϵ2): ... rmin = 0.4, rmax = 0.6, µ = 0.005 and γ = 10. |