Eingang zum Volltext

Urheberrechtshinweis / Copyright notice

Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URL: http://opus.kobv.de/zib/volltexte/2007/1038/

Achterberg, Tobias
Weitere Beteiligte (Hrsg. etc.): 1. Berichter: Grötschel, Martin; 2. Berichter: Bixby, Robert
TU Berlin, Diss., 2006

Constraint Integer Programming

pdf-Format:
Dokument 1.pdf (4.096 KB) (Revised Version 2008) Dokument 2.pdf (3.419 KB) (Orig. Vers. 2007)

Kurzfassung in Englisch

This thesis introduces the novel paradigm of constraint integer programming (CIP), which integrates constraint programming (CP) and mixed integer programming (MIP) modeling and solving techniques.
It is supplemented by the software SCIP, which is a solver and framework for constraint integer programming that also features SAT solving techniques.
SCIP is freely available in source code for academic and non-commercial purposes.

Our constraint integer programming approach is a generalization of MIP that allows for the inclusion of arbitrary constraints, as long as they turn into linear constraints on the continuous variables after all integer variables have
been fixed.
The constraints, may they be linear or more complex, are treated by any combination of CP and MIP techniques: the propagation of the domains by constraint specific algorithms, the generation of a linear relaxation and its solving by LP methods, and the strengthening of the LP by cutting plane separation.

The current version of SCIP comes with all of the necessary components to solve mixed integer programs.
In the thesis, we cover most of these ingredients and present extensive computational results to compare different variants for the individual building blocks of a MIP solver.
We focus on the algorithms and their impact on the overall performance of the solver.

In addition to mixed integer programming, the thesis deals with chip design verification, which is an important topic of electronic design automation.
Chip manufacturers have to make sure that the logic design of a circuit conforms to the specification of the chip.
Otherwise, the chip would show an erroneous behavior that may cause failures in the device where it is employed.
An important subproblem of chip design verification is the property checking problem, which is to verify whether a circuit satisfies a specified property.
We show how this problem can be modeled as constraint integer program and provide a number of problem-specific algorithms that exploit the structure of the individual constraints and the circuit as a whole.
Another set of extensive computational benchmarks compares our CIP approach to the current state-of-the-art SAT methodology and documents the success of our method.

Kurzfassung in Deutsch

Diese Arbeit stellt einen integrierten Ansatz aus Constraint Programming (CP) und Gemischt-Ganzzahliger Programmierung (Mixed Integer Programming, MIP) vor, den wir Constraint Integer Programming (CIP) nennen.
Sowohl Modellierungs- als auch Lösungstechniken beider Felder fließen in den neuen integrierten Ansatz ein, um die unterschiedlichen Stärken der beiden Gebiete zu kombinieren.
Als weiteren Beitrag stellen wir der wissenschaftlichen Gemeinschaft die Software SCIP zur Verfügung, die ein Framework für Constraint Integer Programming darstellt und zusätzlich Techniken des SAT-Lösens beinhaltet.
SCIP ist im Source Code für akademische und nicht-kommerzielle Zwecke frei erhältlich.

Unser Ansatz des Constraint Integer Programming ist eine Verallgemeinerung von MIP, die zusätzlich die Verwendung beliebiger Constraints erlaubt, solange sich diese durch lineare Bedingungen ausdrücken lassen falls alle ganzzahligen Variablen auf feste Werte eingestellt sind.
Die Constraints werden von einer beliebigen Kombination aus CP- und MIP-Techniken behandelt.
Dies beinhaltet insbesondere die Domain Propagation, die Relaxierung der Constraints durch lineare Ungleichungen, sowie die Verstärkung der Relaxierung durch dynamisch generierte Schnittebenen.

Die derzeitige Version von SCIP enthält alle Komponenten, die für das effiziente Lösen von Gemischt-Ganzzahligen Programmen benötigt werden.
Die vorliegende Arbeit liefert eine ausführliche Beschreibung dieser Komponenten und bewertet verschiedene Varianten in Hinblick auf ihren Einfluß auf das Gesamt-Lösungsverhalten anhand von aufwendigen praktischen Experimenten.
Dabei wird besonders auf die algorithmischen Aspekte eingegangen.

Der zweite Hauptteil der Arbeit befasst sich mit der Chip-Design-Verifikation, die ein wichtiges Thema innerhalb des Fachgebiets der Electronic Design Automation darstellt.
Chip-Hersteller müssen sicherstellen, dass der logische Entwurf einer Schaltung der gegebenen Spezifikation entspricht.
Andernfalls würde der Chip fehlerhaftes Verhalten aufweisen, dass zu Fehlfunktionen innerhalb des Gerätes führen kann, in dem der Chip verwendet wird.
Ein wichtiges Teilproblem in diesem Feld ist das Eigenschafts-Verifikations-Problem, bei dem geprüft wird, ob der gegebene Schaltkreisentwurf eine gewünschte Eigenschaft aufweist.
Wir zeigen, wie dieses Problem als Constraint Integer Program modelliert werden kann und geben eine Reihe von problemspezifischen Algorithmen an, die die Struktur der einzelnen Constraints und der Gesamtschaltung ausnutzen.
Testrechnungen auf Industrie-Beispielen vergleichen unseren Ansatz mit den bisher verwendeten SAT-Techniken und belegen den Erfolg unserer Methode.

Freie Schlagwörter (deutsch): Ganzzahlige Programmierung , Constraint Programmierung , SAT , Chip-Verifikation
Freie Schlagwörter (englisch): integer programming , constraint programming , SAT , chip verification
CCS - Klassifikation G.1.6
CCS - Klassifikation B.8.1
MSC - Klassifikation 90C11
MSC - Klassifikation 90C10
Collection ZIB / Dissertationen
Abteilung: Optimierung
DDC-Sachgruppe: Mathematik
Dokumentart: Examensarbeit
Sprache: Englisch
Erstellungsjahr: 2007
Publikationsdatum: 15.10.2007

Metadatensuche | Volltextsuche | Browsen | Die neuesten Publikationen | Veröffentlichen
Fragen und Anregungen an bibliothek@zib.de
Letzte Änderung: