A wide variety of nonmonotonic semantics can be expressed as approximators defined under AFT (Approximation Fixpoint Theory). Using traditional AFT theory, it is not possible to define approximators that rely on information computed in previous iterations of stable revision. However, this information is rich for semantics that incorporate classical negation into nonmonotonic reasoning. In this work, we introduce a methodology resembling AFT that can utilize priorly computed upper bounds to more precisely capture semantics. We demonstrate our framework's applicability to hybrid MKNF (minimal knowledge and negation as failure) knowledge bases by extending the state-of-the-art approximator.

Combining the closed-world reasoning of answer set programming (ASP) with the open-world reasoning of ontologies broadens the space of applications of reasoners. Disjunctive hybrid MKNF knowledge bases succinctly extend ASP and in some cases without increasing the complexity of reasoning tasks. However, in many cases, solver development is lagging behind. As the result, the only known method of solving disjunctive hybrid MKNF knowledge bases is based on guess-and-verify, as formulated by Motik and Rosati in their original work. A main obstacle is understanding how constraint propagation may be performed by a solver, which, in the context of ASP, centers around the computation of \textit{unfounded atoms}, the atoms that are false given a partial interpretation. In this work, we build towards improving solvers for hybrid MKNF knowledge bases with disjunctive rules: We formalize a notion of unfounded sets for these knowledge bases, identify lower complexity bounds, and demonstrate how we might integrate these developments into a solver. We discuss challenges introduced by ontologies that are not present in the development of solvers for disjunctive logic programs, which warrant some deviations from traditional definitions of unfounded sets. We compare our work with prior definitions of unfounded sets.

We present an approach to representing large sets of mutual exclusions, also known as mutexes or mutex constraints. These are the types of constraints that specify the exclusion of some properties, events, processes, and so on. They are ubiquitous in many areas of applications. The size of these constraints for a given problem can be overwhelming enough to present a bottleneck for the solving efficiency of the underlying solver. In this paper, we propose a novel graph-theoretic technique based on multicliques for a compact representation of mutex constraints and apply it to domain-independent planning in ASP. As computing a minimum multiclique covering from a mutex graph is NP-hard, we propose an efficient approximation algorithm for multiclique covering and show experimentally that it generates substantially smaller grounding size for mutex constraints in ASP than the previously known work in SAT.

We investigate the problem of cost-optimal planning in ASP. Current ASP planners can be trivially extended to a cost-optimal one by adding weak constraints, but only for a given makespan (number of steps). It is desirable to have a planner that guarantees global optimality. In this paper, we present two approaches to addressing this problem. First, we show how to engineer a cost-optimal planner composed of two ASP programs running in parallel. Using lessons learned from this, we then develop an entirely new approach to cost-optimal planning, stepless planning, which is completely free of makespan. Experiments to compare the two approaches with the only known cost-optimal planner in SAT reveal good potentials for stepless planning in ASP. The paper is under consideration for acceptance in TPLP.

A state-of-the-art criterion to evaluate the importance of a given learned clause is called Literal Block Distance (LBD) score. It measures the number of distinct decision levels in a given learned clause. The lower the LBD score of a learned clause, the better is its quality. The learned clauses with LBD score of 2, called glue clauses, are known to possess high pruning power which are never deleted from the clause databases of the modern CDCL SAT solvers. In this work, we relate glue clauses to decision variables. We call the variables that appeared in at least one glue clause up to the current search state glue variables. We first show experimentally, by running the state-of-the-art CDCL SAT solver MapleL-CMDist on benchmarks from SAT Competition-2017 and 2018, that branching decisions with glue variables are categorically more inference and conflict efficient than nonglue variables. Based on this observation, we develop a structure aware CDCL variable bumping scheme, which bumps the activity score of a glue variable based on its appearance count in the glue clauses that are learned so far by the search. Empirical evaluation shows effectiveness of the new method over the main track instances from SAT Competition 2017 and 2018.

In this abstract, we present our study of exploring the SAT search space via random-sampling, with the goal of improving Conflict Directed Clause Learning (CDCL) SAT solvers. Our proposed CDCL SAT solving algorithm expSAT uses a novel branching heuristic expVSIDS. It combines the standard VSIDS scores with heuristic scores derived from exploration. Experiments with application benchmarks from recent SAT competitions demonstrate the potential of the expSAT approach for improving CDCL SAT solvers.

Finite chase, or alternatively chase termination, is an important condition to ensure the decidability of existential rule languages. In the past few years, a number of rule languages with finite chase have been studied. In this work, we propose a novel approach for classifying the rule languages with finite chase. Using this approach, a family of decidable rule languages, which extend the existing languages with the finite chase property, are naturally defined. We then study the complexity of these languages. Although all of them are tractable for data complexity, we show that their combined complexity can be arbitrarily high. Furthermore, we prove that all the rule languages with finite chase that extend the weakly acyclic language are of the same expressiveness as the weakly acyclic one, while rule languages with higher combined complexity are in general more succinct than those with lower combined complexity.

Finite chase, or alternatively chase termination, is an important condition to ensure the decidability of existential rule languages. In the past few years, a number of rule languages with finite chase have been studied. In this work, we propose a novel approach for classifying the rule languages with finite chase. Using this approach, a family of decidable rule languages, which extend the existing languages with the finite chase property, are naturally defined. We then study the complexity of these languages. Although all of them are tractable for data complexity, we show that their combined complexity can be arbitrarily high. Furthermore, we prove that all the rule languages with finite chase that extend the weakly acyclic language are of the same expressiveness as the weakly acyclic one, while rule languages with higher combined complexity are in general more succinct than those with lower combined complexity.

Logic programs with abstract constraint atoms proposed by Marek and Truszczynski are very general logic programs.They are general enough to captureaggregate logic programs as well asrecently proposed description logic programs.In this paper, we propose a well-founded semantics for basic logic programs with arbitrary abstract constraint atoms, which are sets of rules whose heads have exactly one atom. Weshow that similar to the well-founded semanticsof normal logic programs, it has many desirable properties such as that it can becomputed in polynomial time, and is always correct with respect to theanswer set semantics. This paves the way for using our well-founded semanticsto simplify these logic programs. We also show how our semantics can be applied toaggregate logic programs and description logic programs, and compare itto the well-founded semantics already proposed for these logic programs.

We present a new approach to characterizing the semantics for the integration of rules and first-order logic in general, and description logics in particular, based on a circumscription characterization of answer set programming, introduced earlier by Lin and Zhou. We show that both Rosati's semantics based on NM-models and Lukasiewicz's answer set semantics can be characterized by circumscription, and the difference between the two can be seen as a matter of circumscription policies. This approach leads to a number of new insights. First, we rebut a criticism on Lukasiewicz's semantics for its inability to reason for negative consequences. Second, our approach leads to a spectrum of possible semantics based on different circumscription policies, and shows a clear picture of how they are related. Finally, we show that the idea of this paper can be applied to first-order general stable models.