A simplex-based extension of fourier-motzkin for solving linear integer arithmetic

IJCAR, pp. 67-81, 2012.

Cited by: 168|Bibtex|Views9|Links
EI
Keywords:
efficient oraclebounds inferencesimplex-based extensionaffine formexhaustive searchMore(6+)

Abstract:

This paper describes a novel decision procedure for quantifier-free linear integer arithmetic. Standard techniques usually relax the initial problem to the rational domain and then proceed either by projection (e.g.Omega-Test) or by branching/cutting methods (branch-and-bound, branch-and-cut, Gomory cuts). Our approach tries to bridge the...More

Code:

Data:

Your rating :
0

 

Tags
Comments