uu.seUppsala University Publications
Change search
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Towards Machine-Assisted Reformulation for MiniZinc
Uppsala University, Disciplinary Domain of Science and Technology, Mathematics and Computer Science, Department of Information Technology, Division of Computing Science.ORCID iD: 0000-0003-2106-7186
2020 (English)Licentiate thesis, monograph (Other academic)
Abstract [en]

Model reformulation plays an important role in improving models, reducing search space so that solutions can be found faster. Hence we categorise model reformulation into three types: a model is reformulated to another model with the same mod- elling language, a model with non constraint programming standard types is compiled to another model with constraint programming (CP) standard types, and a model is converted to Boolean satisfiability problem (SAT), Mixed-integer programming (MIP), Satisfiability modulo theories (SMT), and Mixed integer linear programming (MILP). Based on these categories, reformulation and compilation could be used in different ways to improve a model such as automatic reformulations, semi-automatic reformulations, MIP to constraint programming (CP), implied constraints, set Constraint Satisfaction Problems (CSPs) to CSPs, string variables to CSP without string variables, symmetry breaking, pre-computation, non-binary to binary translations, and reformulations into SAT, MILP, and SMT. CP is a pervasive and highly successful technology for solving a wide variety of constraint satisfaction problems (CSPs) such as air traffic management, resource allocation, transportation, scheduling, and so on. Model reformulation can have a significant impact on solving time. Techniques from formal methods will be used to provide machine assistance for MiniZinc, which is the high-level modelling language to model CSPs. In this thesis, we present an overview of reformulation focusing on the contributions made in the area of reformulation of CSPs where significant performance improvements have been achieved. According to criteria and types that categorise reformulation, we systematically unify and organise the vast literature as well as contrast and compare different categories of the reformulation for solving CSPs. Ultimately, we identify the challenges, implement frameworks, and evaluate our experimental results in reformulations for future research.

Place, publisher, year, edition, pages
Uppsala: Acta Universitatis Upsaliensis, 2020. , p. 77
Series
Information technology licentiate theses: Licentiate theses from the Department of Information Technology, ISSN 1404-5117
Keywords [en]
constraint programming, optimisation, counter automata, reformulation
National Category
Computer Sciences
Research subject
Computing Science; Computer Science with specialization in Real Time Systems
Identifiers
URN: urn:nbn:se:uu:diva-396968OAI: oai:DiVA.org:uu-396968DiVA, id: diva2:1382887
Presentation
2020-01-09, ITC.1213, Department of Information Technology, Polacksbacken (Lägerhyddsvägen 2), Uppsala, 15:15 (English)
Available from: 2020-01-13 Created: 2020-01-06 Last updated: 2020-01-13Bibliographically approved

Open Access in DiVA

No full text in DiVA

Search in DiVA

By author/editor
Huu-Phuc, Phuc
By organisation
Division of Computing Science
Computer Sciences

Search outside of DiVA

GoogleGoogle Scholar

urn-nbn

Altmetric score

urn-nbn
Total: 10 hits
CiteExportLink to record
Permanent link

Direct link
Cite
Citation style
  • apa
  • ieee
  • modern-language-association
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf