非表示:
キーワード:
Computer Science, Logic in Computer Science, cs.LO
要旨:
We consider feasibility of linear integer programs in the context of
verification systems such as SMT solvers or theorem provers. Although
satisfiability of linear integer programs is decidable, many state-of-the-art
solvers neglect termination in favor of efficiency. It is challenging to design
a solver that is both terminating and practically efficient. Recent work by
Jovanovic and de Moura constitutes an important step into this direction. Their
algorithm CUTSAT is sound, but does not terminate, in general. In this paper we
extend their CUTSAT algorithm by refined inference rules, a new type of
conflicting core, and a dedicated rule application strategy. This leads to our
algorithm CUTSAT++, which guarantees termination.
