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