Satisfiability Checking with Difference Constraints

Cotton, Scott

Datensatz

DATENSATZ AKTIONENEXPORT

DownloadE-Mail

Bitte beachten Sie, dass eine neuere Version dieses Datensatzes verfügbar ist:
https://pure.mpg.de/pubman/item/item_2173540_3

DetailsÜbersicht

Satisfiability Checking with Difference Constraints

Cotton, S. (2005). Satisfiability Checking with Difference Constraints. Master Thesis, Universität des Saarlandes, Saarbrücken.

Item is Freigegeben

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:

Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-0027-D5C9-C Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-0027-D5CA-A

Genre: Hochschulschrift

ausblenden:

Urheber:
Cotton, Scott¹, Autor
Podelski, Andreas², Ratgeber
Finkbeiner, Bernd³, Gutachter

Affiliations:
1International Max Planck Research School, MPI for Informatics, Max Planck Society, ou_1116551
2Programming Logics, MPI for Informatics, Max Planck Society, ou_40045
3External Organizations, ou_persistent22

Inhalt

einblenden:

ausblenden:

Schlagwörter: -

Zusammenfassung: This thesis studies the problem of determining the satisfiability of a Boolean combination of binary difference constraints of the form x-y <= c where x and y are numeric variables and c is a constant. In particular, we present an incremental and model-based interpreter for the theory of difference constraints in the context of a generic Boolean satisfiability checking procedure capable of incorporating interpreters for arbitrary theories. We show how to use the model based approach to efficiently make inferences with the option of complete inference.