@article{Hecher2022, author = {Hecher, Markus}, title = {Treewidth-aware reductions of normal ASP to SAT}, series = {Artificial intelligence}, volume = {304}, journal = {Artificial intelligence}, publisher = {Elsevier}, address = {Amsterdam}, issn = {0004-3702}, doi = {10.1016/j.artint.2021.103651}, pages = {24}, year = {2022}, abstract = {Answer Set Programming (ASP) is a paradigm for modeling and solving problems for knowledge representation and reasoning. There are plenty of results dedicated to studying the hardness of (fragments of) ASP. So far, these studies resulted in characterizations in terms of computational complexity as well as in fine-grained insights presented in form of dichotomy-style results, lower bounds when translating to other formalisms like propositional satisfiability (SAT), and even detailed parameterized complexity landscapes. A generic parameter in parameterized complexity originating from graph theory is the socalled treewidth, which in a sense captures structural density of a program. Recently, there was an increase in the number of treewidth-based solvers related to SAT. While there are translations from (normal) ASP to SAT, no reduction that preserves treewidth or at least keeps track of the treewidth increase is known. In this paper we propose a novel reduction from normal ASP to SAT that is aware of the treewidth, and guarantees that a slight increase of treewidth is indeed sufficient. Further, we show a new result establishing that, when considering treewidth, already the fragment of normal ASP is slightly harder than SAT (under reasonable assumptions in computational complexity). This also confirms that our reduction probably cannot be significantly improved and that the slight increase of treewidth is unavoidable. Finally, we present an empirical study of our novel reduction from normal ASP to SAT, where we compare treewidth upper bounds that are obtained via known decomposition heuristics. Overall, our reduction works better with these heuristics than existing translations. (c) 2021 Elsevier B.V. All rights reserved.}, language = {en} } @article{BanbaraInoueKaufmannetal.2018, author = {Banbara, Mutsunori and Inoue, Katsumi and Kaufmann, Benjamin and Okimoto, Tenda and Schaub, Torsten H. and Soh, Takehide and Tamura, Naoyuki and Wanko, Philipp}, title = {teaspoon}, series = {Annals of operation research}, volume = {275}, journal = {Annals of operation research}, number = {1}, publisher = {Springer}, address = {Dordrecht}, issn = {0254-5330}, doi = {10.1007/s10479-018-2757-7}, pages = {3 -- 37}, year = {2018}, abstract = {Answer Set Programming (ASP) is an approach to declarative problem solving, combining a rich yet simple modeling language with high performance solving capacities. We here develop an ASP-based approach to curriculum-based course timetabling (CB-CTT), one of the most widely studied course timetabling problems. The resulting teaspoon system reads a CB-CTT instance of a standard input format and converts it into a set of ASP facts. In turn, these facts are combined with a first-order encoding for CB-CTT solving, which can subsequently be solved by any off-the-shelf ASP systems. We establish the competitiveness of our approach by empirically contrasting it to the best known bounds obtained so far via dedicated implementations. Furthermore, we extend the teaspoon system to multi-objective course timetabling and consider minimal perturbation problems.}, language = {en} } @article{AguadoCabalarFandinoetal.2019, author = {Aguado, Felicidad and Cabalar, Pedro and Fandi{\~n}o, Jorge and Pearce, David and Perez, Gilberto and Vidal-Peracho, Concepcion}, title = {Revisiting Explicit Negation in Answer Set Programming}, series = {Theory and practice of logic programming}, volume = {19}, journal = {Theory and practice of logic programming}, number = {5-6}, publisher = {Cambridge Univ. Press}, address = {New York}, issn = {1471-0684}, doi = {10.1017/S1471068419000267}, pages = {908 -- 924}, year = {2019}, language = {en} } @article{GebserKaufmannKaminskietal.2011, author = {Gebser, Martin and Kaufmann, Benjamin and Kaminski, Roland and Ostrowski, Max and Schaub, Torsten H. and Schneider, Marius}, title = {Potassco the Potsdam answer set solving collection}, series = {AI communications : AICOM ; the European journal on artificial intelligence}, volume = {24}, journal = {AI communications : AICOM ; the European journal on artificial intelligence}, number = {2}, publisher = {IOS Press}, address = {Amsterdam}, issn = {0921-7126}, doi = {10.3233/AIC-2011-0491}, pages = {107 -- 124}, year = {2011}, abstract = {This paper gives an overview of the open source project Potassco, the Potsdam Answer Set Solving Collection, bundling tools for Answer Set Programming developed at the University of Potsdam.}, language = {en} } @article{VidelaGuziolowskiEduatietal.2015, author = {Videla, Santiago and Guziolowski, Carito and Eduati, Federica and Thiele, Sven and Gebser, Martin and Nicolas, Jacques and Saez-Rodriguez, Julio and Schaub, Torsten H. and Siegel, Anne}, title = {Learning Boolean logic models of signaling networks with ASP}, series = {Theoretical computer science}, volume = {599}, journal = {Theoretical computer science}, publisher = {Elsevier}, address = {Amsterdam}, issn = {0304-3975}, doi = {10.1016/j.tcs.2014.06.022}, pages = {79 -- 101}, year = {2015}, abstract = {Boolean networks provide a simple yet powerful qualitative modeling approach in systems biology. However, manual identification of logic rules underlying the system being studied is in most cases out of reach. Therefore, automated inference of Boolean logical networks from experimental data is a fundamental question in this field. This paper addresses the problem consisting of learning from a prior knowledge network describing causal interactions and phosphorylation activities at a pseudo-steady state, Boolean logic models of immediate-early response in signaling transduction networks. The underlying optimization problem has been so far addressed through mathematical programming approaches and the use of dedicated genetic algorithms. In a recent work we have shown severe limitations of stochastic approaches in this domain and proposed to use Answer Set Programming (ASP), considering a simpler problem setting. Herein, we extend our previous work in order to consider more realistic biological conditions including numerical datasets, the presence of feedback-loops in the prior knowledge network and the necessity of multi-objective optimization. In order to cope with such extensions, we propose several discretization schemes and elaborate upon our previous ASP encoding. Towards real-world biological data, we evaluate the performance of our approach over in silico numerical datasets based on a real and large-scale prior knowledge network. The correctness of our encoding and discretization schemes are dealt with in Appendices A-B. (C) 2014 Elsevier B.V. All rights reserved.}, language = {en} } @article{BobdaYongaGebseretal.2018, author = {Bobda, Christophe and Yonga, Franck and Gebser, Martin and Ishebabi, Harold and Schaub, Torsten H.}, title = {High-level synthesis of on-chip multiprocessor architectures based on answer set programming}, series = {Journal of Parallel and Distributed Computing}, volume = {117}, journal = {Journal of Parallel and Distributed Computing}, publisher = {Elsevier}, address = {San Diego}, issn = {0743-7315}, doi = {10.1016/j.jpdc.2018.02.010}, pages = {161 -- 179}, year = {2018}, abstract = {We present a system-level synthesis approach for heterogeneous multi-processor on chip, based on Answer Set Programming(ASP). Starting with a high-level description of an application, its timing constraints and the physical constraints of the target device, our goal is to produce the optimal computing infrastructure made of heterogeneous processors, peripherals, memories and communication components. Optimization aims at maximizing speed, while minimizing chip area. Also, a scheduler must be produced that fulfills the real-time requirements of the application. Even though our approach will work for application specific integrated circuits, we have chosen FPGA as target device in this work because of their reconfiguration capabilities which makes it possible to explore several design alternatives. This paper addresses the bottleneck of problem representation size by providing a direct and compact ASP encoding for automatic synthesis that is semantically equivalent to previously established ILP and ASP models. We describe a use-case in which designers specify their applications in C/C++ from which optimum systems can be derived. We demonstrate the superiority of our approach toward existing heuristics and exact methods with synthesis results on a set of realistic case studies. (C) 2018 Elsevier Inc. All rights reserved.}, language = {en} } @article{AguadoCabalarFandinnoetal.2019, author = {Aguado, Felicidad and Cabalar, Pedro and Fandinno, Jorge and Pearce, David and Perez, Gilberto and Vidal, Concepcion}, title = {Forgetting auxiliary atoms in forks}, series = {Artificial intelligence}, volume = {275}, journal = {Artificial intelligence}, publisher = {Elsevier}, address = {Amsterdam}, issn = {0004-3702}, doi = {10.1016/j.artint.2019.07.005}, pages = {575 -- 601}, year = {2019}, abstract = {In this work we tackle the problem of checking strong equivalence of logic programs that may contain local auxiliary atoms, to be removed from their stable models and to be forbidden in any external context. We call this property projective strong equivalence (PSE). It has been recently proved that not any logic program containing auxiliary atoms can be reformulated, under PSE, as another logic program or formula without them - this is known as strongly persistent forgetting. In this paper, we introduce a conservative extension of Equilibrium Logic and its monotonic basis, the logic of Here-and-There, in which we deal with a new connective '|' we call fork. We provide a semantic characterisation of PSE for forks and use it to show that, in this extension, it is always possible to forget auxiliary atoms under strong persistence. We further define when the obtained fork is representable as a regular formula.}, language = {en} } @article{BreitenreiterAndjelkovićSchrapeetal.2022, author = {Breitenreiter, Anselm and Andjelković, Marko and Schrape, Oliver and Krstić, Miloš}, title = {Fast error propagation probability estimates by answer set programming and approximate model counting}, series = {IEEE Access}, volume = {10}, journal = {IEEE Access}, publisher = {Inst. of Electr. and Electronics Engineers}, address = {Piscataway}, issn = {2169-3536}, doi = {10.1109/ACCESS.2022.3174564}, pages = {51814 -- 51825}, year = {2022}, abstract = {We present a method employing Answer Set Programming in combination with Approximate Model Counting for fast and accurate calculation of error propagation probabilities in digital circuits. By an efficient problem encoding, we achieve an input data format similar to a Verilog netlist so that extensive preprocessing is avoided. By a tight interconnection of our application with the underlying solver, we avoid iterating over fault sites and reduce calls to the solver. Several circuits were analyzed with varying numbers of considered cycles and different degrees of approximation. Our experiments show, that the runtime can be reduced by approximation by a factor of 91, whereas the error compared to the exact result is below 1\%.}, language = {en} } @article{GebserKaufmannSchaub2012, author = {Gebser, Martin and Kaufmann, Benjamin and Schaub, Torsten H.}, title = {Conflict-driven answer set solving: From theory to practice}, series = {Artificial intelligence}, volume = {187}, journal = {Artificial intelligence}, number = {8}, publisher = {Elsevier}, address = {Amsterdam}, issn = {0004-3702}, doi = {10.1016/j.artint.2012.04.001}, pages = {52 -- 89}, year = {2012}, abstract = {We introduce an approach to computing answer sets of logic programs, based on concepts successfully applied in Satisfiability (SAT) checking. The idea is to view inferences in Answer Set Programming (ASP) as unit propagation on nogoods. This provides us with a uniform constraint-based framework capturing diverse inferences encountered in ASP solving. Moreover, our approach allows us to apply advanced solving techniques from the area of SAT. As a result, we present the first full-fledged algorithmic framework for native conflict-driven ASP solving. Our approach is implemented in the ASP solver clasp that has demonstrated its competitiveness and versatility by winning first places at various solver contests.}, language = {en} } @misc{RazzaqKaminskiRomeroetal.2018, author = {Razzaq, Misbah and Kaminski, Roland and Romero, Javier and Schaub, Torsten H. and Bourdon, Jeremie and Guziolowski, Carito}, title = {Computing diverse boolean networks from phosphoproteomic time series data}, series = {Computational Methods in Systems Biology}, volume = {11095}, journal = {Computational Methods in Systems Biology}, publisher = {Springer}, address = {Berlin}, isbn = {978-3-319-99429-1}, issn = {0302-9743}, doi = {10.1007/978-3-319-99429-1_4}, pages = {59 -- 74}, year = {2018}, abstract = {Logical modeling has been widely used to understand and expand the knowledge about protein interactions among different pathways. Realizing this, the caspo-ts system has been proposed recently to learn logical models from time series data. It uses Answer Set Programming to enumerate Boolean Networks (BNs) given prior knowledge networks and phosphoproteomic time series data. In the resulting sequence of solutions, similar BNs are typically clustered together. This can be problematic for large scale problems where we cannot explore the whole solution space in reasonable time. Our approach extends the caspo-ts system to cope with the important use case of finding diverse solutions of a problem with a large number of solutions. We first present the algorithm for finding diverse solutions and then we demonstrate the results of the proposed approach on two different benchmark scenarios in systems biology: (1) an artificial dataset to model TCR signaling and (2) the HPN-DREAM challenge dataset to model breast cancer cell lines.}, language = {en} }