list | abstracts | bib ]

Linear Arithmetic with Stars

paper pdf    paper ps   

Abstract

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 arithmetic formulas.

Citation

Ruzica Piskac and Viktor Kuncak. Linear arithmetic with stars. In Computed-Aided Verification (CAV), volume 5123 of LNCS, 2008.

BibTex Entry

@INPROCEEDINGS{PiskacKuncak08LinearArithmeticwithStars,
  author = {Ruzica Piskac and Viktor Kuncak},
  title = {Linear Arithmetic with Stars},
  booktitle = {Computed-Aided Verification (CAV)},
  year = 2008,
  series = {LNCS},
  volume = {5123},
  localurl = {http://lara.epfl.ch/~kuncak/papers/PiskacKuncak08LinearArithmeticwithStars.pdf}
}

list | abstracts | bib ]