TY  - JOUR
A1  - Fandinno, Jorge
A1  - Laferriere, Francois
A1  - Romero, Javier
A1  - Schaub, Torsten H.
A1  - Son, Tran Cao
T1  - Planning with incomplete information in quantified answer set programming
JF  - Theory and practice of logic programming
N2  - We present a general approach to planning with incomplete information in Answer Set Programming (ASP). More precisely, we consider the problems of conformant and conditional planning with sensing actions and assumptions. We represent planning problems using a simple formalism where logic programs describe the transition function between states, the initial states and the goal states. For solving planning problems, we use Quantified Answer Set Programming (QASP), an extension of ASP with existential and universal quantifiers over atoms that is analogous to Quantified Boolean Formulas (QBFs). We define the language of quantified logic programs and use it to represent the solutions different variants of conformant and conditional planning. On the practical side, we present a translation-based QASP solver that converts quantified logic programs into QBFs and then executes a QBF solver, and we evaluate experimentally the approach on conformant and conditional planning benchmarks.
KW  - answer set programming
KW  - planning
KW  - quantified logics
Y1  - 2021
U6  - https://doi.org/10.1017/S1471068421000259
SN  - 1471-0684
SN  - 1475-3081
VL  - 21
IS  - 5
SP  - 663
EP  - 679
PB  - Cambridge University Press
CY  - Cambridge
ER  - 
TY  - JOUR
A1  - Everardo Pérez, Flavio Omar
A1  - Osorio, Mauricio
T1  - Towards an answer set programming methodology for constructing programs following a semi-automatic approach
BT  - extended and revised version
JF  - Electronic notes in theoretical computer science
N2  - Answer Set Programming (ASP) is a successful rule-based formalism for modeling and solving knowledge-intense combinatorial (optimization) problems. Despite its success in both academic and industry, open challenges like automatic source code optimization, and software engineering remains. This is because a problem encoded into an ASP might not have the desired solving performance compared to an equivalent representation. Motivated by these two challenges, this paper has three main contributions. First, we propose a developing process towards a methodology to implement ASP programs, being faithful to existing methods. Second, we present ASP encodings that serve as the basis from the developing process. Third, we demonstrate the use of ASP to reverse the standard solving process. That is, knowing answer sets in advance, and desired strong equivalent properties, “we” exhaustively reconstruct ASP programs if they exist. This paper was originally motivated by the search of propositional formulas (if they exist) that represent the semantics of a new aggregate operator. Particularly, a parity aggregate. This aggregate comes as an improvement from the already existing parity (xor) constraints from xorro, where lacks expressiveness, even though these constraints fit perfectly for reasoning modes like sampling or model counting. To this end, this extended version covers the fundaments from parity constraints as well as the xorro system. Hence, we delve a little more in the examples and the proposed methodology over parity constraints. Finally, we discuss our results by showing the only representation available, that satisfies different properties from the classical logic xor operator, which is also consistent with the semantics of parity constraints from xorro.
KW  - answer set programming
KW  - combinatorial optimization problems
KW  - parity aggregate operator
Y1  - 2020
U6  - https://doi.org/10.1016/j.entcs.2020.10.004
SN  - 1571-0661
VL  - 354
SP  - 29
EP  - 44
PB  - Elsevier
CY  - Amsterdam [u.a.]
ER  - 
TY  - JOUR
A1  - Gebser, Martin
A1  - Janhunen, Tomi
A1  - Rintanen, Jussi
T1  - Declarative encodings of acyclicity properties
JF  - Journal of logic and computation
N2  - Many knowledge representation tasks involve trees or similar structures as abstract datatypes. However, devising compact and efficient declarative representations of such structural properties is non-obvious and can be challenging indeed. In this article, we take a number of acyclicity properties into consideration and investigate various logic-based approaches to encode them. We use answer set programming as the primary representation language but also consider mappings to related formalisms, such as propositional logic, difference logic and linear programming. We study the compactness of encodings and the resulting computational performance on benchmarks involving acyclic or tree structures.
KW  - acyclicity properties
KW  - logic-based modeling
KW  - answer set programming
KW  - satisfiability
Y1  - 2015
U6  - https://doi.org/10.1093/logcom/exv063
SN  - 0955-792X
SN  - 1465-363X
VL  - 30
IS  - 4
SP  - 923
EP  - 952
PB  - Oxford Univ. Press
CY  - Eynsham, Oxford
ER  - 
TY  - GEN
A1  - Fandinno, Jorge
T1  - Founded (auto)epistemic equilibrium logic satisfies epistemic splitting
T2  - Postprints der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe
N2  - In a recent line of research, two familiar concepts from logic programming semantics (unfounded sets and splitting) were extrapolated to the case of epistemic logic programs. The property of epistemic splitting provides a natural and modular way to understand programs without epistemic cycles but, surprisingly, was only fulfilled by Gelfond's original semantics (G91), among the many proposals in the literature. On the other hand, G91 may suffer from a kind of self-supported, unfounded derivations when epistemic cycles come into play. Recently, the absence of these derivations was also formalised as a property of epistemic semantics called foundedness. Moreover, a first semantics proved to satisfy foundedness was also proposed, the so-called Founded Autoepistemic Equilibrium Logic (FAEEL). In this paper, we prove that FAEEL also satisfies the epistemic splitting property something that, together with foundedness, was not fulfilled by any other approach up to date. To prove this result, we provide an alternative characterisation of FAEEL as a combination of G91 with a simpler logic we called Founded Epistemic Equilibrium Logic (FEEL), which is somehow an extrapolation of the stable model semantics to the modal logic S5.
T3  - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - 1060 
KW  - answer set programming
KW  - epistemic specifications
KW  - epistemic logic programs
Y1  - 2020
U6  - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-469685
SN  - 1866-8372
IS  - 1060
SP  - 671
EP  - 687
ER  - 
TY  - JOUR
A1  - Dimopoulos, Yannis
A1  - Gebser, Martin
A1  - Lühne, Patrick
A1  - Romero Davila, Javier
A1  - Schaub, Torsten H.
T1  - plasp 3
BT  - Towards Effective ASP Planning
JF  - Theory and practice of logic programming
N2  - We describe the new version of the Planning Domain Definition Language (PDDL)-to-Answer Set Programming (ASP) translator plasp. First, it widens the range of accepted PDDL features. Second, it contains novel planning encodings, some inspired by Satisfiability Testing (SAT) planning and others exploiting ASP features such as well-foundedness. All of them are designed for handling multivalued fluents in order to capture both PDDL as well as SAS planning formats. Third, enabled by multishot ASP solving, it offers advanced planning algorithms also borrowed from SAT planning. As a result, plasp provides us with an ASP-based framework for studying a variety of planning techniques in a uniform setting. Finally, we demonstrate in an empirical analysis that these techniques have a significant impact on the performance of ASP planning.
KW  - knowledge representation and nonmonotonic reasoning
KW  - technical notes and rapid communications
KW  - answer set programming
KW  - automated planning
KW  - action and change
Y1  - 2019
U6  - https://doi.org/10.1017/S1471068418000583
SN  - 1471-0684
SN  - 1475-3081
VL  - 19
IS  - 3
SP  - 477
EP  - 504
PB  - Cambridge Univ. Press
CY  - New York
ER  - 
TY  - JOUR
A1  - Frioux, Clémence
A1  - Schaub, Torsten H.
A1  - Schellhorn, Sebastian
A1  - Siegel, Anne
A1  - Wanko, Philipp
T1  - Hybrid metabolic network completion
JF  - Theory and practice of logic programming
N2  - Metabolic networks play a crucial role in biology since they capture all chemical reactions in an organism. While there are networks of high quality for many model organisms, networks for less studied organisms are often of poor quality and suffer from incompleteness. To this end, we introduced in previous work an answer set programming (ASP)-based approach to metabolic network completion. Although this qualitative approach allows for restoring moderately degraded networks, it fails to restore highly degraded ones. This is because it ignores quantitative constraints capturing reaction rates. To address this problem, we propose a hybrid approach to metabolic network completion that integrates our qualitative ASP approach with quantitative means for capturing reaction rates. We begin by formally reconciling existing stoichiometric and topological approaches to network completion in a unified formalism. With it, we develop a hybrid ASP encoding and rely upon the theory reasoning capacities of the ASP system dingo for solving the resulting logic program with linear constraints over reals. We empirically evaluate our approach by means of the metabolic network of Escherichia coli. Our analysis shows that our novel approach yields greatly superior results than obtainable from purely qualitative or quantitative approaches.
KW  - answer set programming
KW  - metabolic network
KW  - gap-filling
KW  - linear programming
KW  - hybrid solving
KW  - bioinformatics
Y1  - 2018
U6  - https://doi.org/10.1017/S1471068418000455
SN  - 1471-0684
SN  - 1475-3081
VL  - 19
IS  - 1
SP  - 83
EP  - 108
PB  - Cambridge University Press
CY  - New York
ER  - 
TY  - JOUR
A1  - Gebser, Martin
A1  - Obermeier, Philipp
A1  - Schaub, Torsten H.
A1  - Ratsch-Heitmann, Michel
A1  - Runge, Mario
T1  - Routing driverless transport vehicles in car assembly with answer set programming
JF  - Theory and practice of logic programming
N2  - Automated storage and retrieval systems are principal components of modern production and warehouse facilities. In particular, automated guided vehicles nowadays substitute human-operated pallet trucks in transporting production materials between storage locations and assembly stations. While low-level control systems take care of navigating such driverless vehicles along programmed routes and avoid collisions even under unforeseen circumstances, in the common case of multiple vehicles sharing the same operation area, the problem remains how to set up routes such that a collection of transport tasks is accomplished most effectively. We address this prevalent problem in the context of car assembly at Mercedes-Benz Ludwigsfelde GmbH, a large-scale producer of commercial vehicles, where routes for automated guided vehicles used in the production process have traditionally been hand-coded by human engineers. Such adhoc methods may suffice as long as a running production process remains in place, while any change in the factory layout or production targets necessitates tedious manual reconfiguration, not to mention the missing portability between different production plants. Unlike this, we propose a declarative approach based on Answer Set Programming to optimize the routes taken by automated guided vehicles for accomplishing transport tasks. The advantages include a transparent and executable problem formalization, provable optimality of routes relative to objective criteria, as well as elaboration tolerance towards particular factory layouts and production targets. Moreover, we demonstrate that our approach is efficient enough to deal with the transport tasks evolving in realistic production processes at the car factory of Mercedes-Benz Ludwigsfelde GmbH.
KW  - automated guided vehicle routing
KW  - car assembly operations
KW  - answer set programming
Y1  - 2018
U6  - https://doi.org/10.1017/S1471068418000182
SN  - 1471-0684
SN  - 1475-3081
VL  - 18
IS  - 3-4
SP  - 520
EP  - 534
PB  - Cambridge Univ. Press
CY  - New York
ER  - 
TY  - GEN
A1  - Fichte, Johannes Klaus
A1  - Truszczynski, Miroslaw
A1  - Woltran, Stefan
T1  - Dual-normal logic programs
BT  - the forgotten class
T2  - Postprints der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe
N2  - Disjunctive Answer Set Programming is a powerful declarative programming paradigm with complexity beyond NP. Identifying classes of programs for which the consistency problem is in NP is of interest from the theoretical standpoint and can potentially lead to improvements in the design of answer set programming solvers. One of such classes consists of dual-normal programs, where the number of positive body atoms in proper rules is at most one. Unlike other classes of programs, dual-normal programs have received little attention so far. In this paper we study this class. We relate dual-normal programs to propositional theories and to normal programs by presenting several inter-translations. With the translation from dual-normal to normal programs at hand, we introduce the novel class of body-cycle free programs, which are in many respects dual to head-cycle free programs. We establish the expressive power of dual-normal programs in terms of SE- and UE-models, and compare them to normal programs. We also discuss the complexity of deciding whether dual-normal programs are strongly and uniformly equivalent.
T3  - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - 585 
KW  - answer set programming
KW  - classes of logic programs
KW  - strong and uniform equivalence
KW  - propositional satisfiability
Y1  - 2019
U6  - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-414490
SN  - 1866-8372
IS  - 585
ER  - 
TY  - JOUR
A1  - Hoos, Holger
A1  - Kaminski, Roland
A1  - Lindauer, Marius
A1  - Schaub, Torsten H.
T1  - aspeed: Solver scheduling via answer set programming
JF  - Theory and practice of logic programming
N2  - Although Boolean Constraint Technology has made tremendous progress over the last decade, the efficacy of state-of-the-art solvers is known to vary considerably across different types of problem instances, and is known to depend strongly on algorithm parameters. This problem was addressed by means of a simple, yet effective approach using handmade, uniform, and unordered schedules of multiple solvers in ppfolio, which showed very impressive performance in the 2011 Satisfiability Testing (SAT) Competition. Inspired by this, we take advantage of the modeling and solving capacities of Answer Set Programming (ASP) to automatically determine more refined, that is, nonuniform and ordered solver schedules from the existing benchmarking data. We begin by formulating the determination of such schedules as multi-criteria optimization problems and provide corresponding ASP encodings. The resulting encodings are easily customizable for different settings, and the computation of optimum schedules can mostly be done in the blink of an eye, even when dealing with large runtime data sets stemming from many solvers on hundreds to thousands of instances. Also, the fact that our approach can be customized easily enabled us to swiftly adapt it to generate parallel schedules for multi-processor machines.
KW  - algorithm schedules
KW  - answer set programming
KW  - portfolio-based solving
Y1  - 2015
U6  - https://doi.org/10.1017/S1471068414000015
SN  - 1471-0684
SN  - 1475-3081
VL  - 15
SP  - 117
EP  - 142
PB  - Cambridge Univ. Press
CY  - New York
ER  - 
TY  - GEN
A1  - Hoos, Holger
A1  - Kaminski, Roland
A1  - Lindauer, Marius
A1  - Schaub, Torsten H.
T1  - aspeed
BT  - solver scheduling via answer set programming
T2  - Postprints der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe
N2  - Although Boolean Constraint Technology has made tremendous progress over the last decade, the efficacy of state-of-the-art solvers is known to vary considerably across different types of problem instances, and is known to depend strongly on algorithm parameters. This problem was addressed by means of a simple, yet effective approach using handmade, uniform, and unordered schedules of multiple solvers in ppfolio, which showed very impressive performance in the 2011 Satisfiability Testing (SAT) Competition. Inspired by this, we take advantage of the modeling and solving capacities of Answer Set Programming (ASP) to automatically determine more refined, that is, nonuniform and ordered solver schedules from the existing benchmarking data. We begin by formulating the determination of such schedules as multi-criteria optimization problems and provide corresponding ASP encodings. The resulting encodings are easily customizable for different settings, and the computation of optimum schedules can mostly be done in the blink of an eye, even when dealing with large runtime data sets stemming from many solvers on hundreds to thousands of instances. Also, the fact that our approach can be customized easily enabled us to swiftly adapt it to generate parallel schedules for multi-processor machines.
T3  - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - 588 
KW  - algorithm schedules
KW  - answer set programming
KW  - portfolio-based solving
Y1  - 2019
U6  - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-414743
SN  - 1866-8372
IS  - 588
ER  -