ABSTRACT. The specifications of various domains include properties which persist, at the latest, by some future time. In multi-agent voting protocols, e.g., a proposed motion may be seconded at the latest by some specified time. Contemporary applications additionally require efficient temporal pattern matching over high-velocity streams, for computing the values of such properties with minimal latency. To address these issues, we present a formal computational framework, based on the Event Calculus, that handles effectively streams including events with temporally-constrained effects. We present the syntax, semantics, reasoning algorithms and complexity of our proposed framework. Furthermore, we present an empirical analysis on large synthetic and real data streams.

ABSTRACT. Scheduling methods are important for effective production and logistics management, where tasks need to be allocated and performed by limited resources. In particular, the Job-shop Scheduling Problem (JSP) is a well-known and challenging combinatorial optimization problem in which tasks sharing a machine are to be arranged in sequence such that encompassing jobs can be completed as early as possible. Given that already moderately sized JSP instances can turn out as highly combinatorial, so that neither optimal schedules nor the runtime to termination of complete optimization methods is known, efficient approaches to approximate good-quality schedules are of interest. In this paper, we propose problem decomposition into time windows whose operations can be successively scheduled and optimized by means of multi-shot ASP solving. From a computational perspective, decomposition aims to split highly complex scheduling tasks into better manageable subproblems with a balanced number of operations, so that good-quality or even optimal partial solutions can be reliably found in a small fraction of runtime. Regarding the feasibility and quality of solutions, problem decomposition must respect the precedence of operations within their jobs, and partial schedules optimized by time windows should yield better global solutions than obtainable in similar runtime on the full problem. We devise and investigate a variety of decomposition strategies in terms of the number and size of time windows as well as heuristics for choosing their operations. Moreover, we incorporate time window overlapping and compression techniques into the iterative scheduling process in order to counteract limitations of window-wise optimization restricted to partial schedules. Our experiments on JSP benchmark sets of several sizes show that successive optimization by multi-shot ASP solving leads to substantially better schedules within the runtime limit than global optimization on the full problem, where the gap increases with the number of operations to schedule.

ABSTRACT. Quantitative extensions of logic programming often require the solution of so called *second level* inference tasks, i.e., problems that involve a third operation, such as maximization or normalization, on top of addition and multiplication, and thus go beyond the well-known weighted or algebraic model counting setting of probabilistic logic programming under the distribution semantics. We introduce Second Level Algebraic Model Counting (2AMC) as a generic framework for this kind of problems. As 2AMC is to (algebraic) model counting what forall-exists-SAT is to propositional satisfiability, it is notoriously hard to solve. First level techniques based on Knowledge Compilation (KC) have been adapted for specific 2AMC instances by imposing variable order constraints on the resulting circuit. However, those constraints can severely increase the circuit size and thus decrease the efficiency of such approaches. We show that we can exploit the logical structure of a 2AMC problem to omit parts of these constraints, thus limiting the negative effect. Furthermore, we introduce and implement a strategy to generate a sufficient set of constraints statically, with a priori guarantees for the performance of KC. Our empirical evaluation on several benchmarks and tasks confirms that our theoretical results can translate into more efficient solving in practice.

ABSTRACT. We address the problem of verifying that the functions of a program meet their contracts, specified by pre/postconditions. We follow an approach based on Constrained Horn Clauses (CHCs) by which the verification problem is reduced to the problem of checking satisfiability of a set of clauses derived from the given program and contracts. We consider programs that manipulate Algebraic Data Types (ADTs) and a class of contracts specified by using catamorphisms, that is, functions defined by a simple recursion schema on the given ADT. We show by several examples that state-of-the-art CHC satisfiability tools are not effective at solving the satisfiability problems obtained by direct translation of the contracts into CHCs. Then, we propose a transformation technique that removes the ADT terms from CHCs, thereby deriving new sets of clauses that work on basic sorts, such as integers and booleans. We prove that the transformation is sound, in the sense that if the transformed set of CHCs is satisfiable, then so is the original set. We also prove that the transformation always terminates for the class of contracts specified by catamorphisms. Finally, we present the experimental results obtained by an implementation of our technique when verifying many non-trivial contracts relative to list sorting and tree manipulating programs.

ABSTRACT. Answer set programming (ASP) is a popular declarative programming paradigm with a wide range of applications in artificial intelligence. Oftentimes, when modeling an AI problem with ASP, and in particular when we are interested beyond simple search for optimal solutions, an actual solution, differences between solutions, or number of solutions of the ASP program matter. For example, when a user aims to identify a specific answer set according to her needs, or requires the total number of diverging solutions to comprehend probabilistic applications such as reasoning in medical domains. Then, there are only certain problem specific and handcrafted encoding techniques available to navigate the solution space of ASP programs, which is oftentimes not enough. In this paper, we propose a formal and general framework for interactive navigation toward desired subsets of answer sets analogous to faceted browsing. Our approach enables the user to explore the solution space by consciously zooming in or out of sub-spaces of solutions at a certain configurable pace. We illustrate that weighted faceted navigation is computationally hard. Finally, we provide an implementation of our approach that demonstrates the feasibility of our framework for incomprehensible solution spaces.

ABSTRACT. While answer-set programming (ASP) is a successful approach to declarative problem solving, optimisation can still be a challenge for it. Large-neighbourhood search (LNS) is a metaheuristic technique where parts of a solution are alternately destroyed and reconstructed, which has high but untapped potential for ASP solving. We present a framework for LNS optimisation for ASP, in which neighbourhoods can be specified either declaratively as part of the ASP encoding, or automatically generated by code. In the full paper, we illustrate the framework on different optimisation problems, some of which are notoriously difficult, including shift planning and a parallel machine scheduling problem from semi-conductor production which demonstrate the effectiveness of the LNS approach.

ABSTRACT. Answer Set Programming (ASP), a modern development of Logic Programming, is one of the foremost paradigms in the important branch of artificial intelligence (AI) known as Knowledge Representation and Reasoning. ASP enables a natural integration of Computing and AI education with STEM subjects. This integration addresses a widely acknowledged challenge in K-12 education, and early empirical results on ASP-based integration are promising. Although ASP is considered a simple language when compared with imperative programming languages, programming errors can still be a significant barrier for students. This is particularly true for K-12 students who are novice users of ASP. And while categorizing errors and measuring their difficulty has yielded insights into imperative languages like Java, little is known about the types and difficulty of errors encountered by K-12 students using ASP. To address this, we collected high school student programs submitted during a 4-session seminar teaching an ASP language known as SPARC. From error messages in this dataset, we identify a collection of error classes, then measure how frequently each error occurs and how difficult it is to resolve. We find that errors related to the sort system of SPARC are the most worthy of emphasis from educators based on their frequency of occurrence and resolution difficulty.

ABSTRACT. The Model Reconciliation Problem (MRP) was introduced to address issues in explainable AI planning. A solution to a MRP is an explanation for the differences between the models of the human and the planning agent (robot). Most approaches to solving MRPs assume that the robot, who needs to provide explanations, knows the human model. This assumption is not always realistic in several situations (e.g., the human might decide to update her model and the robot is unaware of the updates).

In this paper, we propose a dialog-based approach for computing explanations of MRPs under the assumptions that (i) the robot does not know the human model; (ii) the human and the robot share the set of predicates of the planning domain and their exchanges are about action descriptions and fluents’ values; (iii) communication between the parties is perfect; and (iv) the parties are truthful. A solution of a MRP is computed through a dialog, defined as a sequence of rounds of exchanges, between the robot and the human. In each round, the robot sends a potential explanation, called proposal, to the human who replies with her evaluation of the proposal, called response. We develop algorithms for computing proposals by the robot and responses by the human and implement these algorithms in a system that combines imperative means with answer set programming using the multi-shot feature of clingo.

ABSTRACT. Weighted knowledge bases for description logics with typicality have been recently considered under a “concept-wise” multipreference semantics (in both the two-valued and fuzzy case), as the basis of a logical semantics of MultiLayer Perceptrons (MLPs). In this paper we consider weighted conditional ALC knowledge bases with typicality in the finitely many-valued case, through three different semantic constructions. For the boolean fragment LC of ALC we exploit ASP and asprin for reasoning with the concept-wise multipreference entailment under a φ-coherent semantics, suitable to characterize the stationary states of MLPs. As a proof of concept, we experiment the proposed approach for checking properties of trained MLPs.

ABSTRACT. Many industrial applications require finding solutions to challenging combinatorial problems. Efficient elimination of symmetric solution candidates is one of the key enablers for high-performance solving. However, existing model-based approaches for symmetry breaking are limited to problems for which a set of representative and easily-solvable instances is available, which is often not the case in practical applications. This work extends the learning framework and implementation of a model-based approach for Answer Set Programming to overcome these limitations and address challenging problems, such as the Partner Units Problem. In particular, we incorporate a new conflict analysis algorithm in the Inductive Logic Programming system ILASP, redefine the learning task, and suggest a new example generation method to scale up the approach. The experiments conducted for different kinds of Partner Units Problem instances demonstrate the applicability of our approach and the computational benefits due to the first-order constraints learned.

ABSTRACT. In the field of automated planning, an action is called reversible when other actions can be applied in order to revert the effects of this action and return to the original state. In recent years, there has been renewed interest in this topic, which led to novel results in the widely known STRIPS formalism and the PDDL planning language.

In this paper, we aim to solve the computational problem of deciding action reversibility in a practical setting, applying recent advances in the field of logic programming. In particular, a quantified extension of Answer Set Programming (ASP) named ASP with Quantifiers (ASP(Q)) has been proposed by Amendola, Ricca, and Truszczynski, which allows for stacking logic programs by quantifying over answer sets of the previous layer. This language is well-suited to express encodings for the action reversibility problem, since this problem naturally contains a quantifier alternation. In addition, a prototype solver for ASP(Q) is currently developed. We make use of the ASP(Q) language to offer an encoding for action reversibility, and then report on preliminary benchmark results on how well this encoding performs compared to classical ASP.

ABSTRACT. In many industries, scheduling is a key component to efficient management of resources and, thus, ensuring competitiveness and success of companies by minimizing the waste of time and money. In this work, we propose a Multi-resource Partial-ordering Flexible Job-shop Scheduling (MPFJSS) formulation to capture scheduling scenarios where partially-ordered sequences of operations must be scheduled on multiple required resources, such as tools and specialists. The resources are flexible and can process one or more operations based on their characteristics. We have built a model using Answer Set Programming (ASP) in which the execution time of operations is determined using Difference Logic. Furthermore, we introduced two multi-shot strategies that identify the time bounds and find a schedule while minimizing the total tardiness. We conducted experiments on a set of instances provided by a semiconductor manufacturer, and the results showed that the proposed model could find schedules for 87 out of 91 real-world instances.