Institut für Informatik und Computational Science
Refine
Year of publication
Document Type
- Article (31)
- Conference Proceeding (1)
- Doctoral Thesis (1)
- Other (1)
Language
- English (34)
Keywords
- Answer Set Programming (4)
- answer set programming (4)
- Answer set programming (3)
- Algorithmen (1)
- Algorithms (1)
- Antwortmengenprogrammierung (1)
- Beweistheorie (1)
- Boolean logic models (1)
- Combinatorial multi-objective optimization (1)
- Complex optimization (1)
- Incremental answer set programming (1)
- Knowledge Representation and Reasoning (1)
- Logic programming (1)
- Meta-Programming (1)
- Nonmonotonic reasoning (1)
- Preference Handling (1)
- Proof Theory (1)
- Signaling transduction networks (1)
- Systems biology (1)
- Theory (1)
- Wissensrepräsentation und -verarbeitung (1)
- action and change (1)
- acyclicity properties (1)
- automated guided vehicle routing (1)
- automated planning (1)
- bioinformatics (1)
- car assembly operations (1)
- competition (1)
- consistency (1)
- declarative problem solving (1)
- diagnosis (1)
- finite model computation (1)
- knowledge representation and nonmonotonic reasoning (1)
- logic-based modeling (1)
- loop formulas (1)
- proof complexity (1)
- satisfiability (1)
- stable model semantics (1)
- tableau calculi (1)
- technical notes and rapid communications (1)
- unfounded sets (1)
Institute
Answer Set Programming (ASP) is an emerging paradigm for declarative programming, in which a computational problem is specified by a logic program such that particular models, called answer sets, match solutions. ASP faces a growing range of applications, demanding for high-performance tools able to solve complex problems. ASP integrates ideas from a variety of neighboring fields. In particular, automated techniques to search for answer sets are inspired by Boolean Satisfiability (SAT) solving approaches. While the latter have firm proof-theoretic foundations, ASP lacks formal frameworks for characterizing and comparing solving methods. Furthermore, sophisticated search patterns of modern SAT solvers, successfully applied in areas like, e.g., model checking and verification, are not yet established in ASP solving. We address these deficiencies by, for one, providing proof-theoretic frameworks that allow for characterizing, comparing, and analyzing approaches to answer set computation. For another, we devise modern ASP solving algorithms that integrate and extend state-of-the-art techniques for Boolean constraint solving. We thus contribute to the understanding of existing ASP solving approaches and their interconnections as well as to their enhancement by incorporating sophisticated search patterns. The central idea of our approach is to identify atomic as well as composite constituents of a propositional logic program with Boolean variables. This enables us to describe fundamental inference steps, and to selectively combine them in proof-theoretic characterizations of various ASP solving methods. In particular, we show that different concepts of case analyses applied by existing ASP solvers implicate mutual exponential separations regarding their best-case complexities. We also develop a generic proof-theoretic framework amenable to language extensions, and we point out that exponential separations can likewise be obtained due to case analyses on them. We further exploit fundamental inference steps to derive Boolean constraints characterizing answer sets. They enable the conception of ASP solving algorithms including search patterns of modern SAT solvers, while also allowing for direct technology transfers between the areas of ASP and SAT solving. Beyond the search for one answer set of a logic program, we address the enumeration of answer sets and their projections to a subvocabulary, respectively. The algorithms we develop enable repetition-free enumeration in polynomial space without being intrusive, i.e., they do not necessitate any modifications of computations before an answer set is found. Our approach to ASP solving is implemented in clasp, a state-of-the-art Boolean constraint solver that has successfully participated in recent solver competitions. Although we do here not address the implementation techniques of clasp or all of its features, we present the principles of its success in the context of ASP solving.
We introduce a simple approach extending the input language of Answer Set Programming (ASP) systems by multi-valued propositions. Our approach is implemented as a (prototypical) preprocessor translating logic programs with multi-valued propositions into logic programs with Boolean propositions only. Our translation is modular and heavily benefits from the expressive input language of ASP. The resulting approach, along with its implementation, allows for solving interesting constraint satisfaction problems in ASP, showing a good performance.