Ruzica Piskac and Viktor Kuncak.
On linear arithmetic with stars.
Technical Report LARA-REPORT-2008-005, EPFL, 2008.
We consider an extension of integer linear arithmetic with a
star operator that takes closure under vector addition of
the set of solutions of linear arithmetic subformula. We
show that the satisfiability problem for this language is in
NP (and therefore NP-complete). Our proof uses a
generalization of a recent result on sparse solutions of
integer linear programming problems. We present two
consequences of our result. The first one is an optimal
decision procedure for a logic of sets,
multisets, and cardinalities that has applications in
verification, interactive theorem proving, and description
logics. The second is NP-completeness of the
reachability problem for a class of “homogeneous”
transition systems whose transitions are defined using
integer linear arithmetic formulas.
[ bib ]
Back