On Linear Arithmetic with Stars

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.


Year:
2008
Keywords:
Laboratories:




 Record created 2008-02-09, last modified 2018-03-17

n/a:
Download fulltext
PDF

Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)