Answer 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.
展开▼
