Improved Bounds of Integer Solution Counts via Volume and Extending to Mixed-Integer Linear Constraints

Authors Cunjing Ge , Armin Biere



PDF
Thumbnail PDF

File

LIPIcs.CP.2024.13.pdf
  • Filesize: 1.41 MB
  • 17 pages

Document Identifiers

Author Details

Cunjing Ge
  • National Key Laboratory for Novel Software Technology, Nanjing University, China
  • School of Artificial Intelligence, Nanjing University, China
Armin Biere
  • University of Freiburg, Germany

Cite AsGet BibTex

Cunjing Ge and Armin Biere. Improved Bounds of Integer Solution Counts via Volume and Extending to Mixed-Integer Linear Constraints. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 13:1-13:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CP.2024.13

Abstract

Solution counting and solution space integration over linear constraints are important problems with many applications. Previous works addressed either only counting integer points in polytopes (integer counting) with integer variables or alternatively only computing the volume of polytopes (solution space integration) on variables over the reals, including approximating the integer count via a polytope’s volume. We are not aware of a non-trivial algorithm which addresses the mixed case, where linear constraints are over mixed integer and real variables. In this paper, we propose a new randomized algorithm to approximate guarantees (bounds) of integer solution counts. Then we present upper and lower bounds for solution space integration over mixed-integer linear constraints. Thus, proposed algorithms can be extended to mixed-integer cases as well. The experiments show that approximations are often very close to exact results in practice, and bounds approximated by our algorithm are often tight and useful.

Subject Classification

ACM Subject Classification
  • Theory of computation → Automated reasoning
Keywords
  • Integer Solution Counting
  • Mixed-Integer Linear Constraints
  • #SMT(LA) Problems
  • Volume of Polytopes

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Alexander I. Barvinok. Computing the volume, counting integral points, and exponential sums. Discrete & Computational Geometry, 10:123-141, 1993. URL: https://doi.org/10.1007/BF02573970.
  2. Alexander I. Barvinok. Computing the ehrhart polynomial of a convex lattice polytope. Discrete & Computational Geometry, 12:35-48, 1994. URL: https://doi.org/10.1007/BF02574364.
  3. V. Belle, A. Passerini, and Guy Van den Broeck. Probabilistic inference in hybrid domains by weighted model integration. In Qiang Yang and Michael J. Wooldridge, editors, Proc. of IJCAI 2015, pages 2770-2776. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/392.
  4. H. C. P. Berbee, C. G. E. Boender, A. H. G. Rinnooy Kan, C. L. Scheffer, R. L. Smith, and J. Telgen. Hit-and-run algorithms for the identification of nonredundant linear inequalities. Math. Program., 37(2):184-207, 1987. URL: https://doi.org/10.1007/BF02591694.
  5. B. Büeler, A. Enge, and K. Fukuda. Exact Volume Computation for Polytopes: A Practical Study, pages 131-154. Birkhäuser, 2000. URL: https://doi.org/10.1007/978-3-0348-8438-9_6.
  6. Supratik Chakraborty, Kuldeep S. Meel, Rakesh Mistry, and Moshe Y. Vardi. Approximate probabilistic inference via word-level counting. In Proc. of AAAI, pages 3218-3224, 2016. Google Scholar
  7. Dmitry Chistikov, Rayna Dimitrova, and Rupak Majumdar. Approximate counting in SMT and value estimation for probabilistic programs. In Proc. of TACAS, pages 320-334, 2015. Google Scholar
  8. Ben Cousins and Santosh S. Vempala. Gaussian cooling and o*(n3) algorithms for volume and gaussian volume. SIAM J. Comput., 47(3):1237-1273, 2018. URL: https://doi.org/10.1137/15M1054250.
  9. M. E. Dyer, A. M. Frieze, and R. Kannan. A random polynomial time algorithm for approximating the volume of convex bodies. In Proc. of STOC, pages 375-381, 1989. URL: https://doi.org/10.1145/73007.73043.
  10. C. Ge and F. Ma. A fast and practical method to estimate volumes of convex polytopes. In Jianxin Wang and Chee-Keng Yap, editors, Proc. of FAW, volume 9130 of Lecture Notes in Computer Science, pages 52-65. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-19647-3_6.
  11. C. Ge, F. Ma, X. Ma, F. Zhang, P. Huang, and J. Zhang. Approximating integer solution counting via space quantification for linear constraints. In Sarit Kraus, editor, Proc. of IJCAI, pages 1697-1703. ijcai.org, 2019. URL: https://doi.org/10.24963/ijcai.2019/235.
  12. C. Ge, F. Ma, P. Zhang, and J. Zhang. Computing and estimating the volume of the solution space of SMT(LA) constraints. Theor. Comput. Sci., 743:110-129, 2018. URL: https://doi.org/10.1016/j.tcs.2016.10.019.
  13. Cunjing Ge and Armin Biere. Decomposition strategies to count integer solutions over linear constraints. In Zhi-Hua Zhou, editor, Proc. of IJCAI, pages 1389-1395. ijcai.org, 2021. URL: https://doi.org/10.24963/ijcai.2021/192.
  14. Jaco Geldenhuys, Matthew B. Dwyer, and Willem Visser. Probabilistic symbolic execution. In Proc. of ISSTA, pages 166-176, 2012. URL: https://doi.org/10.1145/2338965.2336773.
  15. M. Grötschel, L. Lovász, and A. Schrijver. Geometric algorithms and combinatorial optimization. Combinatorica, 1988. Google Scholar
  16. Amy Huang, Liam Lloyd, Mohamed Omar, and James C. Boerkoel. New perspectives on flexibility in simple temporal planning. In Proc. of ICAPS, pages 123-131, 2018. URL: https://aaai.org/ocs/index.php/ICAPS/ICAPS18/paper/view/17775.
  17. Samuel Kolb, Pedro Zuidberg Dos Martires, and Luc De Raedt. How to exploit structure while solving weighted model integration problems. In Amir Globerson and Ricardo Silva, editors, Proc. of UAI, volume 115 of Proceedings of Machine Learning Research, pages 744-754. AUAI Press, 2019. URL: http://proceedings.mlr.press/v115/kolb20a.html.
  18. Jesús A. De Loera, Raymond Hemmecke, Jeremiah Tauzer, and Ruriko Yoshida. Effective lattice point counting in rational convex polytopes. J. Symb. Comput., 38(4):1273-1302, 2004. URL: https://doi.org/10.1016/j.jsc.2003.04.003.
  19. L. Lovász and I. Deák. Computational results of an O^*(n⁴) volume algorithm. European Journal of Operational Research, 216(1):152-161, 2012. URL: https://doi.org/10.1016/j.ejor.2011.06.024.
  20. L. Lovász and S. Vempala. Hit-and-run from a corner. SIAM J. Comput., 35(4):985-1005, 2006. URL: https://doi.org/10.1137/S009753970544727X.
  21. L. Lovász and S. Vempala. Simulated annealing in convex bodies and an O^*(n⁴) volume algorithm. J. Comput. Syst. Sci., 72(2):392-417, 2006. URL: https://doi.org/10.1016/j.jcss.2005.08.004.
  22. László Lovász. Hit-and-run mixes fast. Math. Program., 86(3):443-461, 1999. URL: https://doi.org/10.1007/s101070050099.
  23. Kasper Søe Luckow, Corina S. Pasareanu, Matthew B. Dwyer, Antonio Filieri, and Willem Visser. Exact and approximate probabilistic symbolic execution for nondeterministic programs. In Proc. of ASE, pages 575-586, 2014. URL: https://doi.org/10.1145/2642937.2643011.
  24. F. Ma, S. Liu, and J. Zhang. Volume computation for boolean combination of linear arithmetic constraints. In Proc. of CADE, pages 453-468, 2009. URL: https://doi.org/10.1007/978-3-642-02959-2_33.
  25. P. Z. Dos Martires, A. Dries, and Luc De Raedt. Exact and approximate weighted model integration with probability density functions using knowledge compilation. In Proc. of AAAI, 2019, pages 7825-7833. AAAI Press, 2019. URL: https://doi.org/10.1609/aaai.v33i01.33017825.
  26. P. Morettin, A. Passerini, and R. Sebastiani. Advanced SMT techniques for weighted model integration. Artif. Intell., 275:1-27, 2019. URL: https://doi.org/10.1016/j.artint.2019.04.003.
  27. Gilles Pesant. Counting-based search for constraint optimization problems. In Proc. of AAAI, pages 3441-3448, 2016. URL: http://www.aaai.org/ocs/index.php/AAAI/AAAI16/paper/view/12065, URL: https://doi.org/10.1609/AAAI.V30I1.10433.
  28. Giuseppe Spallitta, Gabriele Masina, Paolo Morettin, Andrea Passerini, and Roberto Sebastiani. Smt-based weighted model integration with structure awareness. In James Cussens and Kun Zhang, editors, Proc. of UAI, volume 180 of Proceedings of Machine Learning Research, pages 1876-1885. PMLR, 2022. URL: https://proceedings.mlr.press/v180/spallitta22a.html.
  29. Leslie G. Valiant. The complexity of enumeration and reliability problems. SIAM J. Comput., 8(3):410-421, 1979. URL: https://doi.org/10.1137/0208032.
  30. Sven Verdoolaege, Rachid Seghir, Kristof Beyls, Vincent Loechner, and Maurice Bruynooghe. Counting integer points in parametric polytopes using barvinok’s rational functions. Algorithmica, 48(1):37-66, 2007. URL: https://doi.org/10.1007/s00453-006-1231-0.
  31. E. B. Wilson. Probable inference, the law of succession, and statistical inference. Journal of the American Statistical Association, 22(158):209-212, 1927. URL: https://doi.org/10.1080/01621459.1927.10502953.
  32. Alessandro Zanarini and Gilles Pesant. Solution counting algorithms for constraint-centered search heuristics. In Proc. of CP, pages 743-757, 2007. URL: https://doi.org/10.1007/978-3-540-74970-7_52.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail