TY  - JOUR
A1  - Gebser, Martin
A1  - Kaufmann, Benjamin
A1  - Schaub, Torsten H.
T1  - Conflict-driven answer set solving: From theory to practice
JF  - Artificial intelligence
N2  - 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.
KW  - Answer set programming
KW  - Logic programming
KW  - Nonmonotonic reasoning
Y1  - 2012
U6  - https://doi.org/10.1016/j.artint.2012.04.001
SN  - 0004-3702
VL  - 187
IS  - 8
SP  - 52
EP  - 89
PB  - Elsevier
CY  - Amsterdam
ER  - 
TY  - JOUR
A1  - Ostrowski, Max
A1  - Schaub, Torsten H.
T1  - ASP modulo CSP The clingcon system
JF  - Theory and practice of logic programming
N2  - We present the hybrid ASP solver clingcon, combining the simple modeling language and the high performance Boolean solving capacities of Answer Set Programming (ASP) with techniques for using non-Boolean constraints from the area of Constraint Programming (CP). The new clingcon system features an extended syntax supporting global constraints and optimize statements for constraint variables. The major technical innovation improves the interaction between ASP and CP solver through elaborated learning techniques based on irreducible inconsistent sets. A broad empirical evaluation shows that these techniques yield a performance improvement of an order of magnitude.
Y1  - 2012
U6  - https://doi.org/10.1017/S1471068412000142
SN  - 1471-0684
VL  - 12
SP  - 485
EP  - 503
PB  - Cambridge Univ. Press
CY  - New York
ER  - 
TY  - JOUR
A1  - Gebser, Martin
A1  - Kaufmann, Benjamin
A1  - Schaub, Torsten H.
T1  - Multi-threaded ASP solving with clasp
JF  - Theory and practice of logic programming
N2  - We present the new multi-threaded version of the state-of-the-art answer set solver clasp. We detail its component and communication architecture and illustrate how they support the principal functionalities of clasp. Also, we provide some insights into the data representation used for different constraint types handled by clasp. All this is accompanied by an extensive experimental analysis of the major features related to multi-threading in clasp.
Y1  - 2012
U6  - https://doi.org/10.1017/S1471068412000166
SN  - 1471-0684
VL  - 12
IS  - 8
SP  - 525
EP  - 545
PB  - Cambridge Univ. Press
CY  - New York
ER  - 
TY  - GEN
A1  - Ostrowski, Max
A1  - Schaub, Torsten H.
T1  - ASP modulo CSP
BT  - the clingcon system
T2  - Postprints der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe
N2  - We present the hybrid ASP solver clingcon, combining the simple modeling language and the high performance Boolean solving capacities of Answer Set Programming (ASP) with techniques for using non-Boolean constraints from the area of Constraint Programming (CP). The new clingcon system features an extended syntax supporting global constraints and optimize statements for constraint variables. The major technical innovation improves the interaction between ASP and CP solver through elaborated learning techniques based on irreducible inconsistent sets. A broad empirical evaluation shows that these techniques yield a performance improvement of an order of magnitude.
T3  - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - 579 
KW  - answer set
KW  - constraints
KW  - logic
KW  - SMT
Y1  - 2019
U6  - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-413908
SN  - 1866-8372
IS  - 579
ER  - 
TY  - GEN
A1  - Gebser, Martin
A1  - Kaufmann, Benjamin
A1  - Schaub, Torsten H.
T1  - Multi-threaded ASP solving with clasp
T2  - Postprints der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe
N2  - We present the new multi-threaded version of the state-of-the-art answer set solver clasp. We detail its component and communication architecture and illustrate how they support the principal functionalities of clasp. Also, we provide some insights into the data representation used for different constraint types handled by clasp. All this is accompanied by an extensive experimental analysis of the major features related to multi-threading in clasp.
T3  - Zweitveröffentlichungen der Universität Potsdam : Mathematisch-Naturwissenschaftliche Reihe - 586 
KW  - propositional satisfiability
KW  - clause elimination
KW  - parallel execution
KW  - SAT
KW  - algorithm
KW  - platypus
KW  - systems
KW  - search
KW  - solver
Y1  - 2019
U6  - http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:kobv:517-opus4-413977
SN  - 1866-8372
IS  - 586
ER  -