A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic

François Bobot 1, 2 Sylvain Conchon 2 Evelyne Contejean 2 Mohamed Iguernelala 2 Assia Mahboubi 3, 4, 5, 6 Alain Mebsout 2 Guillaume Melquiond 1, 2
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
2 LRI - Laboratoire de Recherche en Informatique
3 SPECFUN - Symbolic Special Functions : Fast and Certified
Inria Saclay - Ile de France
4 MSR - INRIA - Microsoft Research - Inria Joint Centre
5 TYPICAL - Types, Logic and computing
LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau], Inria Saclay - Ile de France, Polytechnique - X, CNRS - Centre National de la Recherche Scientifique : UMR
6 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
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 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.
Type de document :
Communication dans un congrès
Bernhard Gramlich and Dale Miller and Uli Sattler. 6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. Springer, 7364, pp.67-81, 2012, <10.1007/978-3-642-31365-3_8>
Liste complète des métadonnées

https://hal.inria.fr/hal-00687640
Contributeur : Guillaume Melquiond <>
Soumis le : lundi 16 avril 2012 - 19:08:01
Dernière modification le : jeudi 9 février 2017 - 15:06:29
Document(s) archivé(s) le : mercredi 14 décembre 2016 - 23:31:46

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | LIX | X-LIX | X | PARISTECH | X-DEP-INFO | UMR8623 | LRI-VALS | CENTRALESUPELEC

Citation

François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, et al.. A Simplex-Based Extension of Fourier-Motzkin for Solving Linear Integer Arithmetic. Bernhard Gramlich and Dale Miller and Uli Sattler. 6th International Joint Conference on Automated Reasoning, Jun 2012, Manchester, United Kingdom. Springer, 7364, pp.67-81, 2012, <10.1007/978-3-642-31365-3_8>. <hal-00687640v2>

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de
la notice

429

Téléchargements du document

544

Contact


archive-ouverte@inria.fr