Change search
ReferencesLink to record
Permanent link

Direct link
Other Things Besides Number: Abstraction, Constraint Propagation, and String Variable Types
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computing Science. Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Computing Science. (ASTRA)
2016 (English)Doctoral thesis, monograph (Other academic)
Abstract [en]

Constraint programming (CP) is a technology in which a combinatorial problem is modeled declaratively as a conjunction of constraints, each of which captures some of the combinatorial substructure of the problem. Constraints are more than a modeling convenience: every constraint is partially implemented by an inference algorithm, called a propagator, that rules out some but not necessarily all infeasible candidate values of one or more unknowns in the scope of the constraint. Interleaving propagation with systematic search leads to a powerful and complete solution method, combining a high degree of re-usability with natural, high-level modeling.

A propagator can be characterized as a sound approximation of a constraint on an abstraction of sets of candidate values; propagators that share an abstraction are similar in the strength of the inference they perform when identifying infeasible candidate values. In this thesis, we consider abstractions of sets of candidate values that may be described by an elegant mathematical formalism, the Galois connection. We develop a theoretical framework from the correspondence between Galois connections and propagators, unifying two disparate views of the abstraction-propagation connection, namely the oft-overlooked distinction between representational and computational over-approximations. Our framework yields compact definitions of propagator strength, even in complicated cases (i.e., involving several types, or unknowns with internal structure); it also yields a method for the principled derivation of propagators from constraint definitions.

We apply this framework to the extension of an existing CP solver to constraints over strings, that is, words of finite length. We define, via a Galois connection, an over-approximation for bounded-length strings, and demonstrate two different methods for implementing this overapproximation in a CP solver. First we use the Galois connection to derive a bounded-length string representation as an aggregation of existing scalar types; propagators for this representation are obtained by manual derivation, or automated synthesis, or a combination. Then we implement a string variable type, motivating design choices with knowledge gained from the construction of the over-approximation. The resulting CP solver extension not only substantially eases modeling for combinatorial string problems, but also leads to substantial efficiency improvements over prior CP methods.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2016. , 210 p.
Uppsala Dissertations from the Faculty of Science and Technology, ISSN 1104-2516 ; 120
Keyword [en]
constraint programming, string constraint problems, Galois connections, abstraction, constraint propagation, computer-aided verification applications
National Category
Computer Science
Research subject
Computer Science
URN: urn:nbn:se:uu:diva-273311ISBN: 978-91-554-9464-3OAI: diva2:897588
Public defence
2016-03-14, ITC room 2446, Polacksbacken, Lägerhyddsvägen 2, Uppsala, 13:15 (English)
Swedish Research Council, 2009-4384Swedish Research Council, 2011-6133Swedish Research Council, 2012-4908
Available from: 2016-02-22 Created: 2016-01-15 Last updated: 2016-03-09Bibliographically approved

Open Access in DiVA

fulltext(1908 kB)135 downloads
File information
File name FULLTEXT01.pdfFile size 1908 kBChecksum SHA-512
Type fulltextMimetype application/pdf
Buy this publication >>

Search in DiVA

By author/editor
Scott, Joseph
By organisation
Division of Computing ScienceComputing Science
Computer Science

Search outside of DiVA

GoogleGoogle Scholar
Total: 135 downloads
The number of downloads is the sum of all downloads of full texts. It may include eg previous versions that are now no longer available

Total: 2231 hits
ReferencesLink to record
Permanent link

Direct link