Linear Arithmetic with Stars

10 years 8 months ago
Linear Arithmetic with Stars
We consider an extension of integer linear arithmetic with a "star" operator takes closure under vector addition of the solution set of a linear arithmetic subformula. We show that the satisfiability problem for this extended language remains in NP (and therefore NP-complete). Our proof uses semilinear set characterization of solutions of integer linear arithmetic formulas, as well as a generalization of a recent result on sparse solutions of integer linear programming problems. As a consequence of our result, we present worst-case optimal decision procedures for two NP-hard problems that were previously not known to be in NP. The first is the satisfiability problem for a logic of sets, multisets (bags), and cardinality constraints, which has applications in verification, interactive theorem proving, and description logics. The second is the reachability problem for a class of transition systems whose transitions increment the state vector by solutions of integer linear arith...
Ruzica Piskac, Viktor Kuncak
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where CAV
Authors Ruzica Piskac, Viktor Kuncak
Comments (0)