19/08/2021

Decomposition Strategies to Count Integer Solutions over Linear Constraints

Cunjing Ge, Armin Biere

Keywords: Constraints and SAT, SAT, SAT, Satisfiability Modulo Theories

Abstract: Counting integer solutions of linear constraints has found interesting applications in various fields. It is equivalent to the problem of counting integer points inside a polytope. However, state-of-the-art algorithms for this problem become too slow for even a modest number of variables. In this paper, we propose new decomposition techniques which target both the elimination of variables as well as inequalities using structural properties of counting problems. 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.

 0
 0
 0
 0
This is an embedded video. Talk and the respective paper are published at IJCAI 2021 virtual conference. If you are one of the authors of the paper and want to manage your upload, see the question "My papertalk has been externally embedded..." in the FAQ section.

Comments

Post Comment
no comments yet
code of conduct: tbd Characters remaining: 140

Similar Papers