TY - JOUR A1 - Cabalar, Pedro A1 - Dieguez, Martin A1 - Schaub, Torsten H. A1 - Schuhmann, Anna T1 - Towards metric temporal answer set programming JF - Theory and practice of logic programming N2 - We elaborate upon the theoretical foundations of a metric temporal extension of Answer Set Programming. In analogy to previous extensions of ASP with constructs from Linear Temporal and Dynamic Logic, we accomplish this in the setting of the logic of Here-and-There and its non-monotonic extension, called Equilibrium Logic. More precisely, we develop our logic on the same semantic underpinnings as its predecessors and thus use a simple time domain of bounded time steps. This allows us to compare all variants in a uniform framework and ultimately combine them in a common implementation. Y1 - 2020 U6 - https://doi.org/10.1017/S1471068420000307 SN - 1471-0684 SN - 1475-3081 VL - 20 IS - 5 SP - 783 EP - 798 PB - Cambridge Univ. Press CY - Cambridge [u.a.] ER - TY - JOUR A1 - Fandiño, Jorge A1 - Lifschitz, Vladimir A1 - Lühne, Patrick A1 - Schaub, Torsten H. T1 - Verifying tight logic programs with Anthem and Vampire JF - Theory and practice of logic programming N2 - This paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas. Y1 - 2020 U6 - https://doi.org/10.1017/S1471068420000344 SN - 1471-0684 SN - 1475-3081 VL - 20 IS - 5 SP - 735 EP - 750 PB - Cambridge Univ. Press CY - Cambridge [u.a.] ER - TY - JOUR A1 - Cabalar, Pedro A1 - Fandiño, Jorge A1 - Garea, Javier A1 - Romero, Javier A1 - Schaub, Torsten H. T1 - Eclingo BT - a solver for epistemic logic programs JF - Theory and practice of logic programming N2 - We describe eclingo, a solver for epistemic logic programs under Gelfond 1991 semantics built upon the Answer Set Programming system clingo. The input language of eclingo uses the syntax extension capabilities of clingo to define subjective literals that, as usual in epistemic logic programs, allow for checking the truth of a regular literal in all or in some of the answer sets of a program. The eclingo solving process follows a guess and check strategy. It first generates potential truth values for subjective literals and, in a second step, it checks the obtained result with respect to the cautious and brave consequences of the program. This process is implemented using the multi-shot functionalities of clingo. We have also implemented some optimisations, aiming at reducing the search space and, therefore, increasing eclingo 's efficiency in some scenarios. Finally, we compare the efficiency of eclingo with two state-of-the-art solvers for epistemic logic programs on a pair of benchmark scenarios and show that eclingo generally outperforms their obtained results. KW - Answer Set Programming KW - Epistemic Logic Programs KW - Non-Monotonic KW - Reasoning KW - Conformant Planning Y1 - 2020 U6 - https://doi.org/10.1017/S1471068420000228 SN - 1471-0684 SN - 1475-3081 VL - 20 IS - 6 SP - 834 EP - 847 PB - Cambridge Univ. Press CY - New York ER - TY - JOUR A1 - Lindauer, Marius A1 - Hoos, Holger A1 - Leyton-Brown, Kevin A1 - Schaub, Torsten H. T1 - Automatic construction of parallel portfolios via algorithm configuration JF - Artificial intelligence N2 - Since 2004, increases in computational power described by Moore's law have substantially been realized in the form of additional cores rather than through faster clock speeds. To make effective use of modern hardware when solving hard computational problems, it is therefore necessary to employ parallel solution strategies. In this work, we demonstrate how effective parallel solvers for propositional satisfiability (SAT), one of the most widely studied NP-complete problems, can be produced automatically from any existing sequential, highly parametric SAT solver. Our Automatic Construction of Parallel Portfolios (ACPP) approach uses an automatic algorithm configuration procedure to identify a set of configurations that perform well when executed in parallel. Applied to two prominent SAT solvers, Lingeling and clasp, our ACPP procedure identified 8-core solvers that significantly outperformed their sequential counterparts on a diverse set of instances from the application and hard combinatorial category of the 2012 SAT Challenge. We further extended our ACPP approach to produce parallel portfolio solvers consisting of several different solvers by combining their configuration spaces. Applied to the component solvers of the 2012 SAT Challenge gold medal winning SAT Solver pfolioUZK, our ACPP procedures produced a significantly better-performing parallel SAT solver. KW - Algorithm configuration KW - Parallel SAT solving KW - Algorithm portfolios KW - Programming by optimization KW - Automated parallelization Y1 - 2016 U6 - https://doi.org/10.1016/j.artint.2016.05.004 SN - 0004-3702 SN - 1872-7921 VL - 244 SP - 272 EP - 290 PB - Elsevier CY - Amsterdam ER - TY - GEN A1 - Neubauer, Kai A1 - Haubelt, Christian A1 - Wanko, Philipp A1 - Schaub, Torsten H. T1 - Utilizing quad-trees for efficient design space exploration with partial assignment evaluation T2 - 2018 23rd Asia and South Pacific Design Automation Conference (ASP-DAC) N2 - Recently, it has been shown that constraint-based symbolic solving techniques offer an efficient way for deciding binding and routing options in order to obtain a feasible system level implementation. In combination with various background theories, a feasibility analysis of the resulting system may already be performed on partial solutions. That is, infeasible subsets of mapping and routing options can be pruned early in the decision process, which fastens the solving accordingly. However, allowing a proper design space exploration including multi-objective optimization also requires an efficient structure for storing and managing non-dominated solutions. In this work, we propose and study the usage of the Quad-Tree data structure in the context of partial assignment evaluation during system synthesis. Out experiments show that unnecessary dominance checks can be avoided, which indicates a preference of Quad-Trees over a commonly used list-based implementation for large combinatorial optimization problems. Y1 - 2018 SN - 978-1-5090-0602-1 U6 - https://doi.org/10.1109/ASPDAC.2018.8297362 SN - 2153-6961 SP - 434 EP - 439 PB - IEEE CY - New York ER - TY - GEN A1 - Bosser, Anne-Gwenn A1 - Cabalar, Pedro A1 - Dieguez, Martin A1 - Schaub, Torsten H. T1 - Introducing temporal stable models for linear dynamic logic T2 - 16th International Conference on Principles of Knowledge Representation and Reasoning N2 - We propose a new temporal extension of the logic of Here-and-There (HT) and its equilibria obtained by combining it with dynamic logic over (linear) traces. Unlike previous temporal extensions of HT based on linear temporal logic, the dynamic logic features allow us to reason about the composition of actions. For instance, this can be used to exercise fine grained control when planning in robotics, as exemplified by GOLOG. In this paper, we lay the foundations of our approach, and refer to it as Linear Dynamic Equilibrium Logic, or simply DEL. We start by developing the formal framework of DEL and provide relevant characteristic results. Among them, we elaborate upon the relationships to traditional linear dynamic logic and previous temporal extensions of HT. Y1 - 2018 UR - https://www.dc.fi.udc.es/~cabalar/del.pdf SP - 12 EP - 21 PB - ASSOC Association for the Advancement of Artificial Intelligence CY - Palo Alto ER - TY - GEN A1 - Schäpers, Björn A1 - Niemueller, Tim A1 - Lakemeyer, Gerhard A1 - Gebser, Martin A1 - Schaub, Torsten H. T1 - ASP-Based Time-Bounded Planning for Logistics Robots T2 - Twenty-Eighth International Conference on Automated Planning and Scheduling (ICAPS 2018) N2 - Manufacturing industries are undergoing a major paradigm shift towards more autonomy. Automated planning and scheduling then becomes a necessity. The Planning and Execution Competition for Logistics Robots in Simulation held at ICAPS is based on this scenario and provides an interesting testbed. However, the posed problem is challenging as also demonstrated by the somewhat weak results in 2017. The domain requires temporal reasoning and dealing with uncertainty. We propose a novel planning system based on Answer Set Programming and the Clingo solver to tackle these problems and incentivize robot cooperation. Our results show a significant performance improvement, both, in terms of lowering computational requirements and better game metrics. Y1 - 2018 SN - 2334-0835 SN - 2334-0843 SP - 509 EP - 517 PB - ASSOC Association for the Advancement of Artificial Intelligence CY - Palo Alto 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 - Brewka, Gerhard A1 - Schaub, Torsten H. A1 - Woltran, Stefan T1 - Interview with Gerhard Brewka T2 - Künstliche Intelligenz N2 - This interview with Gerhard Brewka was conducted by correspondance in May 2018. The question set was compiled by Torsten Schaub and Stefan Woltran. Y1 - 2018 U6 - https://doi.org/10.1007/s13218-018-0549-5 SN - 0933-1875 SN - 1610-1987 VL - 32 IS - 2-3 SP - 219 EP - 221 PB - Springer CY - Heidelberg ER - TY - GEN A1 - Lifschitz, Vladimir A1 - Schaub, Torsten H. A1 - Woltran, Stefan T1 - Interview with Vladimir Lifschitz T2 - Künstliche Intelligenz N2 - This interview with Vladimir Lifschitz was conducted by Torsten Schaub at the University of Texas at Austin in August 2017. The question set was compiled by Torsten Schaub and Stefan Woltran. Y1 - 2018 U6 - https://doi.org/10.1007/s13218-018-0552-x SN - 0933-1875 SN - 1610-1987 VL - 32 IS - 2-3 SP - 213 EP - 218 PB - Springer CY - Heidelberg ER -