TY - GEN
T1 - A simplex-based extension of Fourier-Motzkin for solving linear integer arithmetic
AU - Bobot, François
AU - Conchon, Sylvain
AU - Contejean, Evelyne
AU - Iguernelala, Mohamed
AU - Mahboubi, Assia
AU - Mebsout, Alain
AU - Melquiond, Guillaume
PY - 2012
Y1 - 2012
N2 - 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 gap between the two techniques: it interleaves an exhaustive search for a model with bounds inference. These bounds are computed provided an oracle capable of finding constant positive linear combinations of affine forms. We also show how to design an efficient oracle based on the Simplex procedure. Our algorithm is proved sound, complete, and terminating and is implemented in the alt-ergo theorem prover. Experimental results are promising and show that our approach is competitive with state-of-the-art SMT solvers. © 2012 Springer-Verlag.
AB - 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 gap between the two techniques: it interleaves an exhaustive search for a model with bounds inference. These bounds are computed provided an oracle capable of finding constant positive linear combinations of affine forms. We also show how to design an efficient oracle based on the Simplex procedure. Our algorithm is proved sound, complete, and terminating and is implemented in the alt-ergo theorem prover. Experimental results are promising and show that our approach is competitive with state-of-the-art SMT solvers. © 2012 Springer-Verlag.
UR - http://www.scopus.com/inward/record.url?scp=84863618194&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-31365-3_8
DO - 10.1007/978-3-642-31365-3_8
M3 - Conference contribution
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 67
EP - 81
BT - Automated Reasoning - 6th International Joint Conference, IJCAR 2012, Proceedings
T2 - 6th International Joint Conference on Automated Reasoning, IJCAR 2012
Y2 - 26 June 2012 through 29 June 2012
ER -