Loop untangling

Kathryn Francis, Peter J. Stuckey

Research output: Chapter in Book/Report/Conference proceedingConference PaperResearchpeer-review

1 Citation (Scopus)

Abstract

An effective translation from procedural code into equivalent constraints is necessary in order to facilitate automated reasoning about the behaviour of programs. We consider the translation of bounded loops, proposing a new form of loop unwinding called loop untangling. In comparison to standard loop unwinding the constraints representing each iteration of the loop are greatly simplified. This is achieved by decoupling the execution order from the representation of each individual iteration. We illustrate this new technique using two different examples and provide experimental results verifying that the technique produces simpler models which result in much better solver performance.

Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming
Subtitle of host publication20th International Conference, CP 2014 Lyon, France, September 8-12, 2014 Proceedings
EditorsBarry O’Sullivan
Place of PublicationCham Switzerland
PublisherSpringer
Pages340-355
Number of pages16
ISBN (Electronic)9783319104287
ISBN (Print)9783319104270
DOIs
Publication statusPublished - 2014
Externally publishedYes
EventInternational Conference on Principles and Practice of Constraint Programming 2014 - Lyon, France
Duration: 8 Sept 201412 Sept 2014
Conference number: 20th
http://cp2014.a4cp.org/

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume8656
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceInternational Conference on Principles and Practice of Constraint Programming 2014
Abbreviated titleCP 2014
Country/TerritoryFrance
CityLyon
Period8/09/1412/09/14
Internet address

Cite this