Approximating Integer Solution Counting via Space Quantification for Linear Constraints
Authors: Cunjing Ge, Feifei Ma, Xutong Ma, Fan Zhang, Pei Huang, Jian Zhang
IJCAI 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental data shows that integer solution counting is usually more expensive than quantifying volume of solution space while their output values are close. So it is helpful to approximate the number of integer solutions by the volume if the error is acceptable. In this paper, we present and prove a bound of such error for LCs. It is the first bound that can be used to approximate the integer solution counts. Based on this result, an approximate integer solution counting method for LCs is proposed. Experiments show that our approach is over 20x faster than the stateof-the-art integer solution counters. Moreover, such advantage increases with the problem scale. |
| Researcher Affiliation | Academia | Cunjing Ge1,3 , Feifei Ma1,2,3 , Xutong Ma1,3 , Fan Zhang1,3 , Pei Huang1,3 and Jian Zhang1,3 1State Key Laboratory of Computer Science, ISCAS 2Laboratory of Parallel Software and Computational Science, ISCAS 3University of Chinese Academy of Sciences |
| Pseudocode | Yes | Algorithm 1 Approximate Counting via Volume |
| Open Source Code | Yes | Our tool and benchmarks are available at: https://github.com/ bearben/VOL2LAT |
| Open Datasets | Yes | Multiple Knapsack: We generated 100 instances from the classic multiple knapsack problem [Ab ıo and Stuckey, 2014]. The coefficients belong to [0, 10], the domain size is 64 and m = n, n {3, 4, 5}. Simple Temporal Planning: We randomly generated 150 instances based on the structure of Simple Temporal Networks (STNs) [Huang et al., 2018]. Instances from program analysis: We analyzed 7 programs ( cubature , gjk , http-parser , mu FFT , Simple XML , tcas and timeout ) ranging from 0.4k to 7.7k lines of source code via a symbolic execution bugfinding tool called CAnalyze [Xu et al., 2014]3 and generated 3803 instances in total. |
| Dataset Splits | No | No specific dataset split percentages, sample counts, or explicit cross-validation methodology are provided. The paper describes generating instances or using established benchmarks without detailing the partitioning for training, validation, and testing. |
| Hardware Specification | Yes | Experiments were conducted on a laptop workstation with 2.40GHz Intel Core i74700MQ CPU and 8GB memory. |
| Software Dependencies | No | The paper mentions implementation in C++ and names tools like Poly Vest, Latt E, Vinci, and q CORAL, but does not provide specific version numbers for any of these software components. |
| Experiment Setup | Yes | We used a timeout of half an hour, and chose ϵ = 0.2 and δ = 0.1 for Poly Vest (volume estimation). |