Fast Cube Tests for LIA Constraint Solving

Abstract : We present two tests that solve linear integer arithmetic constraints. These tests are sound and efficiently find solutions for a large number of problems. While many complete methods search along the problem surface for a solution, these tests use cubes to explore the interior of the problems. The tests are especially efficient for constraints with a large number of integer solutions, e.g., those with infinite lattice width. Inside the SMT-LIB benchmarks, we have found almost one thousand problem instances with infinite lattice width, and we have shown the advantage of our cube tests on these instances by comparing our implementation of the cube test with several state-of-the-art SMT solvers. Our implementation is not only several orders of magnitudes faster, but it also solves all instances, which most SMT solvers do not. Finally, we discovered an additional application for our cube tests: the extraction of equalities implied by a system of linear arithmetic inequalities. This extraction is useful both as a preprocessing step for linear integer constraint solving as well as for the combination of theories by the Nelson-Oppen method.
Type de document :
Communication dans un congrès
Nicola Olivetti and Ashish Tiwari. Automated Reasoning - 8th International Joint Conference (IJCAR 2016), 2016, Coimbra, Portugal. Springer, 9706, pp.116-132, 2016, Lecture Notes in Computer Science. 〈10.1007/978-3-319-40229-1_9〉
Liste complète des métadonnées

Littérature citée [16 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01403200
Contributeur : Stephan Merz <>
Soumis le : vendredi 25 novembre 2016 - 15:11:56
Dernière modification le : lundi 20 novembre 2017 - 15:14:02
Document(s) archivé(s) le : mardi 21 mars 2017 - 05:11:45

Fichier

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

Identifiants

Collections

Citation

Martin Bromberger, Christoph Weidenbach. Fast Cube Tests for LIA Constraint Solving. Nicola Olivetti and Ashish Tiwari. Automated Reasoning - 8th International Joint Conference (IJCAR 2016), 2016, Coimbra, Portugal. Springer, 9706, pp.116-132, 2016, Lecture Notes in Computer Science. 〈10.1007/978-3-319-40229-1_9〉. 〈hal-01403200〉

Partager

Métriques

Consultations de la notice

101

Téléchargements de fichiers

36