Normalization and Rewriting for Answer Set Programming and Optimization

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.