Normalization and Rewriting for Answer Set Programming and Optimization

Loading...
Thumbnail Image

URL

Journal Title

Journal ISSN

Volume Title

School of Science | Doctoral thesis (article-based) | Defence date: 2020-10-30

Date

2020

Major/Subject

Mcode

Degree programme

Language

en

Pages

102 + app. 126

Series

Aalto University publication series DOCTORAL DISSERTATIONS, 157/2020

Abstract

Answer-set programming (ASP) is an automated problem-solving paradigm specifically suitable for combinatorial search and optimization problems. Such problems can be solved both in theory and also increasingly in practice by ASP technology. The purpose of this dissertation is to contribute to ASP technology and particularly to the efficiency of ASP solving tools. In more detail, the contributions of this thesis focus on ASP optimization algorithms as well as ASP search algorithms based on so-called lazy-grounding. To these ends, several methods are proposed and shown theoretically and experimentally to have measurable performance increasing potential. The methods belong to two novel classes of ASP transformations: optimization rewritings, aimed at enhancing optimization performance, and firstorder lazy-normalizations aimed at extending the applicability of lazy-grounding in general. On the topic of transformations, this dissertation moreover presents novel systematic ways to test and verify the correctness of certain types of ASP transformations. These verification methods are distinct in the way they compare programs, which has been designed to reflect the behavior of standard ASP solvers to be as practically relevant as possible. Regarding practical optimization performance, the value of this work is substantial as evidenced by the excellent optimization performance of the proposed techniques in the highly competitive ASP Competition series. In particular, early versions of the techniques attained first place in the optimization track of the sixth edition of the series [56]. Moreover, the included work on lazy-grounding removed an obstacle previously preventing lazy-grounding from being applied to broad classes of programs that are central to the ASP paradigm.

Sääntöpohjainen rajoiteohjelmointi (answer-set programming, ASP) on kombinatoristen haku- ja optimointiongelmien laskennallinen ratkaisukeino. Tällaisia ongelmia voidaan ratkaista ASP-pohjaisilla algoritmeilla sekä teoriassa että monesti käytännössäkin. Tämän väitöskirjan tavoite on edistää ASP-menetelmien tehokkuutta keskittymällä toisaalta optimointialgoritmeihin ja toisaalta sellaisiinhakualgoritmeihin, jotka instantioivat muuttujia laiskasti (lazy-grounding). Tehokkuuden lisäämiseksi väitöskirjassa kuvataan useita uusia menetelmiä sekä todisteita näiden menetelmien tehokkuudesta. Näihin todisteisiin lukeutuu sekä teoreettisia tarkasteluita että laskennallisia kokeita. Nämä kuvatut menetelmät perustuvat ASP-ohjelmamuunnoksiin, jotka jakautuvat kahteen uuteen luokkaan: optimointiehtojen uudelleenkirjoittamiseen (optimization rewriting) optimointitehokkuuden lisäämiseksi ja ensimmäisen kertaluokan laiskaan normalisointiin(first-order lazy-normalization) laiskojen hakualgoritmien sovellettavuuden laajentamiseksi. Ohjelmamuunnoksien lisäksi väitöskirjassa esitellään uusia varmennuskeinoja ASP-ohjelmamuunnoksien oikeellisuudelle. Nämä esitetyt varmennuskeinot ovat poikkeuksellisia niiden käytännönläheisen ohjelmien vertailutavan vuoksi. Tämän työn tuottamilla tuloksilla on huomattava vaikutus optimointitehokkuuteen. Kyseiset parannukset ovatkin siivittäneet niihin perustuvan ASP-ratkaisinohjelman ensimmäiselle sijalle ASP-toteutusten suorituskykyvertailun optimointikategoriassa [56]. Väitöskirjassa esistetyt laiskojen hakualgoritmien laajennukset kattoivat keskeisiä ASP-ohjelmaluokkia, joitaniillä ei aiemmin ole kyetty ratkomaan.

Description

Supervising professor

Niemelä, Ilkka, Prof., Aalto University, Finland

Thesis advisor

Gebser, Martin, Prof., University of Klagenfurt, Austria
Janhunen, Tomi, Prof., Aalto University, Finland

Keywords

computational logic, logic programming, laskennallinen logiikka, logiikkaohjelmointi

Other note

Parts

  • [Publication 1]: Jori Bomanson. LP2NORMAL — A Normalization Tool for Extended Logic Programs. In Proceedings of the 14th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR 2017), Espoo, Finland, July 3-6, 2017. 222–228, August 2017.
    DOI: 10.1007/978-3-319-61660-5_20 View at publisher
  • [Publication 2]: Jori Bomanson, Tomi Janhunen, and Ilkka Niemelä. Applying Visible Strong Equivalence in Answer-Set Program Transformations. Accepted for publication in ACM Transactions on Computational Logic (ACM TOCL), 1–40, July 2020.
    DOI: 10.1007/978-3-642-30743-0_24 View at publisher
  • [Publication 3]: Jori Bomanson, Tomi Janhunen, and Antonius Weinzierl. Enhancing Lazy Grounding with Lazy Normalization in Answer-Set Programming. In Proceedings of the 33rd AAAI Conference on Artificial Intelligence (AAAI 2019), Honolulu, Hawaii, USA, January 27-February 1, 2019. 694–2702,June 2019.
    DOI: 10.1609/aaai.v33i01.33012694 View at publisher
  • [Publication 4]: Jori Bomanson, Martin Gebser, Tomi Janhunen. Rewriting Optimization Statements in Answer-Set Programs. In Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016 TCs), New York City, USA, October 16-21, 2016. 5:1–5:15, December 2016.
    Full text in Acris/Aaltodoc: http://urn.fi/URN:NBN:fi:aalto-201705113891
    DOI: 10.4230/OASIcs.ICLP.2016.5 View at publisher
  • [Publication 5]: Jori Bomanson and Tomi Janhunen. Boosting Answer Set Optimization with Weighted Comparator Networks. Theory and Practice of Logic Programming (TPLP), 1–40, May 2020.
    DOI: 10.1017/S147106842000006X View at publisher

Citation