Decomposition Strategies to Count Integer Solutions over Linear Constraints
Authors: Cunjing Ge, Armin Biere
IJCAI 2021 | 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 improves the performance of state-of-the-art counting algorithms, while the overhead is usually negligible compared to the running time of integer counting. and 5 Evaluation Based on Algorithm 2, we implemented a prototype tool called INTCOUNT1 in C++. Furthermore, we integrated INTCOUNT into a DPLL(T)-based #SMT(LA) counter [Ge et al., 2018]. We used a timeout of 3600 seconds, and chose SIZE LIMIT = n/2 . Another parameter DEPTH LIMIT was set to 4 if n 10, and 1 if n < 10. Experiments were conducted on Intel(R) Xeon(R) E5-2620 v4 @ 2.10GHz CPUs with a time limit of 3600 seconds and memory limit of 8 GB per benchmark. |
| Researcher Affiliation | Academia | Cunjing Ge , Armin Biere Johannes Kepler University Linz, Austria cunjing.ge@jku.at , armin.biere@jku.at |
| Pseudocode | Yes | Algorithm 1: Row and Column Selection and Algorithm 2: Decomposition with Row and Column Elimination |
| Open Source Code | Yes | 1The source code and benchmarks can be found at https:// github.com/bearben/intcount . |
| Open Datasets | Yes | The benchmark set used in our experiments consists of two parts: Random Polytopes: We generated 2840 random benchmarks with three parameters (n, m, lmax), where n [5, 20] is the number of variables, m [1, n] is the number of constraints, and lmax [1, n] is the maximum length (non-zero coefficients) of constraints. The domain of variables is [ 8, 7]. Application Instances: We adopted 3953 benchmarks [Ge et al., 2019] from program analysis and simple temporal planning. Since most of the above program analysis benchmarks can be trivially handled by direct decomposition. We also generated 178 new and more challenging benchmarks by analyzing a Shell sort C program with less simplifications (modeling each element in an array and exploding a loop with more rounds). The domain of variables is [ 32, 31]. and 1The source code and benchmarks can be found at https:// github.com/bearben/intcount . |
| Dataset Splits | No | The paper describes generating benchmarks and running experiments on them, but it does not specify any explicit training/validation/test splits. |
| Hardware Specification | Yes | Experiments were conducted on Intel(R) Xeon(R) E5-2620 v4 @ 2.10GHz CPUs with a time limit of 3600 seconds and memory limit of 8 GB per benchmark. |
| Software Dependencies | No | The paper mentions C++ as the implementation language for INTCOUNT, integrates it into a DPLL(T)-based #SMT(LA) counter, and uses BARVINOK and BOOLECTOR, but it does not provide specific version numbers for any of these software dependencies. |
| Experiment Setup | Yes | We used a timeout of 3600 seconds, and chose SIZE LIMIT = n/2 . Another parameter DEPTH LIMIT was set to 4 if n 10, and 1 if n < 10. |