Efficiently Solving Unbounded Integer Programs in the context of SMT Solvers
Efficiently Solving Unbounded Integer Programs in the context of SMT Solvers
Vortrag von Martin Bromberger
Satisfiability modulo theories (SMT) solvers are automated theorem provers for logical formulas that range over combinations of various first-order theories. These theories typically correspond to domains found in programming languages, e.g., the theories of bit vectors, integers, and arrays. This is intentional because SMT solvers were initially developed as back-end reasoning tools for automated software verification. These days, SMT solvers are also used as back-end reasoning tools for various other applications, e.g., verification of hybrid systems, program synthesis, and as brute-force tactics in various interactive theorem provers.
In this talk, I will present two new techniques for the theory of linear integer arithmetic in the context of SMT solvers:
1) The unit cube test [2,3], a sound (although incomplete) test that finds solutions for integer programs(i.e., systems of linear inequalities) in polynomial time. The test is especially efficient on absolutely unbounded integer programs, which are difficult to handle for many other decision procedures.
2) A bounding transformation [1] that reduces any integer program in polynomial time to an equisatisfiable integer program that is bounded. The transformation is beneficial because it turns branch and bound into a complete and efficient decision procedure for integer programs.
References:
[1] A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems, Martin Bromberger. IJCAR 2018, volume 10900 of LNCS, pages 329–345. Springer, 2018.
[2] New Techniques for Linear Arithmetic: Cubes and Equalities, Martin Bromberger, and Christoph Weidenbach. In FMSD volume 51(3), pages 433–461. Springer, 2017.
[3] Fast Cube Tests for LIA Constraint Solving, Martin Bromberger, and Christoph Weidenbach. In IJCAR 2016, volume 9706 of LNCS, pages 116–132. Springer, 2016.
