Benjamin Kaufmann

IJCAI Conference 2016 Conference Paper

ASP for Anytime Dynamic Programming on Tree Decompositions

• Bernhard Bliem
• Benjamin Kaufmann
• Torsten Schaub
• Stefan Woltran

Answer Set Programming (ASP) has recently been employed to specify and run dynamic programming (DP) algorithms on tree decompositions, a central approach in the field of parameterized complexity, which aims at solving hard problems efficiently for instances of certain structure. This ASP-based method followed the standard DP approach where tables are computed in a bottom-up fashion, yielding good results for several counting or enumeration problems. However, for optimization problems this approach lacks the possibility to report solutions before the optimum is found, and for search problems it often computes a lot of unnecessary rows. In this paper, we present a novel ASP-based system allowing for "lazy" DP, which utilizes recent multi-shot ASP technology. Preliminary experimental results show that this approach not only yields better performance for search problems, but also outperforms some state-of-the-art ASP encodings for optimization problems in terms of anytime computation, i. e. , measuring the quality of the best solution after a certain timeout.

IJCAI Conference 2013 Conference Paper

Advanced Conflict-Driven Disjunctive Answer Set Solving

• Martin Gebser
• Benjamin Kaufmann
• Torsten Schaub

We introduce a new approach to disjunctive ASP solving that aims at an equitable interplay between “generating” and “testing” solver units. To this end, we develop novel characterizations of answer sets and unfounded sets allowing for a bidirectional dynamic information exchange between solver units for orthogonal tasks. This results in the new multithreaded disjunctive ASP solver claspD-2, greatly improving the performance of existing systems.

AAAI Conference 2013 Conference Paper

Domain-Specific Heuristics in Answer Set Programming

• Martin Gebser
• Benjamin Kaufmann
• Javier Romero
• Ramón Otero
• Torsten Schaub
• Philipp Wanko

We introduce a general declarative framework for incorporating domain-specific heuristics into ASP solving. We accomplish this by extending the first-order modeling language of ASP by a distinguished heuristic predicate. The resulting heuristic information is processed as an equitable part of the logic program and subsequently exploited by the solver when it comes to non-deterministically assigning a truth value to an atom. We implemented our approach as a dedicated heuristic in the ASP solver clasp and show its great prospect by an empirical evaluation.

AIJ Journal 2012 Journal Article

Conflict-driven answer set solving: From theory to practice

• Martin Gebser
• Benjamin Kaufmann
• Torsten Schaub

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.

ECAI Conference 2008 Conference Paper

Advanced Preprocessing for Answer Set Solving

• Martin Gebser
• Benjamin Kaufmann
• André Neumann
• Torsten Schaub

We introduce the first substantial approach to preprocessing in the context of answer set solving. The idea is to simplify a logic program while identifying equivalences among its relevant constituents. These equivalences are then used for building a compact representation of the program (in terms of Boolean constraints). We implemented our approach as well as a SAT-based technique to reduce Boolean constraints. This allows us to empirically analyze both preprocessing types and to demonstrate their computational impact.

KR Conference 2008 Conference Paper

Conflict-Driven Disjunctive Answer Set Solving

• Christian Drescher
• Martin Gebser
• Torsten Grote
• Benjamin Kaufmann
• Arne Koenig
• Max Ostrowski
• Torsten Schaub

We elaborate a uniform approach to computing answer sets of disjunctive logic programs based on state-of-the-art Boolean constraint solving techniques. Starting from a constraint-based characterization of answer sets, we develop advanced solving algorithms, featuring backjumping and conflict-driven learning using the First-UIP scheme as well as sophisticated unfounded set checking. As a final result, we obtain a competitive solver for $Sigma_2^P$-complete problems, taking advantage of Boolean constraint solving technology without using any legacy solvers as black boxes.

IJCAI Conference 2007 Conference Paper

• Martin Gebser
• Benjamin Kaufmann
• Andr
• eacute; Neumann
• Torsten Schaub

We introduce a new approach to computing answer sets of logic programs, based on concepts from constraint processing (CSP) and satisfiability checking (SAT). 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 for the different kinds of inferences in ASP. It also allows us to apply advanced techniques from the areas of CSP and SAT. We have implemented our approach in the new ASP solver clasp. Our experiments show that the approach is competitive with state-of-the-art ASP solvers.