A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems

Abstract : We present a combination of the Mixed-Echelon-Hermite transformation and the Double-Bounded Reduction for systems of linear mixed arithmetic that preserve satisfiability and can be computed in polynomial time. Together, the two transformations turn any system of linear mixed constraints into a bounded system, i.e., a system for which termination can be achieved easily. Existing approaches for linear mixed arithmetic, e.g., branch-and-bound and cuts from proofs, only explore a finite search space after application of our two transformations. Instead of generating a priori bounds for the variables, e.g., as suggested by Papadimitriou, unbounded variables are eliminated through the two transformations. The transformations orient themselves on the structure of an input system instead of computing a priori (over- )approximations out of the available constants. Experiments provide further evidence to the efficiency of the transformations in practice. We also present a polynomial method for converting certificates of (un)satisfiability from the transformed to the original system.
Type de document :
Communication dans un congrès
Didier Galmiche; Stephan Schulz; Roberto Sebastiani. IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. Springer, 10900, pp.329-345, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/hal-01942228
Contributeur : Stephan Merz <>
Soumis le : lundi 3 décembre 2018 - 09:27:04
Dernière modification le : mardi 11 décembre 2018 - 11:26:41

Fichier

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

Identifiants

  • HAL Id : hal-01942228, version 1

Collections

Citation

Martin Bromberger. A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems. Didier Galmiche; Stephan Schulz; Roberto Sebastiani. IJCAR 2018 - 9th International Joint Conference on Automated Reasoning, Jul 2018, Oxford, United Kingdom. Springer, 10900, pp.329-345, Lecture Notes in Computer Science. 〈hal-01942228〉

Partager

Métriques

Consultations de la notice

11

Téléchargements de fichiers

6