ABSTRACT. We describe the novel functionalities comprised in clasp's series 3. This includes parallel solving of disjunctive logic programs, parallel optimization with orthogonal strategies, declarative support for specifying domain heuristics, an application programming interface for library integration, and a portfolio of prefabricated expert configurations. This is complemented by experiments evaluating clasp 3's optimization capacities as well as the impact of domain heuristics.

ABSTRACT. Answer Set Programming (ASP) solvers address several reasoning tasks that go beyond the mere computation of answer sets. Among them are cautious reasoning, for modeling query entailment, and optimum answer set computation, for supporting numerical optimization. This paper reports on the recent improvements of the solver WASP, and details the algorithms and the design choices for addressing several reasoning tasks in ASP. An experimental analysis on publicly available benchmarks shows that the new version of WASP outperforms the previous one. Comparing with the state-of-the-art solver clasp, the performance of WASP is competitive in the overall for number of solved instances and average execution time.

ABSTRACT. Encoding finite linear CSPs as Boolean formulas and solving them by using modern SAT solvers has proven to be highly effective by the award-winning sugar system. We here develop an alternative approach based on ASP that serves two purposes. First, it provides a library for solving CSPs as part of an encompassing logic program. Second, it furnishes an ASP-based CSP solver similar to sugar. Both tasks are addressed by using first-order ASP encodings that provide us with a high degree of flexibility, either for integration within ASP or for easy experimentation with different implementations. When used as a CSP solver, the resulting system aspartame re-uses parts of sugar for parsing and normalizing CSPs. The obtained set of facts is then combined with an ASP encoding that can be grounded and solved by off-the-shelf ASP systems. We establish the competitiveness of our approach by empirically contrasting aspartame and sugar.

ABSTRACT. Over the last years, Answer Set Programming has significantly extended its range of applicability, and moved beyond solving static problems to dynamic ones, even in online environments. However, its nonmonotonic nature as well as its upstream instantiation process impede a seamless integration of new objects into its reasoning process, which is crucial in dynamic domains such as logistics or robotics. We address this problem and introduce a simple approach to successively incorporating new information into ASP systems. Our approach rests upon a translation of logic programs and thus refrains from any dedicated algorithms. We prove its modularity as regards the addition of new information and show its soundness and completeness. We apply our methodology to two domains of the Fifth ASP Competition and evaluate traditional one-shot and incremental multi-shot solving approaches.

ABSTRACT. Automated algorithm selection techniques have been applied successfully to Answer Set Programming (ASP) solvers. The idea is to select automatically the "best'' computation strategy on the basis of syntactic input features. The choice of the solving strategy is done by relying on machine learning techniques. 

ASP computation includes two levels of elaboration: variable elimination, called grounding, and propositional answer set search, called solving. The application of these methods is usually limited to propositional programs, and the choice of algorithms is thus limited to the solving phase.

In this paper we present ME-ASP^ML, a new ASP system applying algorithm selection techniques based on classification for selecting the most promising combination of grounder and solver. An experiment conducted on benchmarks and solvers of the Fifth ASP competition confirm that ME-ASP^ML is able to solve more instances than state of the art proposals and competing systems.

ABSTRACT. In the domain of hard real-time systems, where system complexity meets stringent timing constraints, the task of system-level synthesis has become more and more challenging. As a remedy, we introduce an SMT-based system synthesis approach where the boolean solver determines a static binding of computational tasks and a routing of messages while the theory solver computes a global time-triggered schedule based on the boolean solver’s solution. The binding and routing is stated as an optimization problem in order to refine the solution found by the boolean solver such that the theory solver is more likely to find a feasible schedule within a reasonable amount of time. In this paper we enhance this approach by applying domain-specific heuristics to the optimization problem. Our experiments show that by utilizing domain knowledge we were able to significantly increase the number of solved instances.

ABSTRACT. The modelling of dynamically varying spatial information is a key requirement in a wide range of application domains including intelligent systems, cognitive robotics, architectural design assistance, and temporal and event-based GIS. We present ASPMT(QS), a novel approach and fully-implemented prototype for non-monotonic spatial reasoning (e.g. performing causal explanation in an abductive manner) based on Answer Set Programming Modulo Theories. ASPMT(QS) consists of a (qualitative) spatial representation module and a method for turning tight ASPMT instances into Sat Modulo Theories (SMT) instances in order to compute stable models by means of SMT solvers. We formalise and implement concepts of spatial default reasoning and spatial frame axioms using choice formulas. Spatial reasoning is performed by encoding spatial relations as systems of polynomial constraints, and solving via SMT with the theory of real nonlinear arithmetic. We empirically evaluate ASPMT(QS) in comparison with other prominent contemporary spatial reasoning systems. Our results show that ASPMT(QS) is the only existing system that is capable of reasoning about indirect spatial effects (i.e. addressing the ramification problem), and integrating geometric (numerical) and qualitative spatial information within a non-monotonic spatial reasoning context.

ABSTRACT. Acyclicity constraints are prevalent in knowledge representation and, in particular, 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 with recursive structures. The implementation, obtained as an extension to the state-of-the-art answer set solver clasp, has a unique propagation mechanism that combines traditional unfounded set checking with acyclicity propagation. The interplay of these orthogonal checks is experimentally evaluated by equipping answer set programs with supplementary acyclicity constraints.

ABSTRACT. We present algorithms for solving Modular Systems inspired by the Conflict-Directed Clause Learning algorithm for propositional satisfiability.

ABSTRACT. Forest Logic Programs (FoLP) are a decidable fragment of Open Answer Set Programming (OASP) which have the forest model property. OASP extends Answer Set Programming (ASP) with open domains---a feature which makes it possible for FoLPs to simulate reasoning with the expressive description logic SHOQ. At the same time, the fragment retains the attractive rule syntax and the non-monotonicity specific to ASP. In the past, several tableaux algorithms have been devised to reason with FoLPs, the most recent of which established a NEXPTIME upper bound for reasoning with the fragment. While known to be EXPTIME-hard, the exact complexity characterization of reasoning with the fragment was still unknown. In this paper we settle this open question by a reduction of reasoning with FoLPs to emptiness checking of fully enriched automata, a form of automata which run on forests, and which are known to be EXPTIME-complete.

ABSTRACT. Dynamic programming (DP) on tree decompositions is a well studied approach for solving hard problems efficiently. Usually, implementations rely on tables for storing information, and algorithms specify how tuples are manipulated during traversal of the decomposition. However, a bottleneck of such table-based algorithms is relatively high memory consumption. Binary Decision Diagrams (BDDs) and related concepts have been shown to be very well suited to store information efficiently. While several techniques have been proposed that combine DP with efficient BDD-based storage for some particular problems (e.g., Constraint Satisfaction), in this work we present a general approach where DP algorithms are specified on a logical level in form of set-based formula manipulation operations that are executed directly on the BDD data structure. In the paper, we provide several case studies in order to illustrate the method at work, and report on preliminary experiments. These show promising results, both with respect to memory and run-time.

ABSTRACT. Integrating knowledge from various sources is a recurring problem in Artificial Intelligence, often addressed by multi-context systems (MCSs). Existing MCSs however have limited support for the open-world semantics of knowledge bases (KBs) expressed in knowledge representation languages based on first-order logic. To address this problem we introduce knowledge base networks (KBNs), which consist of open-world KBs linked by non-monotonic bridge rules under a stable model semantics. Basic entailment in KBNs is decidable whenever it is in the individual KBs. This is due to a fundamental representation theorem, which allows us to derive complexity results, and also gives a perspective for implementation. In particular, for networks of KBs in well-known Description Logics (DLs), reasoning is reducible to reasoning in dl-programs of Eiter et al. As a by product, we obtain an embedding of Motik and Rosati’s hybrid MKNF KBs, which amount to a special case of KBNs, to dl-programs. We also show that reasoning in networks of ontologies in lightweight DLs is not harder than in answer set programming.

ABSTRACT. We present a new approach to evaluate conditionals in human reasoning. This approach is based on the weak completion semantics which has been successfully applied to adequately model various other human reasoning tasks in the past. The main idea is to explicitely consider the case, where the condition of a conditional is unknown with respect to some background knowledge, and to evaluate it with minimal revision followed by abduction. We formally compare our approach to a recent approach by Schulz and demonstrate that our proposal is superior in that it can handle more human reasoning tasks.

ABSTRACT. Logic programs with graded modality (LPGM) combine ideas underlying graded modal logic and answer set programming. Logic programming under answer set semantics is extended with a new graded modality M_[lb:ub] where lb and ub are natural numbers satisfying lb <= ub. The modality is used to precede a literal in rules bodies, and thus allows for the representation of graded introspections: M_[lb:ub] F intuitively means: it is known that the number of belief sets where F is true is between lb and ub. We define the semantics of Logic programs with graded modality, give an algorithm for computing solutions of LPGMs, and show the effectiveness of the formalism for modeling two problems.

ABSTRACT. Algorithmic decision theory can be roughly defined as the design and study of languages and methods for expressing and solving various classes of decision problems, including: decision under uncertainty, sequential decision making, multicriteria decision making, collective decision making, and strategic interactions in distributed decision making. A decision problem is specified by two main components: the preferences of the agent(s); and the beliefs the agent(s) has (have) about the initial state of the world and its evolution, and possibly about the beliefs and preferences of other agents. Computational tasks involve, among others: the construction and refinement of the problem, through learning and elicitation tasks; the search for a centralized decision (for an agent or a group of agents); the impact of selfish behaviour in decentralized, multi-agent decision contexts. Logic in algorithmic decision theory can be useful as a declarative representation language for the various components of the problems, and as a generic problem solving tool. The combination of both allow for representing and solving complex decision making problems. This talk points to some research issues at the meeting point of logic and algorithmic decision theory.