Please use this identifier to cite or link to this item: doi:10.22028/D291-30636
Title: Decision procedures for linear arithmetic
Author(s): Bromberger, Martin
Language: English
Year of Publication: 2019
DDC notations: 004 Computer science, internet
Publikation type: Doctoral Thesis
Abstract: In this thesis, we present new decision procedures for linear arithmetic in the context of SMT solvers and theorem provers: 1) CutSat++, a calculus for linear integer arithmetic that combines techniques from SAT solving and quantifier elimination in order to be sound, terminating, and complete. 2) The largest cube test and the unit cube test, two sound (although incomplete) tests that find integer and mixed solutions in polynomial time. The tests are especially efficient on absolutely unbounded constraint systems, which are difficult to handle for many other decision procedures. 3) Techniques for the investigation of equalities implied by a constraint system. Moreover, we present several applications for these techniques. 4) The Double-Bounded reduction and the Mixed-Echelon-Hermite transformation, two transformations that reduce any constraint system in polynomial time to an equisatisfiable constraint system that is bounded. The transformations are beneficial because they turn branch-and-bound into a complete and efficient decision procedure for unbounded constraint systems. We have implemented the above decision procedures (except for Cut- Sat++) as part of our linear arithmetic theory solver SPASS-IQ and as part of our CDCL(LA) solver SPASS-SATT. We also present various benchmark evaluations that confirm the practical efficiency of our new decision procedures.
In dieser Arbeit präsentieren wir neue Entscheidungsprozeduren für lineare Arithmetik im Kontext von SMT-Solvern und Theorembeweisern: 1) CutSat++, ein korrekter und vollständiger Kalkül für ganzzahlige lineare Arithmetik, der Techniken zur Entscheidung von Aussagenlogik mit Techniken aus der Quantorenelimination vereint. 2) Der Größte-Würfeltest und der Einheitswürfeltest, zwei korrekte (wenn auch unvollständige) Tests, die in polynomieller Zeit (gemischt-)ganzzahlige Lösungen finden. Die Tests sind besonders effizient auf vollständig unbegrenzten Systemen, welche für viele andere Entscheidungsprozeduren schwer sind. 3) Techniken zur Ermittlung von Gleichungen, die von einem linearen Ungleichungssystem impliziert werden. Des Weiteren präsentieren wir mehrere Anwendungsmöglichkeiten für diese Techniken. 4) Die Beidseitig-Begrenzte-Reduktion und die Gemischte-Echelon-Hermitesche- Transformation, die ein Ungleichungssystem in polynomieller Zeit auf ein erfüllbarkeitsäquivalentes System reduzieren, das begrenzt ist. Vereint verwandeln die Transformationen Branch-and-Bound in eine vollständige und effiziente Entscheidungsprozedur für unbeschränkte Ungleichungssysteme. Wir haben diese Techniken (ausgenommen CutSat++) in SPASS-IQ (unserem theory solver für lineare Arithmetik) und in SPASS-SATT (unserem CDCL(LA) solver) implementiert. Basierend darauf präsentieren wir Benchmark-Evaluationen, die die Effizienz unserer Entscheidungsprozeduren bestätigen.
Link to this record: urn:nbn:de:bsz:291--ds-306363
hdl:20.500.11880/28955
http://dx.doi.org/10.22028/D291-30636
Advisor: Weidenbach, Christoph
Date of oral examination: 10-Dec-2019
Date of registration: 6-Apr-2020
Faculty: MI - Fakultät für Mathematik und Informatik
Department: MI - Informatik
Professorship: MI - Keiner Professur zugeordnet
Collections:SciDok - Der Wissenschaftsserver der Universität des Saarlandes

Files for this record:
File Description SizeFormat 
thesis_bromberger_v20200224.pdf6,18 MBAdobe PDFView/Open


Items in SciDok are protected by copyright, with all rights reserved, unless otherwise indicated.