A simplex-based extension of fourier-motzkin for solving linear integer arithmetic
IJCAR, pp. 67-81, 2012.
efficient oraclebounds inferencesimplex-based extensionaffine formexhaustive searchMore(6+)
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
Full Text (Upload PDF)
PPT (Upload PPT)