Solving LIA⋆ Constraints Using Hilbert Bases

Abstract

LIA⋆, a theory of linear integer arithmetic extended with unbounded sums over values satisfying given linear integer arithmetic formulas, was introduced in 2008 by Piskac and Kunˇcak to support reasoning in the theory of multisets with cardinality. They presented a decision procedure for quantifier-free LIA⋆ constraints based on the computation of semilinear sets. While that procedure is inefficient in practice, efficient procedures based on over- and under-approximations of quantifier-free LIA⋆ constraints were eventually developed and are currently implemented in the tools SLS-reachability and SQLSolver. We present a method for solving LIA⋆ constraints that relies on the computation of Hilbert bases and module generators for LIA formulas. The method can be fully integrated into CDCL(T)- style SMT solvers supporting linear integer arithmetic. We have implemented it in the SMT solver cvc5, which did not previously support LIA⋆ reasoning. The integration in cvc5 benefits from features like model generation and proof production, which are not available in the other tools. We discuss an initial experimental evaluation where cvc5’s performance on a sizable benchmark set is superior to that of SQLSolver and SLS-reachability.