On Linear Arithmetic with Stars

paper ps   
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.

Citation

Ruzica Piskac and Viktor Kuncak. On linear arithmetic with stars. Technical Report LARA-REPORT-2008-005, EPFL, 2008.

BibTex Entry

@techreport{PiskacKuncak08OnLinearArithmeticwithStars,
  author = {Ruzica Piskac and Viktor Kuncak},
  title = {On Linear Arithmetic with Stars},
  institution = {EPFL},
  number = {LARA-REPORT-2008-005},
  year = 2008,
  abstract = {
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.
}
}