Normalization and Rewriting for Answer Set Programming and Optimization

Jori Bomanson

Normalization and Rewriting for Answer Set Programming and Optimization

Julkaisun otsikon käännös: Sääntöpohjaisten haku- ja optimointiohjelmien normalisointi ja uudelleenkirjoitus

Jori Bomanson

Tutkimustuotos: Doctoral Thesis › Collection of Articles

Abstrakti

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.

Julkaisun otsikon käännös	Sääntöpohjaisten haku- ja optimointiohjelmien normalisointi ja uudelleenkirjoitus
Alkuperäiskieli	Englanti
Pätevyys	Tohtorintutkinto
Myöntävä instituutio	Aalto-yliopisto
Valvoja/neuvonantaja	Niemelä, Ilkka, Vastuuprofessori Gebser, Martin, Ohjaaja Janhunen, Tomi, Ohjaaja
Kustantaja	Aalto University
Painoksen ISBN	978-952-64-0078-5
Sähköinen ISBN	978-952-64-0079-2
Tila	Julkaistu - 2020
OKM-julkaisutyyppi	G5 Tohtorinväitöskirja (artikkeli)

Tutkimusalat

laskennallinen logiikka
logiikkaohjelmointi

Pääsy asiakirjaan

http://urn.fi/URN:ISBN:978-952-64-0079-2

OpenUrl-saatavuus

Koko teksti

Science-IT
Mikko Hakala (Manager)
Perustieteiden korkeakoulu
Laitteistot/tilat: Facility

Siteeraa tätä

@phdthesis{ebbee13f1ddf449f8209084f408c50ab,

title = "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.",

keywords = "computational logic, logic programming, laskennallinen logiikka, logiikkaohjelmointi, computational logic, logic programming",

author = "Jori Bomanson",

year = "2020",

language = "English",

isbn = "978-952-64-0078-5",

series = "Aalto University publication series DOCTORAL DISSERTATIONS",

publisher = "Aalto University",

number = "157",

address = "Finland",

school = "Aalto University",

}

TY - THES

T1 - Normalization and Rewriting for Answer Set Programming and Optimization

AU - Bomanson, Jori

PY - 2020

Y1 - 2020

N2 - 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.

AB - 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.

KW - computational logic

KW - logic programming

KW - laskennallinen logiikka

KW - logiikkaohjelmointi

KW - computational logic

KW - logic programming

M3 - Doctoral Thesis

SN - 978-952-64-0078-5

T3 - Aalto University publication series DOCTORAL DISSERTATIONS

PB - Aalto University

ER -

Normalization and Rewriting for Answer Set Programming and Optimization

Abstrakti

Tutkimusalat

Pääsy asiakirjaan

OpenUrl-saatavuus

Sormenjälki

Laitteet

Science-IT

Siteeraa tätä