Browsing by Author "Bomanson, Jori"
Now showing 1 - 5 of 5
- Results Per Page
- Sort Options
- Applying Visible Strong Equivalence in Answer-Set Program Transformations
A1 Alkuperäisartikkeli tieteellisessä aikakauslehdessä(2020-10) Bomanson, Jori; Janhunen, Tomi; Niemelä, IlkkaStrong equivalence is one of the basic notions of equivalence that have been proposed for logic programs subject to the answer-set semantics. In this article, we propose a new generalization of strong equivalence (SE) that takes the visibility of atoms into account and we characterize it in terms of appropriately revised SE-models. Our design resembles (relativized) strong equivalence but is substantially different due to adopting a strict one-to-one correspondence of models from the notion of visible equivalence. We additionally tailor the characterization for more convenient use with positive programs and provide formal tools to exploit the tailored version also in the case of some programs that use negation. We illustrate the use of visible strong equivalence and the characterizations in showing the correctness of program transformations that make use of atom visibility. Moreover, we present a translation that enables us to automate the task of verifying visible strong equivalence for particular fragments of answer-set programs. We experimentally study the efficiency of verification when the goal is to check whether an extended rule is visibly strongly equivalent to its normalization, i.e., a subprogram expressing the original rule in terms of normal rules only. In the process, we verify the outputs of several real implementations of normalization schemes on a considerable number of input rules. - Developing Efficient Encodings for Weighted Expressions in Answer Set Programs
Perustieteiden korkeakoulu | Master's thesis(2014-08-21) Bomanson, JoriAnswer set programming is a declarative problem solving paradigm suitable for searching solutions to combinatorial search problems. Propositional answer set programs, studied in this thesis, consist of rules that state logical connections between atomic propositions, or atoms. A program represents the problem of finding truth assignments, called answer sets, that satisfy the rules in the program, under the condition that by default atoms are false. Answer set programming can be used as a general purpose problem solving mechanism, by writing programs whose answer sets correspond to solutions of a chosen search problem, and then using automated tools to find them. In this work, we focus on normalizing a particular type of rules, weight rules, into so called normal rules. We develop normalization strategies that extend existing translations applied in answer set programming and propositional satisfiability checking. In particular, we propose to incorporate a base selection heuristic and a structure sharing algorithm into a weight rule translation that decomposes the rule in a mixed-radix base. Both the previous and novel techniques have been implemented in a normalization tool, and we experimentally evaluate the effect of our methods on search performance. The proposed techniques improve on the compared normalization methods in terms of conciseness, the number of conflicts encountered during search, and the amount of time needed to find answer sets using a state-of-the-art solving back-end. On certain benchmark classes, the normalization techniques improve even on native weight-handling capabilities of the solver. - Nopea matriisikertolasku ja klikkien etsintä
Perustieteiden korkeakoulu | Bachelor's thesis(2012-08-04) Bomanson, Jori - Normalization and Rewriting for Answer Set Programming and Optimization
School of Science | Doctoral dissertation (article-based)(2020) Bomanson, JoriAnswer-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. - Rewriting optimization statements in answer-set programs
A4 Artikkeli konferenssijulkaisussa(2016-11-01) Bomanson, Jori; Gebser, Martin; Janhunen, TomiConstraints on Pseudo-Boolean (PB) expressions can be translated into Conjunctive Normal Form (CNF) using several known translations. In Answer-Set Programming (ASP), analogous expressions appear in weight rules and optimization statements. Previously, we have translated weight rules into normal rules, using normalizations designed in accord with existing CNF encodings. In this work, we rededicate such designs to rewrite optimization statements in ASP. In this context, a rewrite of an optimization statement is a replacement accompanied by a set of normal rules that together replicate the original meaning. The goal is partially the same as in translating PB constraints or weight rules: to introduce new meaningful auxiliary atoms that may help a solver in the search for (optimal) solutions. In addition to adapting previous translations, we present selective rewriting techniques in order to meet the above goal while using only a limited amount of new rules and atoms. We experimentally evaluate these methods in preprocessing ASP optimization statements and then searching for optimal answer sets. The results exhibit significant advances in terms of numbers of optimally solved instances, reductions in search conflicts, and shortened computation times. By appropriate choices of rewriting techniques, improvements are made on instances involving both small and large weights. In particular, we show that selective rewriting is paramount on benchmarks involving large weights.