TY  - JOUR
A1  - Bomanson, Jori
A1  - Janhunen, Tomi
A1  - Schaub, Torsten H.
A1  - Gebser, Martin
A1  - Kaufmann, Benjamin
T1  - Answer Set Programming Modulo Acyclicity
JF  - Fundamenta informaticae
N2  - Acyclicity constraints are prevalent in knowledge representation and applications where acyclic data structures such as DAGs and trees play a role. Recently, such constraints have been considered in the satisfiability modulo theories (SMT) framework, and in this paper we carry out an analogous extension to the answer set programming (ASP) paradigm. The resulting formalism, ASP modulo acyclicity, offers a rich set of primitives to express constraints related to recursive structures. In the technical results of the paper, we relate the new generalization with standard ASP by showing (i) how acyclicity extensions translate into normal rules, (ii) how weight constraint programs can be instrumented by acyclicity extensions to capture stability in analogy to unfounded set checking, and (iii) how the gap between supported and stable models is effectively closed in the presence of such an extension. Moreover, we present an efficient implementation of acyclicity constraints by incorporating a respective propagator into the state-of-the-art ASP solver CLASP. The implementation provides a unique combination of traditional unfounded set checking with acyclicity propagation. In the experimental part, we evaluate the interplay of these orthogonal checks by equipping logic programs with supplementary acyclicity constraints. The performance results show that native support for acyclicity constraints is a worthwhile addition, furnishing a complementary modeling construct in ASP itself as well as effective means for translation-based ASP solving.
Y1  - 2016
U6  - https://doi.org/10.3233/FI-2016-1398
SN  - 0169-2968
SN  - 1875-8681
VL  - 147
SP  - 63
EP  - 91
PB  - IOS Press
CY  - Amsterdam
ER  - 
TY  - JOUR
A1  - Janhunen, Tomi
A1  - Kaminski, Roland
A1  - Ostrowski, Max
A1  - Schellhorn, Sebastian
A1  - Wanko, Philipp
A1  - Schaub, Torsten H.
T1  - Clingo goes linear constraints over reals and integers
JF  - Theory and practice of logic programming
N2  - The recent series 5 of the Answer Set Programming (ASP) system clingo provides generic means to enhance basic ASP with theory reasoning capabilities. We instantiate this framework with different forms of linear constraints and elaborate upon its formal properties. Given this, we discuss the respective implementations, and present techniques for using these constraints in a reactive context. More precisely, we introduce extensions to clingo with difference and linear constraints over integers and reals, respectively, and realize them in complementary ways. Finally, we empirically evaluate the resulting clingo derivatives clingo[dl] and clingo[lp] on common language fragments and contrast them to related ASP systems.
KW  - Constraint Answer Set Programming (CASP)
KW  - Answer Set Programming (ASP)
KW  - Constraint Processing (CP)
KW  - Theory Solving
Y1  - 2017
U6  - https://doi.org/10.1017/S1471068417000242
SN  - 1471-0684
SN  - 1475-3081
VL  - 17
SP  - 872
EP  - 888
PB  - Cambridge Univ. Press
CY  - New York
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  - JOUR
A1  - Gressmann, Jean
A1  - Janhunen, Tomi
A1  - Mercer, Robert E.
A1  - Schaub, Torsten H.
A1  - Thiele, Sven
A1  - Tichy, Richard
T1  - On probing and multi-threading in platypus
Y1  - 2006
UR  - http://www2.in.tu-clausthal.de/~tmbehrens/NMR_Proc_TR4.pdf
ER  - 
TY  - JOUR
A1  - Gressmann, Jean
A1  - Janhunen, Tomi
A1  - Mercer, Robert E.
A1  - Schaub, Torsten H.
A1  - Thiele, Sven
A1  - Tichy, Richard
T1  - On probing and multi-threading in platypus
Y1  - 2006
ER  - 
TY  - JOUR
A1  - Gressmann, Jean
A1  - Janhunen, Tomi
A1  - Mercer, Robert E.
A1  - Schaub, Torsten H.
A1  - Thiele, Sven
A1  - Tichy, Richard
T1  - Platypus : a platform for distributed answer set solving
Y1  - 2005
UR  - http://www.cs.uni-potsdam.de/wv/pdfformat/grjamescthti05a.pdf
ER  - 
TY  - JOUR
A1  - Anger, Christian
A1  - Gebser, Martin
A1  - Janhunen, Tomi
A1  - Schaub, Torsten H.
T1  - What's a head without a body?
Y1  - 2006
ER  -