This research is partially supported by NSF grants 1757207, 1812619, 1812628, and 1914635.

DeepStochLog: Neural Stochastic Logic Programming (Extended Abstract)

Introduction

The integration of neural and symbolic learning methods is high on the research agenda. It is popular to use (variants of) logic programs to represent the available symbolic knowledge and use Prolog-like mechanisms to generate differentiable structures. This can often be achieved by introducing probability into these neural logic programming models, cf. [1]. Most notably, one distinguishes probabilistic from stochastic logic programs (PLPs vs SLPs). The more popular PLPs [2] are based on a possible worlds semantics, which extends probabilistic graphical models, while the SLPs [4] are based on stochastic grammars. The difference can also be described as a random graph vs a random walk model. So far, the emphasis in neural-symbolic computation has been on the PLP approach [3]. To fill this gap, we introduce DeepStochLog, a neural stochastic logic programming approach. It incorporates ideas from DeepProbLog, such as the neural predicate. The neural predicate encapsulates neural networks to cope with sub-symbolic data such as images. Without loss of generality, we base DeepStochLog on stochastic definite clause grammars (SDCGs) as this notation is easier to introduce and use and results in a sequence-based model. SDCGs are a probabilistic unification-based grammar formalism, which is translatable to SLPs. The experimental evaluation shows that DeepStochLog scales a lot better than neural probabilistic logic programs and achieves state-of-the-art results on challenging neural-symbolic learning tasks.

Stochastic Definite Clause Grammars

Stochastic Definite Clause Grammars have their roots in Context-Free Grammars (CFG). A context-free grammar G is a 4-tuple (V,Σ,S,R), with V the set of non-terminals, Σ the set of terminals, S ∈ V the starting symbol and R a set of rewrite rules of the form N → S₁, ..., S_k where N is a non-terminal and S_i either terminals or non-terminals. Definite clause grammars (DCGs) extend CFGs with logic. Instead of using non-terminals, they use logical atoms, i.e. a(t₁,...,t_n). Stochastic definite clause grammars (SDCGs) extend DCGs by associating probabilities to the rules. This is identical to how Probabilistic Context-Free Grammars (PCFG) extend CFGs. The rules take the form p_i :  : N → S₁, ..., S_k, where p_i is a probability. SDCGs require that the probabilities for the rules defining a single non-terminal predicate sum to 1.

DeepStochLog

DeepStochLog integrates neural networks and SDCGs by introducing neural definite clause grammars (NDCG). More formally, DeepStochLog allows for specifying an SDCG that additionally supports neural definite clause grammar rules. These are statements of the form: nn(m,ℐ,𝒪,𝒟) :: nt → g₁, ..., g_n where nt is an atom, g₁, ..., g_n is a goal (a conjunction of atoms), and the ℐ = [I₁,...,I_m] and 𝒪 = [O₁,...,O_L] are lists of variables occurring in g₁, ..., g_n and nt. The nn declaration states that m is a neural network taking variables I₁, …, I_m as input and producing a probability distribution over output variables O₁, ..., O_L as output. 𝒟 = [D₁,...,D_L] is a list of unary predicates, where D_i defines the domain of output variable O_i.

Intuitively, a neural rule serves as a template for multiple SDCG rules sharing the same non-terminal predicate as head. They allow a neural network to compute the corresponding probabilities (that sum to 1). To do so, the neural network can take as inputs the arguments of the atoms in the rule. This allows for arguments of the rules to be subsymbolic information, like images.

DeepStochLog can be used to parse input sequences and compute the probability that the given NDCG parses a sequence. This is achieved by parsing the sequence using standard Prolog DCG techniques with SLG resolution to get an AND/OR tree (= parse tree). This tree is then translated into an arithmetic circuit by substituting AND nodes with multiplication, OR nodes with summation and leaves with corresponding probabilities. The probability that a given start symbol generates a given sequence of terminals is simply computed by evaluating the corresponding arithmetic circuit bottom-up.

Results

DeepStochLog reaches state-of-the-art predictive performance on neural-symbolic tasks. When applied to parsing addition expressions or more general arithmetic expressions encoded as sequences of images of handwritten symbols, DeepStochLog outperforms state-of-the-art neural symbolic systems in parsing accuracy. In Table 1, we compare DeepStochLog with DeepProbLog [3] and NeurASP [5].

DeepStochLog outperforms PLP-based systems in terms of inference times thanks to the different semantics and tabling. DeepStochLog scales better than competitors when parsing longer sequences. While competitors either timeout or strongly degrade their performances, DeepStochLog handles long sequences with no performance degradation. As a consequence, DeepStochLog can be applied to semi-supervised classification in real citation networks, a task out of the scope of PLP-based frameworks.

DeepStochLog goes beyond grammars and can encode more general programs. DeepStochLog can exploit the equivalence between SDCGs and SLPs. Thus, it can encode more general programs that cannot be directly mapped to a grammar. As a consequence, DeepStochLog programs can be directly translated from DeepProbLog programs, by ensuring that the SDCG semantics is satisfied. We showed that DeepStochLog has the same performances as DeepProbLog on word algebra problems.

Figure 1: The AND/OR tree for the goal e(1) and the sentence [, +, ]. Failing branches are omitted.

Acknowledgements

This research was funded by the Research Foundation-Flanders (FWO-Vlaanderen), the KU Leuven Research Fund, the European Research Council (ERC), EU contracts #694980 and #952215, The Flemish Government and the Knut and Alice Wallenberg Foundation.

Bibliography

1. Luc De Raedt, Sebastijan Dumančić, Robin Manhaeve & Giuseppe Marra (2020): From Statistical Relational to Neuro-Symbolic Artificial Intelligence. In: Proceedings of the Twenty-Ninth International Conference on International Joint Conferences on Artificial Intelligence, doi:https://doi.org/10.24963/ijcai.2020/688.
2. Luc De Raedt & Angelika Kimmig (2015): Probabilistic (logic) programming concepts. Machine Learning 100(1), pp. 5–47, doi:https://doi.org/10.1007/s10994-015-5494-z.
3. Robin Manhaeve, Sebastijan Dumanˇci´c, Angelika Kimmig, Thomas Demeester & Luc De Raedt (2018): DeepProbLog: Neural probabilistic logic programming. 31.
4. Stephen Muggleton (1996): Stochastic logic programs. Advances in Inductive Logic Programming 32, pp. 254–264.
5. Zhun Yang, Adam Ishay & Joohyung Lee (2020): NeurASP: Embracing neural networks into answer set programming. In: 29th International Joint Conference on Artificial Intelligence (IJCAI 2020), doi: https://doi.org/10.24963/ijcai.2020/243.

Transforming Gringo Rules into Formulas in a Natural Way

The semantics of some rules in the input language of the grounder gringo [2,3] can be characterized in terms of a translation into the language of first-order logic [5, Section 6]. The translation $\tau^*$, defined in that paper, transforms a mini-gringo rule into a first-order sentence that has the same meaning under the stable model semantics. It can be used to relate strong equivalence between gringo programs to a similar condition on first-order formulas [5, Proposition 4]. It is used also in the design of the proof assistant anthem [1].

The result of applying $\tau^*$ can be quite complicated, even for short rules. In this paper [4], we describe a set of mini-gringo rules—we call them regular—that can be transformed into formulas in a natural way. The new translation contributes to our understanding of the relationship between the language of gringo and first-order languages.

References

1. Jorge Fandinno, Vladimir Lifschitz, Patrick Lühne & Torsten Schaub (2020): Verifying Tight Programs with Anthem and Vampire. Theory and Practice of Logic Programming 20, pp. 735–750, doi:10.1017/S1471068420000344.
2. Martin Gebser, Amelia Harrison, Roland Kaminski, Vladimir Lifschitz & Torsten Schaub (2015): Abstract Gringo. Theory and Practice of Logic Programming 15, pp. 449–463, doi:10.1017/S1471068415000150.
3. Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Marius Lindauer, Max Ostrowski, Javier Romero, Torsten Schaub & Sven Thiele (2019): Potassco User Guide. Available at https://github.com/potassco/guide/releases/.
4. Vladimir Lifschitz (2021): Transforming Gringo Rules into Formulas in a Natural Way. In: Proceedings of the 17th European Conference on Logics in Artificial Intelligence, JELIA '21. Springer, pp. 421–434, doi:10.1007/978-3-030-75775-5_28.
5. Vladimir Lifschitz, Patrick Lühne & Torsten Schaub (2019): Verifying Strong Equivalence of Programs in the Input Language of gringo. In: Proceedings of the 15th International Conference on Logic Programming and Non-monotonic Reasoning, LPNMR '19. Springer, pp. 270–283, doi:10.1007/978-3-030-20528-7_20.
6. Vladimir Lifschitz, David Pearce & Agustin Valverde (2007): A characterization of strong equivalence for logic programs with variables. In: Proceedings of the 9th International Conference on Logic Programming and Non-monotonic Reasoning, LPNMR '07. Springer, pp. 188–200, doi:10.1007/978-3-540-72200-7_17.

Solving a Multi-resource Partial-ordering Flexible Variant of the Job-shop Scheduling Problem with Hybrid ASP

1. Introduction

Job-shop Scheduling (JSS) ([7]) is one of the most well-known scheduling problems in which a set of machines are used to execute given jobs, represented as sequences of operations, and the goal is to complete the jobs as soon as possible. Extensions like flexible ([1]) and multi-resource ([2]) JSS generalize the allocation of a machine and additional resources for an operation to suit practical scheduling applications. In this work, we consider a Multi-resource Partial – ordering Flexible JSS (MPF-JSS) problem, where multiple resources are needed for executing operations, and jobs consist of partially-ordered sequences of operations to be completed. More specifically, we distinguish machines and engineers as two separate sets of resources required to perform an operation. Flexibility lies in the choice among several resources with the required skills in each category. The goal is to determine the best possible execution order and allocation of operations to resources for minimizing the total tardiness of jobs wrt. their deadlines. We model the MPF-JSS problem by an encoding in Answer Set Programming (ASP) with Difference Logic (DL) ([4]) and take advantage of multi-shot solving ([5]). DL constraints allow for compactly expressing timing requirements, avoiding grounding issues that would otherwise be encountered when a feasible schedule necessitates a large number of time points. By means of multi-shot solving, we implement two strategies to identify upper time bounds on feasible schedules whose tardiness is further subject to minimization. We tested our proposed model on a dataset representing ten operational days of an Infineon Fault Analysis lab. Our experiments yield success to optimize schedules for 87 out of 91 real-world instances, while only a very small number of jobs can be handled without multi-shot solving.

2. Modeling MPF-JSS with Hybrid ASP

We consider a scheduling problem in which different resources are interrelated to process the upcoming operations. In particular, MPF-JSS is an extension of the classical JSS problem where three additional aspects are considered: (a) Multi-resources – several categories of resources can be required to execute an operation; (b) Partially-ordered – some operations cannot be executed before completing their predecessors and others are unaffected by such constraints; and (c) Flexible – an operation can be performed by a variety of available resources. More specifically, an MPF-JSS instance consists of a set of jobs, characterized by a partially ordered set of operations to be performed, where each operation needs to be allocated to some machine and (possibly) an engineer with the required skills. The following constraints must be respected: (i) once an operation starts, it cannot be interrupted; (ii) each resource can perform only one operation at a time; (iii) the execution times of operations of the same job cannot overlap; and (iv) operations must be scheduled according to the partial order given by jobs.

We propose two multi-shot ASP modulo DL solving strategies. The first approach incrementally increases the upper bound on the tardiness of each job in order to identify a limit for which schedules are feasible. That is, search starts with the tardiness bound 0, and if this yields unsatisfiability (UNSAT), the bound is incremented by a constant, set by a parameter of our Python control script on top of clingo[DL] ([6]), and this process proceeds until some schedule is found. Figure 1 illustrates an execution of the incremental search strategy, where the bound on jobs' tardiness is increased in steps of size 2 until satisfiability (SAT) is obtained with the time bound 8. ASP optimization methods are then used to find a schedule minimizing the total tardiness, i.e., the sum of delays over jobs completed after their deadlines.

The second approach performs an exponential binary search for the exact tardiness bound at which schedules get feasible. As displayed in Figure 2, the increment on the bound is gradually increased up to step size 4 for finding the first schedule with the time bound 8. A binary search scheme then successively halves the step size for converging to the exact bound, 7 in this case, for which schedules are feasible, whose total tardiness is subject to ASP optimization in the last phase of the multi-shot solving process.

3. Results

We conducted experiments on a set of real-world instances of the MPF-JSS problem representing the operations at ten days randomly selected from the work records of an Infineon Fault Analysis lab. The instances yield the following approximate number of components based on the dimensions of the studied lab: (i) 50 operation kinds; (ii) 75 machines; and (iii) 45 engineers. For each of the selected days, the number of jobs ranges between 30 and 50. We further split each instance into up to ten sub-instances by picking 5, 10, 15, 20, etc. of the respective jobs, which resulted in a total of 91 instances of varying size.

For each obtained instance, we ran three solving strategies with clingo[DL] (version 1.1.0): (1) single-shot – standard ASP modulo DL program with a tardiness bound precomputed using a heuristic; (2) inc – the incremental multi-shot variant with a constant step size of 20 time points; and (3) exp – the exponential multi-shot solving approach. We restricted each solver run to 2 hours wall clock time on an Intel 3930K workstation with 64GB RAM under Ubuntu 18.05.

Figure 3 shows a cactus plot comparing the solving performance of the two multi-shot approaches and the single-shot version as baseline. The latter times out on all instances with more than 15 jobs and merely succeeds to optimize schedules on instances with 15 jobs for two of the ten days. The two multi-shot approaches significantly outperform the single-shot version. While the incremental strategy yields optimized schedules for 85 out of 91 instances, the exponential multi-shot variant scales up to 87 instances. This advantage is due to tighter tardiness bounds identified by the exponential strategy, thus reducing the efforts for ASP optimization to minimize the total tardiness. Given that a lower tardiness bound is more restrictive, the incremental variant manages to find better schedules than the exponential strategy for three instances, where the total tardiness improvement amounts to 80 time points on average.

Figure 1: Incremental approach
Figure 2: Exponential approach	Figure 3: Cactus plot of solving times

References

1. Peter Brucker & Rainer Schliel (1990): Job-shop scheduling with multi-purpose machines. Computing 45(4), pp. 369–375, doi:10.1007/BF02238804.
2. Stéphane Dauzère-Pérès, W. Roux & Jean Lasserre (1998): Multi-resource shop scheduling with resource flexibility.. EJOR 107(2), pp. 289–305, doi:10.1016/S0377-2217(97)00341-X.
3. Giulia Francescutto, Konstantin Schekotihin & Mohammed El-Kholany (2021): Solving a multi-resource partial-ordering flexible variant of the job-shop scheduling problem with hybrid ASP. In: Proceedings of the European Conference on Logics in Artificial Intelligence (JELIA 2021), Springer, pp. 313–328. doi:10.1007/978-3-030-75775-5_21
4. Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Max Ostrowski, Torsten Schaub & Philipp Wanko (2016): Theory solving made easy with clingo 5. In: Technical Communications of the International Conference on Logic Programming (ICLP 2016), Leibniz International Proceedings in Informatics, pp. 2:1–2:15. doi:10.4230/OASIcs.ICLP.2016.2.
5. Martin Gebser, Roland Kaminski, Benjamin Kaufmann & Torsten Schaub (2019): Multi-shot ASP solving with clingo. TPLP 19(1), pp. 27–82, doi:10.1017/S1471068418000054.
6. Tomi Janhunen, Roland Kaminski, Max Ostrowski, Sebastian Schellhorn, Philipp Wanko & Torsten Schaub (2017): Clingo goes linear constraints over reals and integers. TPLP 17(5-6), pp. 872 – 888, doi:10.1017/S1471068417000242.
7. Selmer Martin Johnson (1954): Optimal two-and three-stage production schedules with setup times included. Naval Research Logistics Quarterly 1(1), pp. 61–68, doi:10.1002/nav.3800010110

Efficient Datalog Rewriting for Query Answering in TGD Ontologies

Background

Ontology-mediated query (OMQ) concerns answering a query w.r.t. an ontology as virtual schemata. In this paper, we consider ontologies consisting of existential rules (a.k.a. Datalog$\pm$ rules or tuple generating dependencies (TGDs)) [1,2], which are a family of expressive ontology languages that cover Datalog and many Horn description logics, including the core dialects of DL-Lite and $\mathcal{EL}$, which underlay the OWL 2 Profiles. A OMQ consists of a finite set of existential rules $\Sigma$ and a conjunctive query (CQ) $q$, denoted $\Sigma_q$.

There are two major approaches for answering OMQ, the chase-based approach and the query rewriting approach. The chase-based approach relies on the termination of the chase procedure (a.k.a. forward chaining), and it is shown that computing a full chase can be rather inefficient when query answers depend only on a small portion of it. On the other hand, existing query rewriting systems for existential rules are typically based on first-order rewritings [2,3]. A limitation of such an approach is that it can only handle ontologies and queries that are first-order rewritable. Yet many practical ontologies do not necessarily fall into these classes, such as some ontologies formulated in $\mathcal{EL}$. Even for ontologies and queries that are first-order rewritable, the results of rewriting can suffer from a significant blow up and become difficult for DBMS to handle.

It is shown that taking Datalog as the target query language can lead to much more compact rewritings, yet existing research on Datalog rewriting of existential rules is mostly theoretical, and very few systems have been developed for Datalog rewriting over existential rules that are more general than description logics. In this paper, we fill the gap by presenting both a practical approach and a prototype system for Datalog rewriting and query answering over a wide range of ontologies expressed in existential rules. We also identify classes of ontologies where the rewriting process terminates, introducing a class by combining existing well-accepted classes. We implement a prototype system, Drewer, and experiments show that it is able to handle a wide range of benchmarks in the literature. Moreover, Drewer shows superior performance over state-of-the-art systems on both the compactness of rewriting and the efficiency of query answering.

Our Approach

Our algorithm is based on the notions of piece unification [1] and unfolding [5]. To achieve compactness of rewriting, we separate the results of unfolding into short rules by introducing the so-called separating predicates and reusing such predicates when possible.

Consider a Boolean CQ $q$ expressed as a Datalog rule $\mathsf{Q} \leftarrow\mathsf{A}(U,V,W)\wedge \mathsf{A}(U,V,V) \wedge \mathsf{A}(U,U,W)$ and an existential rule $\sigma_1:\; \exists Y_1.\mathsf{A}(X_1,X_1,Y_1) \leftarrow\mathsf{B}(X_1,Z_1)$. The unfolding of $q$ by $\sigma_1$ gives $\rho_1:\; \mathsf{Q} \leftarrow\mathsf{A}(U,U,U)\wedge \mathsf{B}(U,Z_1)$. And we split the body of $\rho_1$ via a fresh predicate $\mathsf{P}$ to obtain two additional Datalog rules $\rho'_1:\; \mathsf{Q} \leftarrow\mathsf{A}(U,U,U) \wedge \mathsf{P}(U)$ and $\rho''_1:\; \mathsf{P}(U) \leftarrow\mathsf{B}(U,Z_1)$. Rules like $\rho_1$ are auxiliary and will be temporarily kept for further rewriting. For example, $\rho_1$ can be further rewritten by another existential rule $\sigma_2:\; \exists X_2.[\mathsf{A}(X_2,X_2,X_2)\wedge \mathsf{B}(X_2,Y_2)] \leftarrow\mathsf{C}(Y_2)$, whereas $\rho'_1$ and $\rho''_1$ cannot. After the rewriting process is completed, auxiliary rules like $\rho_1$ are removed.

Definition 1. For a Datalog rule $\rho$, an existential rule $\sigma$, and a piece unifier $\mu=\langle H, B, \tau\rangle$ of $\rho$ and $\sigma$, the result of rewriting $\rho$ by $\sigma$ with $\mu$ consists of the following Datalog rules \begin{align} \mathsf{head}(\rho)\tau & \leftarrow\bigwedge(\mathsf{body}(\rho)\setminus B)\tau \wedge \bigwedge \mathsf{body}(\sigma)\tau, \label{eq:0}\\ \mathsf{head}(\rho)\tau & \leftarrow\bigwedge(\mathsf{body}(\rho)\setminus B)\tau \wedge \mathsf{P}(\mathbf{X}),\label{eq:1}\\ \mathsf{P}(\mathbf{X}) & \leftarrow\bigwedge \mathsf{body}(\sigma)\tau, \label{eq:2} \end{align} where $\mathbf{X} = (\mathbf{X}_{\rho} \cup \mathcal{V}_{\mathsf{body}(\rho)\setminus B})\tau \cap \mathbf{X}_{\sigma}\tau$, and $\mathsf{P}$ is a fresh predicate with arity $|\mathbf{X}|$, called a separating predicate.

To avoid repetitively introducing fresh separating predicates, we reuse them through a labelling function. The rewriting of an OMQ $\Sigma_q$, denoted as $\mathsf{rew}(\Sigma_q)$, consists of all the resulting Datalog rules in a sequence of rewriting as above except for the auxiliary rules. $\mathsf{rew}(\Sigma_q)$ is finite if a fixpoint is reached in finite steps. The correctness of our rewriting is shown below.

Proposition 1. For an OMQ $\Sigma_q$, $\mathsf{rew}(\Sigma_q)$ is a Datalog rewriting of $\Sigma_q$ whenever $\mathsf{rew}(\Sigma_q)$ is finite.

We have also introduced several new Datalog rewritable classes based on variants of our Datalog rewriting methods. An ontology $\Sigma$ is separable if for each atomic query $q$, the variant of $\mathsf{rew}(\Sigma_q)$ that does not generate auxiliary rules is a Datalog rewriting of $\Sigma_q$. Intuitively, the condition requires that the bodies of the Datalog rules generated during rewriting can be separated. The class of separable ontologies is denoted $\mathsf{Sep}$, and we show that the existing $\mathsf{Shy}$ class [4], which was originally introduced to guarantee the termination of a special form of chase, is a subclass of $\mathsf{Sep}$.

Theorem 1. $\mathsf{Shy} \subset \mathsf{Sep}$.

The separable condition can be too restrictive, and we revise the condition to allow blocks of, instead of individual, body atoms to be separately rewritten. We also associate each block $B$ from the initial OMQ or generated during the rewriting with a fresh predicate $\mathsf{P}_B$, called a block predicate, which generalises the notion of separating predicates. Next, we define an ontology $\Sigma$ to block expandable if for each block $B$ consisting of more than one atoms, the collection of rules that can be applied in recursively rewriting atoms in $B$ can be syntatically verified as a finite unification set [1]. The class of block expandable ontologies is denoted $\mathsf{BExp}$ and it is a concrete class whose membership can be verified syntactically. The class of $\mathsf{BExp}$ contains several well known classes, such as linear ($\mathsf{Lin}$), sticky ($\mathsf{Stky}$) [2], and $\mathsf{aGRD}$ (that is, ontologies whose graphs of rule dependencies are acyclic) [1].

Theorem 2. $\mathsf{Lin}\cup \mathsf{Stky}\cup \mathsf{aGRD}\cup \mathsf{Shy}\subset \mathsf{BExp}$.

Experiments

We have implemented a prototype system, Drewer (Datalog REWriting for Existential Rules), and evaluated the performance of our system on several commonly used ontologies for ontology-mediated query answering.

Table 1 shows the evaluations on query rewriting, where we compared Drewer with state-of-the-art query rewriting systems on the size of rewriting and time efficiency. The sizes are measured by the numbers of rules and the times are in milliseconds. "TO" denotes time out whereas a "-" means the system could not handle the OMQ (or reported errors). For Graal, its rewriting sizes are $x+y$, where $x$ is the number of CQs in the rewriting and $y$ is the number of Datalog rules corresponding to its so-called compiled pre-orders.

References

1. Jean-François Baget, Michel Leclère, Marie-Laure Mugnier & Eric Salvat (2011): On rules with existential variables: Walking the decidability line. Artificial Intelligence Journal, 175(9-10):1620–1654, doi:10.1016/j.artint.2011.03.002.
2. Andrea Calì, Georg Gottlob & Andreas Pieris (2012): Towards more expressive ontology languages: The query answering problem. Artificial Intelligence Journal, 193:87–128, doi:10.1016/j.artint.2012.08.002.
3. Mélanie König, Michel Leclère, Marie-Laure Mugnier & Michaël Thomazo (2015): Sound, complete and minimal UCQ-rewriting for existential rules. Semantic Web, 6(5):451–475, doi:10.3233/SW-140153.
4. Nicola Leone, Marco Manna, Giorgio Terracina & Pierfrancesco Veltri (2019): Fast Query Answering over Existential Rules. ACM Transactions on Computational Logic, 20(2):12:1–12:48, doi:10.1145/3308448.
5. Zhe Wang, Kewen Wang & Xiaowang Zhang (2018): Forgetting and Unfolding for Existential Rules. In: Proceedings of the 32nd AAAI Conference on Artificial Intelligence, pp. 2013–2020.

ApproxASP - A Scalable Approximate Answer Set Counter (Extended Abstract)

Abstract

Introduction

Approximate Counting

Approximate counting tries to compute the number of solutions using a probabilistic algorithm. Therefore, assume that $\mathsf{Sol}(I)$ consists of the set of solutions for a problem instance $I$. The approximation algorithm takes instance $I$, a real $\epsilon > 0$ called tolerance, and a real $\delta$ with $0 < \delta \leq 1$ called confidence as input. The output is a real number $\mathit{cnt}$, which estimates the cardinality of $\mathsf{Sol}(I)$ based on the parameters $\epsilon$ and $\delta$ following the inequality $\Pr[\frac{|\mathsf{Sol}(I)|}{(1 + \epsilon)} \leq \mathit{cnt} \leq (1 + \epsilon) \cdot |\mathsf{Sol}(I)|] \geq 1 - \delta$. The central idea of the approximate model counting approach is the use of hash functions to partition the answer sets for a program $P$ into roughly equal small cells. Then pick a random cell and scale it by the number of cells to obtain an $\epsilon$-approximate estimate of the model count. Note that apriori we do not know the distribution of answer sets. We have to perform good hashing without the knowledge of the distribution of answer sets, i.e., partition the $\mathsf{AS}(P)$ into cells such that each cell has roughly equal number of answer sets. Interestingly, this can be resolved by using a $k$-wise independent hash function. In the context of approximate sampling and counting techniques, the most exploited hash family is $\mathcal{H}_{xor}$ [6], which is also called parity constraints.

Intuitively, a parity constraint makes sure that an even or odd number of its atoms occur in an answer set of the program. In fact, the ASP-Core-2 language already allows for representing parity constraints using aggregate rules. Unfortunately, such a construction is quite impractical for two reasons. First, it would require us to add far too many auxiliary variables for each new parity constraint, and second, we would suffer from the known inadequacy to scale due to grounding. Hence, we follow an incremental ``propagator''-based implementation when solving parity constraints. We extend clingo by full XOR solving by using Han and Jiang's Gauss-Jordan elimination (GJE) [11], which is implemented within the state-of-the-art SAT solver Cryptominisat [12].

Actual approximate counting works as follows: We use an already evolved algorithm from the case of propositional satisfiability and lift it to ASP. The $\mathsf{ApproxASP}$ algorithm takes as input an ASP program $P$, an independent support $I$ for $P$ (which can also just be all atoms of the program), a tolerance $\epsilon$ $(0 < \epsilon \leq 1)$, and a confidence $\delta$ with $0 < \delta \leq 1$. First, sampled counts and the number of cells are initialized. Then, we compute a threshold $pivot$ that depends on $\epsilon$ to determine the chosen value of the size of a small cell. Next, we check whether the input program $P$ has at least a pivot number of answer sets projected to $I$ (Enum-k-AS); otherwise, we are trivially done and return $\mathsf{AS}(P)$. Subsequently, the algorithm continues and calculates a value that determines how often we need to sample for the input confidence $\delta$. Next, we divide the search space and sample a cell at most $r$ times using the function DivideNSampleCell. If the attempt to split into at least 2 cells works, represented by a non-zero number of cells, we store the count and estimate the total count by taking the number of cells times the answer sets count within the sampled cell. Finally, the estimate of the count is the median of the stored estimates.

Table 1: The runtime performance comparison of (C) clingo, (D) DynASP, (G) Ganak, (AMC) ApproxMC, and (AAS) ApproxASP on all considered instances.

		C	D	G	AMC	AAS
Normal	#Instances	1500	1500	1500	1500	1500
	#Solved	738	47	973	1325	1323
	PAR-2	5172	9705	3606	1200	1218
Disjunctive	#Instances	200	200	200	200	200
	#Solved	177	0	0	0	185
	PAR-2	1372	10000	10000	10000	795

Empirical Work.

Conclusion

References

1. Gerhard Brewka, Thomas Eiter & Mirosław Truszczyński (2011): Answer set programming at a glance. In: Communications of the ACM 54, no. 12, pp. 92-103, doi:10.1145/2043174.2043195.
2. Martin Gebser, Roland Kaminski, Benjamin Kaufmann & Torsten Schaub (2012) Answer set solving in practice. In: Synthesis lectures on artificial intelligence and machine learning 6, no. 3, pp. 1-238. doi:10.2200/S00457ED1V01Y201211AIM019.
3. Joohyung Lee, Samidh Talsania & Yi Wang (2017) Computing LPMLN using ASP and MLN solvers. In: Theory and Practice of Logic Programming 17, no. 5-6, pp. 942-960. doi:10.1017/S1471068417000400.
4. Johannes Klaus Fichte, Sarah Alice Gaggl, and Dominik Rusovac (2021) Rushing and Strolling among Answer Sets--Navigation Made Easy. In: AAAI Conference on Artificial Intelligence, 36(5), pp. 5651-5659. doi:10.1007/3-540-45241-9_12
5. Monica Nogueira, Marcello Balduccini, Michael Gelfond, Richard Watson & Matthew Barry (2021) An A-Prolog decision support system for the Space Shuttle. In: International symposium on practical aspects of declarative languages, pp. 169-183. doi:10.1007/3-540-45241-9_12
6. Mate Soos, Stephan Gocht & Kuldeep S. Meel (2020) Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling. In: International Conference on Computer Aided Verification, pp. 463-484. doi:10.1007/978-3-030-53288-8_22
7. Johannes Klaus Fichte, Markus Hecher & Florim Hamiti (2021) The model counting competition 2020. In: Journal of Experimental Algorithmics (JEA), pp. 1-26. doi:10.1145/3459080
8. Vladimir Lifschitz & Alexander Razborov (2006) Why are there so many loop formulas?. In: ACM Transactions on Computational Logic (TOCL) 7, no. 2, pp. 261-268. doi:10.1145/1131313.1131316
9. Johannes Klaus Fichte, Markus Hecher, Michael Morak & Stefan Woltran (2017) Answer set solving with bounded treewidth revisited. In: International Conference on Logic Programming and Nonmonotonic Reasoning, pp. 132-145. doi:10.1007/978-3-319-61660-5_13
10. Tomi Janhunen (2006) Some (in) translatability results for normal logic programs and propositional theories. In: Journal of Applied Non-Classical Logics 16, no. 1-2, pp. 35-86. doi:10.3166/jancl.16.35-86
11. Cheng-Shen Han & Jie-Hong Roland Jiang (2012) When boolean satisfiability meets gaussian elimination in a simplex way. In: International Conference on Computer Aided Verification, pp. 410-426. doi:10.1007/978-3-642-31424-7_31
12. Mate Soos, Karsten Nohl & Claude Castelluccia (2009) Extending SAT solvers to cryptographic problems. In: International Conference on Theory and Applications of Satisfiability Testing, pp. 244-257. doi:10.1007/978-3-642-02777-2_24

Exploiting Parameters Learning for Hyper-parameters Optimization in Deep Neural Networks

In the last years, the Hyper-parameter Optimization (HPO) research field has gained more and more attention. Many works have focused on finding the best combination of the Deep Neural Network's (DNN's) hyper-parameters (HPs) or architecture. The state-of-the-art algorithm in terms of HPO is Bayesian Optimization (BO). This is because it keeps track of past results obtained during the optimization and uses this experience to build a probabilistic model mapping HPs to a probability density of the objective function. BO builds a surrogate probabilistic model of the objective function, finds the HPs values that perform best on the surrogate model and updates it with new results. In this work, a system was developed, called Symbolic DNN-Tuner which logically evaluates the results obtained from the training and the validation phase and, by applying symbolic tuning rules, fixes the network architecture, and its HPs, therefore improving performance. Symbolic DNN-Tuner improve BO applied to DNN by adding an analysis of the results of the network on training and validation sets. This analysis is performed by exploiting rule-based programming, and in particular by using Probabilistic Logic Programming (PLP).

Introduction

This work aims to create a system to drive the training of DNNs by automatizing the choice of HPs analyzing the performance of each training done during the optimization process. This new system (Symbolic DNN-Tuner) extends BO [8, 6] exploiting PLP [7] by mapping some tricks usually used in manual HPs optimization [5] into non-deterministic, and probabilistic Symbolic Tuning Rules (STRs). These rules specify Tuning Actions (TAs) which have the purpose of editing the HPs search space, adding new HPs or updating the network structure without human intervention. Each STR has a weight that determines the probability of application of its TA. At the beginning of the optimization process, the probabilistic weights of STRs are set manually, and then they are refined, after each training, via Learning from Interpretations (LFI) [4] (an inference algorithm available in PLP) based on the improvements obtained or not, for each TA applied in previous training.

The two main parts of Symbolic DNN-Tuner [2, 3] are a first one called Neural Block which manages all aspects regarding the networks (training, validation, HPs search space and application of the TA) and a second one called Symbolic Block that, based on the network performance and computed metrics after each training, diagnoses problems and identifies the (most probable) TA to be applied on the network architecture.

Symbolic DNN-Tuner

As mentioned before, Symbolic DNN-Tuner is a system to drive the training of a DNN, analysing the performance of each training through PLP and automatizing the choice of HPs to obtain a network with better performance. By the analysis of the metrics and the performance of the network, it is possible to identify many problems (e.g., overfitting, underfitting, etc.) that BO is not able to avoid because it works only with a single metric (validation loss or accuracy, training loss or accuracy). When Symbolic DNN-Tuner diagnoses these problems, it changes the search space of HP values or the structure of the network by applying TAs to drive the DNN to a better solution.

Symbolic Block

The Symbolic Block of Symbolic DNN-Tuner is concerned with the analysis of metrics and performance of the trained network. This part is fully developed with ProbLog [1]. The two major contributions of this part are the symbolic analysis and LFI. This block analyses the network metrics like loss and accuracy during both training and validation and produces a diagnosis. From this diagnosis, exploiting the STRs, the block returns the TAs to be applied.

The Symbolic Block's ProbLog program is composed of three parts: Facts, Diagnosis and Tuning. The whole logic program is dynamically created by the union of these three parts at each iteration of the algorithm. Facts memorize metrics obtained from the Neural Block, the Diagnosis section contains the code for diagnosing the DNN's behaviour problems. The Tuning section is composed of the STRs. Through ProbLog inference, we can query this program to obtain the TAs. The extracted TAs are passed to the Neural Block and applied to the DNN structure or the HPs search space.

Listing 1 shows an extract of all STRs in Symbolic DNN-Tuner. The values in the head of the clauses are the probabilistic weights, the action() predicate identifies the TAs. Then, when a problem() is True, we take the TAs with the highest probability and the TAs (e.g., decr_lr if problem(underfitting) is true - decrementing learning rate in case of underfitting) are applied to the network or the HPs search space.

The probabilistic weights are learned from the experience gained from previous iterations. The experience becomes the set of training examples for the LFI program. This program (Listing 2) is composed of two parts: the program and the evidence obtained from the ImprovementChecker module. This module checks whether the last training is better in terms of metrics w.r.t the previously performed training. The LFI program is built dynamically at each iteration of the system. After each training, Symbolic DNN-Tuner checks the improvement of the network. The improvement is a boolean value and it is used to build the evidence. The aim is to reward with greater probability those TAs that have led to improvements. In this way, Symbolic DNN-Tuner can learn which TA was better and consequently favours it over the others.

Now, with the ProbLog program updated with the just calculated new probabilities for STRs, we can query the program for the probabilities of a given atom. For clarity purposes, we report an extract of ProbLog code in Listing 3.

Listing 3: Extract of Logic section of Symbolic DNN-Tuner

In Listing 3 we can see the facts, the logic code for the metrics analysis and problem identification and the STRs under FACTS, DIAGNOSIS-PROBLEMS} and TUNING} section respectively. At the end of the program we can see the queries.

The FACTS contains the history of the accuracy and the loss during training phase and validation phase (a([]), l([]), va([]) and vl([]) respectively). itacc() and itloss() are two thresholds used to diagnose underfitting.

This system was tested on three dataset: CIFAR10, CIFAR100 and CIMA dataset. The first two datasets are for benchmarking purpose and the last is a dataset provided by an Italian company called CIMA S.P.A. used as industrial, real case dataset. This dataset is composed by 3200 training images and 640 of validation images of size 256x128 divided in 16 classes. These images are facsimiles of Euro-like banknotes. The performed experiments showed that Symbolic DNN-Tuner performs better than standard Bayesian Optimization on these three datasets in terms of accuracy and loss, and also provides an explanation of the possible reasons for network malfunctioning.

References

1. Anton Dries, Angelika Kimmig, Wannes Meert, Joris Renkens, Guy Van den Broeck, Jonas Vlasselaer & Luc De Raedt (2015): Problog2: Probabilistic logic programming. In: Joint european conference on machine learning and knowledge discovery in databases. Springer, pp. 312–315, doi:10.1007/978-3-319-23461-8_37.
2. Michele Fraccaroli, Evelina Lamma & Fabrizio Riguzzi (2021): Symbolic DNN-Tuner. Machine Learning, pp. 1–26, doi:10.1007/s10994-021-06097-1.
3. Michele Fraccaroli, Evelina Lamma & Fabrizio Riguzzi (2022): Symbolic DNN-Tuner: A Python and ProbLog-based system for optimizing Deep Neural Networks hyperparameters. SoftwareX 17, pp. 100957, doi:10.1016/j.softx.2021.100957.
4. Bernd Gutmann, Ingo Thon & Luc De Raedt (2011): Learning the parameters of probabilistic logic programs from interpretations. In: Joint European Conference on Machine Learning and Knowledge Discovery in Databases. Springer, pp. 581–596, doi:10.1007/978-3-642-23780-5_47.
5. Grégoire Montavon, Geneviève Orr & Klaus-Robert Múller (2012): Neural networks: tricks of the trade 7700. springer, doi:10.1007/978-3-642-35289-8.
6. Martin Pelikan, David E Goldberg & Erick Cantú-Paz (1999): BOA: The Bayesian optimization algorithm. In: Proceedings of the 1st Annual Conference on Genetic and Evolutionary Computation-Volume 1. Morgan Kaufmann Publishers Inc., pp. 525–532. doi:10.1007/978-3-540-32373-0_
7. Fabrizio Riguzzi (2018): Foundations of Probabilistic Logic Programming. River Publishers. isbn:978-877022018-7
8. Jasper Snoek, Hugo Larochelle & Ryan P Adams (2012): Practical bayesian optimization of machine learning algorithms. In: Advances in neural information processing systems, pp. 2951–2959. doi:10.48550/arXiv.1206.2944.

Treewidth-aware Reductions of Normal ASP to SAT — Is Normal ASP Harder than SAT after All? (Extended Abstract)

1 Introduction

Answer Set Programming (ASP) is an active research area of knowledge representation and reasoning. ASP provides a declarative modeling language and problem solving framework for hard computational problems, which has been widely applied. In ASP questions are encoded into rules and constraints that form a program (over atoms), whose solutions are called answer sets. In terms of computational complexity, the consistency problem of deciding the existence of an answer set is well-studied, i.e., the problem is Σ₂^P-complete. Some fragments of ASP have lower complexity though. A prominent example is the class of normal programs, whose consistency problem is NP-complete.

There is also a wide range of more fine-grained studies for ASP, also in parameterized complexity, where certain (combinations of) parameters are taken into account. In parameterized complexity, the “hardness” of a problem is classified according to the impact of a parameter for solving the problem. There, one often distinguishes the runtime dependency of the parameter, e.g., levels of exponentiality [10] in the parameter, required for problem solving. Concretely, under the Exponential Time Hypothesis (ETH) [6], Boolean satisfiability (SAT) is single exponential in the structural parameter treewidth, wheras evaluating Quantified Boolean formulas (quantifier depth two) is double exponential [4].

For ASP there is growing research on treewidth, e.g., [3]. Algorithms of these works exploit structural restrictions (in form of treewidth) of a given program, and often run in polynomial time in the program size, while being exponential only in the treewidth. Intuitively, treewidth gives rise to a tree decomposition, which allows solving numerous NP-hard problems in parts, cf., divide-and-conquer, and indicates the maximum number of variables one has to investigate in such parts during evaluation. There were also competitions and notable progresses in SAT as well as on problems beyond SAT.

Naturally, there are numerous reductions for ASP, e.g., [9, 7], and extensions thereof to SAT. These reductions have been investigated in the context of resulting formula size and number of auxiliary variables. Existing reductions cause only sub-quadratic blow-up in the number of variables, which is unavoidable [8] if the answer sets should be preserved (bijectively). If one considers the structural dependency in form of treewidth, existing reductions could cause quadratic or even unbounded overhead in the treewidth. On the contrary, we present a novel reduction for normal programs that increases the treewidth k at most sub-quadratically (k⋅log(k)). This is indeed interesting as there is a close connection [1] between resolution-width and treewidth, resulting in efficient SAT solver runs on instances of small treewidth. As a result, our reduction could improve solving approaches by means of SAT solvers, e.g., [9]. Then, we establish lower bounds under ETH, for exploiting treewidth for concistency of normal programs. This renders normal ASP “harder” than SAT. At the same time we prove that one cannot significantly improve the reduction, i.e., avoid the sub-quadratic increase of treewidth.

2 Treewidth-Aware Reductions

First, we present the idea of treewidth-aware reductions, where we reduce normal ASP to SAT. This reduction takes an arbitrary normal program Π of treewidth k and constructs a Boolean formula, whose treewidth is bounded by O(k⋅log(k)), thereby being aware of the treewidth increase. This is achieved by guiding the reduction along a structural representation of treewidth, which is a tree decomposition (TD) of Π. Intuitively, every TD of Π is of a certain width, where the treewidth is then the smallest width among every potential TD of Π. Consequently, our treewidth-aware reduction takes a normal program Π, thereby being guided along any TD T of Π of width k, which yields itself a TD of the resulting Boolean formula of width O(k⋅log(k)) that functionally depends on T . The reduction takes up the existing idea of level mappings [9, 7], which, however, needs to be applied for a local part of the program, as indicated by TD T , in order to ensure treewidth-awareness. This application of level mappings [9, 7] that are not applied globally, i.e., for every atom at once, ensures that the treewidth of the resulting Boolean formula does not arbitrarily increase. However, the shift from global to local level mappings comes at the cost of losing a one-to-one correspondence between answer sets of Π and satisfying assignments of the resulting formula. Still, the construction yields the following novel result.

Observe that this seems to be in contrast to classical complexity, where a subquadratic overhead is only unavoidable whenever bijectively capturing the answer sets via satisfying assignments of a Boolean formula, cf., [8]. In an extended version [5] of this work, we provide an implementation of the treewidth-aware reduction and outline its usability, which we also empirically verify along applications.

Towards Novel Hardness Insights. The idea of treewidth-aware reductions can be even applied in a more general setting, which is then the key to finally establish the following main result of the paper.

Observe that Theorem 2 also shows that the reduction of Theorem 1 can probably not be significantly improved. Recently, this lower bound result and its insights led to the development of a family of program classes that are between normal programs and tight programs [2], reflecting the hardness of this lower bound. Each program class of this family is characterized by its “distance” to a tight program.

3 Conclusion

The curiosity of studying and determining the hardness of ASP and the underlying reasons has attracted the attention of the community for a long time. This work discusses the question from a different angle, which hopefully will provide new insights into the hardness of ASP and foster follow-up work. The results indicate that, at least from a structural point of view, deciding the consistency of ASP is harder than SAT, since ASP programs might compactly represent structural dependencies within the formalism. We hope this work might reopen the quest to study treewidth for ASP solving, similarly to SAT [1].

References

Applications of Answer Set Programming to Smart Devices and Large Scale Reasoning (Extended Abstract)*

1. Introduction

Over the last years, the development by the scientific community of robust and efficient systems supporting Answer Set Programming (ASP) [8, 2, 3], an expressive [6] logic programming paradigm proposed in the area of non-monotonic reasoning, fostered the development of a significant number of applications in several contexts (e.g., Artificial Intelligence, Information Integration, Knowledge Management, Healthcare, Workforce Management, Diagnosis, Workflows, Optimization, and more - we refer the reader to the original article [12] for some references).With the growth of the use of ASP in industry, also effective development tools have been introduced, capable of supporting programmers, knowledge engineers and organizations in managing complex projects in real-world domains [7, 9, 5, 4, 11]. Nevertheless, practical applications scenarios have been constantly evolving; we observed, in fact, the availability of computing devices that are getting smaller and smaller (e.g., Smartphones, Smart Devices, Raspberry, etc.) along with the production and availability of heterogeneous data that are getting bigger and bigger.

In this paper, we present DLV Large Scale (DLV-LS), a novel advanced platform for the development of ASP-based applications performing declarative-based reasoning tasks over data-intensive applications, possibly on Smart Devices. The platform heavily relies on DLV [10, 1], one of the most widespread ASP systems in industry, that has been engineered by the DLVSystem company and extended to obtain DLV-LS. The framework encompasses DLV Mobile Edition (DLV-ME), an ASP based solver for Android systems and Raspberry devices, and DLV Enterprise Edition (DLV-EE), an ASP-based platform, accessible by REST interfaces, for large-scale reasoning over Big Data, classical relational database systems, and NoSQL databases. DLV-LS enables Smart Devices to both locally perform reasoning over data generated by their own sensors and properly interact with DLV-EE when more computational power is needed for harder tasks, possibly over bigger centralized data. The resulting DLV-LS system was also equipped by an Integrated Development Environment relying on the extension of the most comprehensive IDE for ASP called ASPIDE [7] making easy the development of ASP solutions for DLV-LS.

(a) Architecture of DLV-LS (left figure). (b) IDE for DLV-LS (right figure).
Figure 1: DLV-LS Architecture and the Integrated Development Environments for DLV-LS.

2. The DLV-LS System

The DLV-LS system (fig. 1a) consists of the following components: (i) DLV-ME, the mobile version of DLV that works on Android and Raspberry systems (Smart Devices); (ii) DLV-EE, emerges from the integration of different versions of DLV exploiting all most recent and advanced features, and, moreover, interacting with Big Data systems and external database systems (both relational and NoSQL). DLV-ME can natively execute logic programs as long as the input is small and the complexity of the logic programs is not high: consider for example the case of an Android ASP based navigator which can recalculate a path locally, or a Raspberry placed on a road that can make local reasoning for traffic control. As a consequence, when the system needs to take advantage of greater computing power, the DLV-EE framework can be invoked using the REST services. In such a way, besides DLV-ME systems, also any other system that wants to use DLV-EE can do it my making REST invocations.

The DLV-EE system is composed by modules for performing (i) distributed reasoning over Big Data systems through the Apache Hadoop system, (ii) reasoning tasks on Relational Database systems and, finally, (iii) reasoning tasks on NoSQL database systems, using, in our case, the Elasticsearch and MongoDB systems.

In order to develop DLV-LS based solutions, our idea consisted of making a synergy of multiple Integrated Development Environments (IDEs) suitably adapted for our purpose (see fig. 1b). In particular, for the development of DLV-ME based solutions for Android and Raspberry, we implemented a synergy between the ASPIDE [7] environment (for the definition of logic programs) and the Android Studio/Eclipse environments for Android/Raspberry solutions. Finally, for the development of solutions that directly exploit DLV-EE, on the one hand it is possible to develop software tools that make use of DLV-EE by accessing the REST services directly, and second we extended the ASPIDE environment in order to exploit the REST services for developing ASP programs that make use of DLV-EE.

For more details about DLV-LS and to download the components, the reader can refer to https: //www.mat.unical.it/ricca/aspide/dlvls.

Acknowledgments. This work has been partially supported by (i) POR CALABRIA FESR-FSE 2014-2020, project "DLV Large Scale: un sistema per applicazioni di Intelligenza Artificiale in architetture data-intensive e mobile", CUP J28C17000220006, (ii) PRIN PE6, Title: "Declarative Reasoning over Streams", funded by MIUR, CUP:H24I17000080001, (iii) PON-MISE MAP4ID, Title: "Multipurpose Analytics Platform 4 IndustrialData", funded by MISE, CUP: B21B19000650008, (iv) PON-MISE S2BDW, Title: "Smarter Solution in the Big Data World", funded by MISE, CUP: B28I17000250008.

* This paper is partially supported by the company DLVSystem Ltd, Italy.

References

1. Mario Alviano, Francesco Calimeri, Carmine Dodaro, Davide Fuscà, Nicola Leone, Simona Perri, Francesco Ricca, Pierfrancesco Veltri & Jessica Zangari (2017): The ASP System DLV2. In Marcello Balduccini & Tomi Janhunen, editors: Logic Programming and Nonmonotonic Reasoning, Springer International Publishing, Cham, pp. 215-221, doi:10.1007/978-3-319-61660-5_19
2. Gerhard Brewka, Thomas Eiter & Mirosław Truszczyński (2011): Answer Set Programming at a Glance 54(12). Available at 10.1145/2043174.2043195.
3. Francesco Calimeri, Wolfgang Faber, Martin Gebser, Giovambattista Ianni, Roland Kaminski, Thomas Krennwallner, Nicola Leone, Marco Maratea, Francesco Ricca & Torsten Schaub (2020): ASP-Core-2 Input Language Format. Theory and Practice of Logic Programming 20(2), pp. 294-309, doi:10.1017/S1471068419000450.
4. Francesco Calimeri, Davide Fuscà, Stefano Germano, Simona Perri & Jessica Zangari (2018): Fostering the Use of Declarative Formalisms for Real-World Applications: The EmbASP Framework. New Generation Computing 37, doi:10.1007/s00354-018-0046-2.
5. Francesco Calimeri, Stefano Germano, Eliana Palermiti, Kristian Reale & Francesco Ricca (2018): Developing ASP Programs with ASPIDE and LoIDE. KI - Künstliche Intelligenz 32, doi:10.1007/s13218-018-0534-z.
6. Thomas Eiter, Georg Gottlob & Heikki Mannila (1997): Disjunctive Datalog 22(3). Available at 10.1145/261124.261126.
7. Onofrio Febbraro, Kristian Reale & Francesco Ricca (2011): ASPIDE: Integrated Development Environment for Answer Set Programming. In James P. Delgrande & Wolfgang Faber, editors: Logic Programming and Nonmonotonic Reasoning, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 317-330, doi:10.1007/978-3-642-20895-9_37
8. Michael Gelfond & Vladimir Lifschitz (1991): Classical Negation in Logic Programs and Disjunctive Databases. New Generation Computing 9, pp. 365-385, doi:10.1007/BF03037169. Available at http://www.cs.utexas.edu/users/ai-lab?gel91b.
9. Stefano Germano, Francesco Calimeri & Eliana Palermiti (2017): LoIDE: a web-based IDE for Logic Pro-gramming - Preliminary Technical Report. CoRR abs/1709.05341. arXiv:1709.05341
10. Nicola Leone, Gerald Pfeifer, Wolfgang Faber, Thomas Eiter, Georg Gottlob, Simona Perri & Francesco Scarcello (2006): The DLV System for Knowledge Representation and Reasoning. ACM Trans. Comput. Logic 7(3), p. 499-562. Available at https://doi.org/10.1145/1149114.1149117.
11. Johannes Oetsch, Jörg Pührer & Hans Tompits (2011): The SeaLion has Landed: An IDE for Answer-Set Programming-Preliminary Report. CoRR abs/1109.3989. arXiv: 1109.3989
12. Kristian Reale, Francesco Calimeri, Nicola Leone & Francesco Ricca (2022): Smart Devices and Large Scale Reasoning via ASP: Tools and Applications. In James Cheney & Simona Perri, editors: Practical Aspects of Declarative Languages - 24th International Symposium, PADL 2022, Philadelphia, PA, USA, January 17-18, 2022, Proceedings, Lecture Notes in Computer Science 13165, Springer, pp. 154-161, doi:10.1007/978-3-030-94479-7_10 .

Inference and Learning with Model Uncertainty in Probabilistic Logic Programs

Introduction

BetaProbLog

1. a set of probabilistic facts $F$. Given a probabilistic fact $p_f::f$, the atom $f$ has probability $p_f$ of being true in a world of the program.
2. a set of beta facts $B$. A fact $beta(\alpha_f,\beta_f)::f$ defines a random variable $X_f \sim Beta(\alpha_f,\beta_f)$ representing the probability of the atom $f$.
3. a set of logic rules $R$ of the form $h \leftarrow b_1,\dots,b_n$ making up a stratified normal logic program.

$X_q =\sum_{H \subseteq F \cup B, q \in \Pi(H)} \prod_{f \in H} w(f) \prod_{f \in (F \cup B) \setminus H} w(\neg f)$

$A(Q) = E_{p(\bf{X})}[g(X_q)] = \int g(X_q) \left( \prod_{i=1}^{|B|} p(X_{f_i}) \right) d\bf{X}$.

Example 1 A BetaProbLog program with two beta facts, one probabilistic fact and two clauses.

$beta(40, 160)::burglary.$
$beta(10, 90)::earthquake.$
$0.8::alarm\_on.$

$alarm \leftarrow alarm\_on, burglary.$
$alarm \leftarrow alarm\_on, earthquake.$

Inference and Learning

Figure 1 Circuit example with samples

$L(\theta) = \sum_{(d, t) \in D} l(A(Q_d,\theta), t)$

Experiments

Question 1: Can BetaProbLog capture the uncertainty with respect to the true model? Following [1]'s experiment, we analyse how well the spread between the inferred and the actual probability is captured. The results were positive, even when the inference algorithm was limited to few samples.

Question 2: Does the inference computation time scale? We investigate BetaProbLog's run time on several translated Bayesian networks (BN). Results show our approach scales very well. For example Hepar2, a BN with $10^3$ parameters, took $1.5$s to execute. Due to the parallelization the evaluation time remained relatively constant regardless of using $10^1$ or $10^4$ samples.

Question 3: Can BetaProbLog recover parameters from target probabilities? This learning task aims to recover the network's missing beta parameters such that the given queries match their target probability. For this we utilise BetaProbLog's parameter learning approach, minimizing the error between the inferred probability of $q$ and the target probability $t$ with the loss function $(A(Q, \theta) - t)^{2}$ where $Q = (q, I)$ and $I$ the identity function. Given enough data, BetaProbLog recovers the parameters.

Conclusion

Acknowledgements

References

1. F. Cerutti, L. M. Kaplan, A. Kimmig & M. Sensoy (2019): Probabilistic Logic Programming with Beta-Distributed Random Variables. In: AAAI, AAAI Press, doi:10.1609/aaai.v33i01.33017769
2. D. Fierens, G. Van den Broeck, J. Renkens, D. Sht. Shterionov, B. Gutmann, I. Thon, G. Janssens & L. De Raedt (2015): Inference and learning in probabilistic logic programs using weighted Boolean formulas. Theory Pract. Log. Program. 15(3), pp. 358−401, doi:10.1017/S1471068414000076
3. E. Hüllermeier & W. Waegeman (2021): Aleatoric and epistemic uncertainty in machine learning: an introduction to concepts and methods. Mach. Learn. 110(3), pp. 457−506, doi:10.1007/s10994−021−05946
4. L. Kaplan, F. Cerutti, M. Sensoy & K. Vijay Mishra (2020): Second-Order Learning and Inference using Incomplete Data for Uncertain Bayesian Networks: A Two Node Example. In: FUSION, IEEE, pp. 1−8, doi:10.23919/FUSION45008.2020.9190472
5. V. Verreet, V. Derkinderen, P. Zuidberg Dos Martires & L. De Raedt (2022): Inference and Learning with Model Uncertainty in Probabilistic Logic Programs. In: AAAI, AAAI Press.

Determining Action Reversibility in STRIPS Using Answer Set Programming with Quantifiers

Introduction

In this extended abstract we summarize a paper published and presented at PADL 2022 [7].

Automated Planning is a field of research that traditionally deals with the problem of generating sequences of actions, called plans, that transform a given initial state of the environment to some goal state [9]. An action, simply put, is a modifier that acts upon and changes the environment. An interesting problem in this field is the question whether an action can be reversed by subsequently applying other actions, thus undoing the effects that the action had on the environment. This problem has been investigated on and off throughout the years [5,3], and has recently received renewed interest [11,6,2].

In our paper, we leverage the translations implemented in plasp [4], and propose an encoding to solve some of the reversibility problems on PDDL domains, restricted, for now, to the STRIPS fragment [8]. This encoding is written in a recently proposed language extension for ASP, namely, ASP with Quantifiers, or ASP(Q) [1], which introduces an explicit way to express quantifiers and quantifier alternations in ASP. Our ASP(Q) encodings are arguably simpler and more readable than the known ASP and ELP encodings [6] for the same problem.

We give a brief overview of STRIPS planning and the ASP(Q) language.

STRIPS Planning.

Let $\mathcal{F}$ be a set of facts, that is, propositional variables describing the environment, which can either be true or false. Then, a subset $s \subseteq \mathcal{F}$ is called a state, which intuitively represents a set of facts considered to be true. An action is a tuple $a = \langle \mathit{pre}(a), \mathit{add}(a), \mathit{del}(a) \rangle$, where $\mathit{pre}(a) \subseteq \mathcal{F}$ is the set of preconditions of $a$, and $\mathit{add}(a) \subseteq \mathcal{F}$ and $\mathit{del}(a) \subseteq \mathcal{F}$ are the add and delete effects of $a$, respectively. An action $a$ is applicable in a state $s$ iff $\mathit{pre}(a) \subseteq s$. The result of applying an action $a$ in a state $s$, given that $a$ is applicable in $s$, is the state $a[s] = (s \setminus \mathit{del}(a)) \cup \mathit{add}(a)$.

Answer Set Programming with Quantifiers (ASP(Q)).

An extension of ASP, referred to as ASP(Q), has been proposed in [1], providing a formalism reminiscent of Quantified Boolean Formulas, but based on ASP. An ASP(Q) program is of the form % $\square_1 P_1 \square_2 P_2 \cdots \square_n P_n : C,$ % where, for each $i \in \{1, \ldots, n\}$, $\square_i \in \{ \exists^{st}, \forall^{st} \}$, $P_i$ is an ASP program, and $C$ is a stratified normal ASP program (e.g. constraints). The intuitive reading of an ASP(Q) program $\exists^{st} P_1 \forall^{st} P_2 \cdots P_n : C$ is that there exists an answer set $A_1$ of $P_1$ such that for each answer set $A_2$ of $P_2$ extended by $A_1$ $\ldots$ such that $C$ extended by $A_n$ is coherent (has an answer set).

Reversibility of Actions

In this section, we review the notion of uniform reversibility, which is a subclass of action reversibility as explained in detail by Morak et al. [11]. Intuitively, we call an action reversible if there is a way to undo all the effects that this action caused, and we call an action uniformly reversible if its effects can be undone by a single sequence of actions irrespective of the state where the action was originally applied.

The notion of uniform reversibility naturally gives rise to the notion of the reverse plan. We say that some action $a$ has a reverse plan $\pi$ iff $a$ is uniformly reversible using the sequence of actions $\pi$. Checking whether an action is uniformly $\phi$-reversible is in $\Sigma^{P}_{2}$ [11].

ASP(Q) Encodings of Reversibility

We use the tool plasp [4] to convert STRIPS planning domains into an ASP format. The basic idea of our encoding is to have an existentially quantified program $P^u_1$ first, which guesses the reverse plan, followed by a universally quantified program $P^u_2$, which creates the trajectories from any choice of the initial state, and the check program $C^u$ will establish whether the trajectory leads back to the initial state, yielding $\Pi^u = \exists^{st}P^u_1 \forall^{st}P^u_2 : C^u$. Each of these programs straightforwardly and intelligebly encodes the relevant guesses and checks.

As opposed to plain ASP, or epistemic extensions thereof, it is also easily possible with ASP(Q) to encode ``non-uniform'' reversibility, where for each state a different reverse plan can appear. Intuitively, instead of encoding ``there exists a plan such that for all initial states it leads back'' here we need an inversion to ``for all initial states there exists a plan that leads back''. But this is fairly straightforward in ASP(Q). For a pre-chosen action to be reversed this gives rise to $\Pi^n = \forall^{st}P^n_1 \exists^{s}P^n_2 : C^n$.

We encourage the reader to consult the main paper [7] for details on these encodings.

Experiments

We have conducted preliminary experiments on universal uniform reversibility, based on experiments from [6]. We used plasp 3.1.1 (https://potassco.org/labs/plasp/), eclingo 0.2.0 (https://github.com/potassco/eclingo) and clingo 5.4.1 (https://potassco.org/clingo/) for the ASP and ELP benchmark set, and the preliminary ASP(Q) solving tool qasp, version 0.1.2, which rewrites ASP(Q) programs to Quantified Boolean Formulas (QBFs) and then use the well-known QuAbS QBF solver [10] (see the benchmark archive for qasp), on a computer with a 2.3 GHz AMD EPYC 7601 CPU with 32 cores and 500 GB RAM running CentOS 8. We have set a timeout of 20 minutes and a memory limit of 16GB (which was never exceeded).

Figure 1: Calculating the unique reverse plan (plan length equals number of facts)

The results are plotted in Figure 1, requiring that solvers output all models that they find (i.e. after finding the first and only model containing a reverse plan, they have to prove that this is also the last model). In general, the ELP and ASP(Q) encodings scale worse than the ASP encoding. However, since these systems solve the same problem from a complexity-theoretic perspective, we see this as an indicator of how much optimization potential is still ``hidden'' for qasp, or any solver for the ASP(Q) language. Due to the elegance of the modelling language, however, we hope that our paper will encourage further development and improvements in the young field of ASP(Q) solvers.

Acknowledgements.

Supported by the S&T Cooperations CZ 05/2019 and CZ 15/2022, by the Czech Ministry of Education, Youth and Sports (Czech-Austrian Mobility program project no. 8J19AT025) and by the OP VVV funded project number CZ.02.1.01/0.0/0.0/16_019/0000765.

References

1. Giovanni Amendola, Francesco Ricca & Miroslaw Truszczynski (2019): Beyond NP: Quantifying over Answer Sets. Theory Pract. Log. Program. 19(5-6), pp. 705–721, doi:10.1017/S1471068419000140.
2. Lukás Chrpa, Wolfgang Faber & Michael Morak (2021): Universal and Uniform Action Reversibility. In: Proc. KR, pp. 651–654, doi:10.24963/kr.2021/63.
3. Jeanette Daum, Álvaro Torralba, Jörg Hoffmann, Patrik Haslum & Ingo Weber (2016): Practical Undoability Checking via Contingent Planning. In: Proc. ICAPS, pp. 106–114. Available at https://www.aaai.org/ocs/index.php/ICAPS/ICAPS16/paper/view/13091/12667.
4. Yannis Dimopoulos, Martin Gebser, Patrick Lühne, Javier Romero & Torsten Schaub (2019): plasp 3: Towards Effective ASP Planning. TPLP 19(3), pp. 477–504, doi:10.1017/S1471068418000583.
5. Thomas Eiter, Esra Erdem & Wolfgang Faber (2008): Undoing the effects of action sequences. J. Applied Logic 6(3), pp. 380–415, doi:10.1016/j.jal.2007.05.002.
6. Wolfgang Faber, Michael Morak & Lukás Chrpa (2021): Determining Action Reversibility in STRIPS Using Answer Set and Epistemic Logic Programming. TPLP 21(5), pp. 646–662, doi:10.1017/S1471068421000429.
7. Wolfgang Faber, Michael Morak & Lukás Chrpa (2022): Determining Action Reversibility in STRIPS Using Answer Set Programming with Quantifiers. In: Proc. PADL, pp. 42–56, doi:10.1007/978-3-030-94479-7_4.
8. Richard Fikes & Nils J. Nilsson (1971): STRIPS: A New Approach to the Application of Theorem Proving to Problem Solving. Artif. Intell. 2(3/4), pp. 189–208, doi:10.1016/0004-3702(71)90010-5.
9. Malik Ghallab, Dana S. Nau & Paolo Traverso (2004): Automated planning - theory and practice. Elsevier.
10. Jesko Hecking-Harbusch & Leander Tentrup (2018): Solving QBF by Abstraction. In: Andrea Orlandini & Martin Zimmermann: Proceedings Ninth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2018, Saarbrücken, Germany, 26-28th September 2018, EPTCS 277, pp. 88–102, doi:10.4204/EPTCS.277.7.
11. Michael Morak, Lukáš Chrpa, Wolfgang Faber & Daniel Fišer (2020): On the Reversibility of Actions in Planning. In: Proc. KR, pp. 652–661, doi:10.24963/kr.2020/65.

A Multi-shot ASP Encoding for the Aircraft Routing and Maintenance Planning Problem (Extended Abstract)

Aircraft routing and maintenance planning are integral parts of the airline scheduling process. We model and solve these combinatorial optimization problems with Answer Set Programming (ASP), contrasting traditional single-shot ASP solving methods to multi-shot solving techniques geared to the rapid discovery of near-optimal solutions to sub-problems of gradually increasing granularity.

Application Domain

Combinatorial optimization problems are usually solved in a single shot, while their size and hardness may sometimes necessitate decomposition into better controllable sub-problems to which some form of local search scales. In this work, we present an approach to solve the Aircraft Routing and Maintenance Planning problem with Answer Set Programming (ASP) [1] by decomposing it, using a time-window approach [2] along with multi-shot solving [3]. Multi-shot ASP solving methods have previously been successfully applied in areas like automated planning [4], automated theorem proving [5], human-robot interaction [6], multi-robot (co)operation [7], and stream reasoning [8]. Presumably closest to our work, which devises multi-shot solving techniques to successively increase the granularity of hard combinatorial optimization problems, is the Asprin system [9] that implements complex user preferences by sequences of queries, yet without considering to unroll the underlying problem representation on the fly.

We address the application domain of airline operation scheduling [10], which consists of six major steps often considered as separate sub-problems, either with or without communication between them.

1. Flight Schedule Preparation: The airline decides on a collection of flights to perform, choosing which airports to serve and at which frequencies to maximize the profit.

2. Fleet Assignment: The next step is to define the type of aircraft that should perform particular flights. Each type of aircraft has different characteristics: total number of seats, fuel consumption, number of first-class seats, number of crew members needed to operate the flight, etc.

3. Aircraft Routing: Each flight gets a specific aircraft assigned, and a sequence of flights assigned to the same plane forms a route. We also need to respect some conditions like airport turnaround time (TAT): the minimum time on ground between two consecutive flights, required to perform operations preparing the aircraft for the next flight.

4. Maintenance Planning: We assign maintenance slots to each aircraft to respect limits defined in terms of a certain number of cycles (i.e., flights), the number of hours from the last maintenance, or hours of flight. Maintenances can only take place at suitable airports (with required equipment and skills), they have a minimum duration, and they need to be performed before the aircraft has reached the given limits. Efficient schedules maximize aircraft usage and keep maintenances low.

5. Crew Scheduling: Next, one needs to assign a crew to operate each flight while respecting all legal restrictions. A preferable solution also aims to fulfill the crew members' personal preferences.

6. Disruption Recovery: The final task is to manage disruptions happening on the day of operation due to unforeseen events such as bad weather conditions, crew strikes, aircraft mechanical failures, airport closures, etc., where the impact of recovery actions like cancellations, delays, diversions, etc. on passenger services ought to remain minimal.

We aim to accomplish Aircraft Routing and Maintenance Planning, subjects of the third and fourth item, in combination, considering one type of maintenance to perform every seven days on each aircraft. To this end, we use the Clingo [3] system for modeling and multi-shot ASP solving, where the satisfaction of TAT constraints, as well as the number of allocated maintenance slots constitute the optimization targets.

Multi-shot Optimization

We devised a multi-shot ASP encoding for Aircraft Routing and Maintenance Planning together with a control script, which decomposes the scheduling task into time windows by iteratively extending the maximum gap admitted between consecutive flights along routes in one-hour steps. The rationale of this approach is that, while long ground times, e.g., a day or more, are admissible, they are usually undesirable yet may be necessary in corner cases, so that imposing hard constraints on the admitted connections may sacrifice the feasibility of schedules. The optimization targets are to minimize the number of TAT violations, i.e., connections scheduled with shorter ground time than typically planned at an airport, in the first place, and the number of allocated maintenance slots as secondary optimization objective. While traditional single-shot solving can at least in principle directly determine a globally optimal schedule among all feasible solutions, multi-shot ASP solving with gradually increasing gaps between consecutive flights tends to initially yield infeasible sub-problems, then first schedules with plenty TAT violations and significant improvements by admitting further connections, and finally solution costs converge such that no more progress is observed when allow ing longer connections or search phases.

In Figure 1, we compare the costs of greedy reference solutions for 20 random instances created by our generation tool [11] to the best schedules obtained with Clingo version 5.4.0 in one hour wall clock time per run, using either traditional single-shot solving or multi-shot solving, respectively. In the multi-shot solving mode, we impose a time limit of 60 seconds for finding/improving a solution within the current time window, and move on to the next step admitting one more hour of ground time between consecutive flights whenever no (improved) schedule is obtained after 60 seconds. In most cases, the best schedules obtained with single-shot solving have higher costs than the greedy reference solutions determined during the instance generation, which indicates that the full Aircraft Routing and Maintenance Planning problem is highly combinatorial, so that one hour solving time does not suffice to reliably compute near-optimal solutions. Better than that, the multi-shot solving mode comes closer to the greedy reference solutions, which are already of good quality by their construction, and improves over them for some of the 20 instances. Due to the high problem combinatorics, neither single- nor multi-shot solving terminate with a provably optimal schedule for any instance, where the multi-shot mode keeps on increasing the gaps of connections when attempts to improve the best solution so far fail.

The multi-shot solving strategies compared in aim to further advance the previous multi-shot mode by means of an early-stop criterion, where a run is aborted after three failed attempts in a row to improve the currently best solution, which cuts the solving time down to less than one hour per instance. When the early-stop mode is run sequentially, as also done with the single- and multi-shot solving approaches before, the solution costs are not reduced any further because runs are aborted rather than going on to increase admissible ground times, yet the solving time taken to converge to schedules of similar quality is significantly reduced. The parallel mode takes advantage of multi-threading running eight complementary search strategies of Clingo, so that an improved solution found by one thread allows all eight threads to continue optimizing without getting aborted by the early-stop criterion. This approach yields very robust multi-shot optimization performance and consistently improves over greedy solutions.

References

1. G. Brewka, J. Delgrande, J. Romero & T. Schaub (2015): asprin: Customizing Answer Set Preferences without a Headache. In: AAAI Proceedings. AAAI Press, pp. 1467-1474, doi:10.1609/aaai.v29i1.9398.
2. K. Chen, D. Lu, Y. Chen, K. Tang, N. Wang & X. Chen (2014): The Intelligent Techniques in Robot KeJia - The Champion of RoboCup@Home 2014. In: RoboCup Proceedings. Springer-Verlag, pp. 130-141, doi:10.1007/978-3-319-18615-3_11.
3. Y. Dimopoulos, M. Gebser, P. Luhne, J. Romero & T. Schaub (2019): plasp 3: Towards Effective ASP Planning. Theory and Practice of Logic Programming 19(3), pp. 477-504, doi:10.1017/S1471068418000583.
4. M. Gebser, R. Kaminski, B. Kaufmann & T. Schaub (2019): Multi-shot ASP Solving with Clingo. Theory and Practice of Logic Programming 19(1), pp. 27-82, doi:10.1007/978-3-319-61660-5_26.
5. M. Gebser, O. Sabuncu & T. Schaub (2011): An Incremental Answer Set Programming Based System for Finite Model Computation. AI Communications 24(2), pp. 195-212, doi:10.3233/aic-2011-0496.
6. A. Jamili (2017): A Robust Mathematical Model and Heuristic Algorithms for Integrated Aircraft Routing and Scheduling, with Consideration of Fleet Assignment Problem. Journal of Air Transport Management 58(C), pp. 21-30., doi:10.1016/j.jairtraman.2016.08.008.
7. V. Lifschitz (2019): Answer Set Programming. Springer-Verlag, doi:10.1007/978-3-030-24658-7.
8. P. Obermeier, J. Romero & T. Schaub (2019): Multi-Shot Stream Reasoning in Answer Set Programming: A Preliminary Report. Open Journal of Databases 6(1), pp. 33-38.
9. B. Schapers, T. Niemueller, G. Lakemeyer, M. Gebser & T. Schaub (2018): ASP-Based Time-Bounded Planning for Logistics Robots. In: ICAPS Proceedings. AAAI Press, pp. 509-517.
10. M. Schutten (1998): Decomposition Methods for Complex Factory Scheduling Problems. European Journal of Operational Research 107(1), pp. 243-244, doi:10.1007/978-1-4615-6329-7_3.
11. P. Tassel & M. Rbaia (2021): A Multi-shot ASP Encoding for the Aircraft Routing and Maintenance Planning Problem. In: JELIA Proceedings. Springer-Verlag, pp. 442-457, doi:10.1007/978-3-030-75775-5_30.

Large-Neighbourhood Search for ASP Optimisation (Extended Abstract)

Abstract

Introduction

Efficient solver technology and a simple modelling language have put answer-set programming (ASP) [6] at the forefront of approaches to declarative problem solving, with a growing number of applications in academia and industry. Many practical applications require optimisation of some objective function, which often is a challenge, as making ASP encodings scale and perform well for the problem instances encountered can be tricky.

Large neighbourhood search (LNS) [7] is a metaheuristic that proceeds in iterations by successively destroying and reconstructing parts of a given solution with the goal to obtain better values for an objective function. For the reconstruction part, complete solvers can be used. While recent work touched LNS in ASP [5], a principled and systematic use is unexplored. This is of particular interest, as ASP is offering problem-solving capacities beyond other solving paradigms such as MIP and CP.

Our main contribution is a framework for LNS optimisation for answer-set solving. To effectively explore different neighbourhoods, we build on the recent solver features of multi-shot solving and solving under assumptions [4]. Multi-shot solving allows us to embed ASP in a more complex workflow that involves tight control over the solver's grounding and solving process. Learned heuristics and constraints can be kept between solver calls and repeated program grounding is effectively avoided. Solving under assumptions is a mechanism by which we can temporally fix parts of a solution between solver calls. While the underlying ideas are generic, we present our framework for the solvers clingo and its extension clingo-dl for difference logic, as well as clingcon for ASP with integer constraints (https://potassco.org/).

Our Python implementation of LNS with ASP in the loop, the solver clingo-lns, is publicly available at http://www.kr.tuwien.ac.at/research/projects/bai/aaai22. Input files for ASP encodings and parameters are set via the command line, --help gives an overview. Solver options include the solver type (clingo, clingo-dl, or clingcon, a global time limit, a time limit for search within a particular neighbourhood, the size of the neighbourhood, and command line arguments to be passed to the solvers. Based on our experience, the arguments that work well for an ASP solver carry over to the use within LNS. The solver supports minimisation and maximisation of hierarchical objective functions as well as minimisation of a single integer variable in clingo-dl mode.

An LNS Framework for ASP

1. We present a system that can be used out of the box with all the supported ASP solvers. Different neighbourhoods can be seamlessly specified in a declarative way as part of the ASP encoding itself. To this end, dedicated predicates are used (no language extension is needed). While neighbourhoods can be specified as part of the ASP encoding, the solver will use random relaxation of the visible atoms specified via #show as the default neighbourhood if no other definition is found. We demonstrate the solver for different optimisation problems in the full paper [3]. In particular, we use the well-known problems Social Golfer and Travelling Salesman, as well as generating smallest sets of clues for Sudoku. Furthermore, we consider an optimisation variant of the Strategic Companies problem and Shift Design [1] as a real-world inspired benchmark. Throughout, LNS with ASP yields improved bounds compared to plain ASP with no or little extra effort.
2. The second way to use LNS with ASP in our framework is by instantiating a Python class that realises the basic LNS loop for a solver. This can be the preferred way for more specialised ASP applications where neighbourhood definitions are easier to specify in an imperative language or when obtaining an initial solution from a construction heuristic instead of the ASP solver is beneficial. As an advanced showcase, we use a challenging parallel machine scheduling problem from industry [2], where we can leverage the capabilities of clingo-dl and improve the state-of-the-art for this problem by using LNS with an efficient construction heuristic to start the search.

Defining Neighbourhoods in ASP

The LNS neighbourhood defines which parts of a solution are kept and which are destroyed in each iteration. Its structure is usually problem specific but generic ones can also be effective. A good neighbourhood is large enough to contain a better solution but sufficiently small for the solver to actually find one. In our framework, one can define it either in a purely declarative way, as part of the encoding and orthogonal to the problem specification, or by using a Python plugin.

As an example, consider the Social Golfer Problem where golfers must be grouped in a weekly schedule such that individuals meet again as little as possible. There, a solution is a weekly schedule that defines which golfer plays in which group; consider a solution for 3 groups of size 3 over 3 weeks:

This schedule can be further optimised as some players meet more than once. A potential neighbourhood could be to unassign random positions in the above schedule; another one could be to destroy entire groups or even weeks, etc. We assume that a schedule is encoded in ASP via predicate plays/3 such that plays(P,W,G) is true if golfer P plays in week W in group G.

To define a neighbourhood in ASP, we introduce two dedicated predicates _lns_select/1 and _lns_fix/2:

• _lns_select/1 is a unary predicate to define a set S of terms. In the LNS loop, a random sample is taken from the terms identified by this select predicate.
• _lns_fix/2 defines a mapping from S to atoms that will be fixed with assumptions between solver calls. The first argument is the atom to fix, the second is the corresponding term from S.

For illustration, if we want to fix random positions of the schedule and therefore relax the rest, we can use the following definitions:

_lns_select((P,W,G)) :- plays(P,W,G).
_lns_fix(plays(P,W,G),(P,W,G)) :- _lns_select((P,W,G)).

Here, atoms over plays/3 are fixed if they match the selected position in the schedule. If we want to fix entire weeks of the schedule, we could use the following rules:

_lns_select(W) :- week(W).
_lns_fix(plays(P,W,G),W) :- _lns_select(W), plays(P,W,G).

Conclusion

Acknowledgments

References

1. Michael Abseher, Martin Gebser, Nysret Musliu, Torsten Schaub & Stefan Woltran (2016): Shift design with answer set programming. Fundamenta Informaticae 147(1), pp. 1-25, doi:10.3233/FI-2016-1396 .
2. Thomas Eiter, Tobias Geibinger, Nysret Musliu, Johannes Oetsch, Peter Skocovsky & Daria Stepanova (2021): Answer-Set Programming for Lexicographical Makespan Optimisation in Parallel Machine Scheduling. In: Proc. 18th International Conference on Principles of Knowledge Representation and Reasoning (KR 2021 ), pp. 280-290, doi:10.24963/kr.2021/27.
3. Thomas Eiter, Tobias Geibinger, Nelson Higuera Ruiz, Nysret Musliu, Johannes Oetsch & Daria Stepanova (2022): Large-Neighbourhood Search for Optimisation in Answer-Set Solving. In: Proc. 36th AAAI Conference on Artificial Intelligence (AAAI-22), http://www.kr.tuwien.ac.at/research/projects/bai/aaai22.pdf.
4. Martin Gebser, Roland Kaminski, Benjamin Kaufmann & Torsten Schaub (2019): Multi-shot ASP Solving with clingo. Theory and Practice of Logic Programming 19(1), pp. 27-82, doi:10.1017/S1471068418000054.
5. Tobias Geibinger, Florian Mischek & Nysret Musliu (2021): Constraint Logic Programming for Real-World Test Laboratory Scheduling. In: Proc. 35th AAAI Conference on Artificial Intelligence (AAAI-21 ), AAAI Press, pp. 6358-6366.
6. Vladimir Lifschitz (2019): Answer Set Programming. Springer, doi:10.1007/978-3-030-24658-7.
7. David Pisinger & Stefan Ropke (2010): Large neighborhood search. In: Handbook of Metaheuristics, Springer, pp. 399-419, doi:10.1007/978-1-4419-1665-5_13.

Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming (Extended Abstract)

Automated commonsense reasoning is essential for building human-like AI systems featuring, for example, explainable AI. Event Calculus (EC) [3, 5] is a family of formalisms that model commonsense reasoning with a sound, logical basis. Previous attempts to mechanize reasoning using EC [4] faced difficulties in the treatment of the continuous change in dense domains (e.g., time and other physical quantities), constraints among variables, default negation, and the uniform application of different inference methods, among others. We propose the use of s(CASP), a query-driven, top-down execution model for Constraint Answer Set Programming, to model and reason using EC. We show how EC scenarios can be naturally and directly encoded in s(CASP) and how it enables deductive and abductive reasoning tasks in domains featuring constraints involving both dense time and dense fluents.

Classical implementations of ASP are limited to variables ranging over discrete and bound domains and use grounding and SAT solving to find out models (called answer sets) of ASP programs. However, reasoning on models of the real world often needs variables ranging over dense domains (domains that are continuous, such as R, or that are not continuous but have an infinite number of elements in any bound, non-singleton interval, such as Q). Dense domains are necessary to accurately represent the properties of some physical quantities, such as time, weight, space, etc.

In [1] we present an approach to modeling Event Calculus using the s(CASP) system [2] as the underlying reasoning infrastructure. The s(CASP) system is an implementation of Constraint Answer Set Programming over first-order predicates which combines ASP and constraints. It features predicates, constraints among non-ground variables, uninterpreted functions, and, most importantly, a top-down, query-driven execution strategy. These features make it possible to return answers with non-ground variables, possibly including constraints among them, and to compute partial models by returning only the fragment of a stable model that is necessary to support the answer to a given query. Thanks to its interface with constraint solvers, sound non-monotonic reasoning with constraints is possible.

This approach achieves more conciseness and expressiveness, in the sense of being able to succinctly express complex computations and reasoning tasks, than other related approaches. Dense domains can be faithfully modeled in s(CASP) as continuous quantities, while in other proposals such domains had to be discretized [4], therefore losing precision or even soundness. Additionally, in our approach the amalgamation of ASP and constraints and its realization in s(CASP) is considerably more natural: under s(CASP), answer set programs are executed in a goal-directed manner so constraints encountered along the way are collected and solved dynamically as execution proceeds – this is very similar to the way in which Prolog was extended with constraints. The implementation of other ASP systems featuring constraints is considerably more complex.

Event Calculus

Event Calculus (presented at length in, for example, [5]) is a formalism for reasoning about events and change, of which there are several axiomatizations. There are three basic, mutually related, concepts in EC: events, fluents, and time points. An event is an action or incident that may occur in the world: for instance, a person dropping a glass is an event. A fluent is a time-varying property of the world, such as the altitude of a glass. A time point is an instant in time. Events may happen at a time point; fluents have a truth value at any time point or over an interval, and their truth values are subject to change upon the occurrence of an event. In addition, fluents may have (continuous) quantities associated with them when they are true.

An EC description consists of a domain narrative and a universal theory. The domain narrative consists of the causal laws of the domain, the known events, and the fluent properties, and the universal theory is a conjunction of EC axioms that encode, for example, the inertia laws.

Translation of the Basic EC axioms into s(CASP): It is related to the translation used by the systems EC2ASP and F2LP [4]. We differ in three aspects that improve performance for a top-down system, fully use s(CASP)'s ability to treat unbound variables, and do not compromise the soundness of the translation. These are: the treatment of rules with negated heads, the possibility of generating unsafe rules, and the use of constraints over dense domains (rationals, in our case).

Translation of a narrative involving continuous change: Let us consider an extension of the water tap example in [6], where we define two possible worlds and added a triggered fluent to describe the ability of s(CASP) to model complex scenarios. In this example, a water tap fills a vessel, whose capacity is either 10 or 16 units, and when the level of water reaches the bucket rim, it starts spilling. Let us present the main ideas behind its encoding, available in Fig. 1.

• Continuous Change: The fluent Level(x) represents that the water is at level x in the vessel. Note the 4/3 factor that relates time and water amount in the Trajectory formulas. As mentioned before, if the underlying solver approximates the numerical operations, water levels could be miscalculated and therefore the answers to some queries could be wrong. The use of CLP(Q) prevents this.
• Triggered Fluent: The fluent Spilling is triggered (lines 12-14) when the water level reaches the rim of the vessel.
• Alternative Worlds: The clauses in lines 3-4 force the vessel capacity to be either 10 or 16, and therefore, they create two possible worlds/models.

Evaluation

We compare EC in s(CASP) with F2LP, which implements Discrete EC and approximates the results that s(CASP) can give. F2LP executes Discrete EC by turning first-order formulas under the stable model semantics into a logic program without constraints that is then evaluated using clingo, an ASP solver. The physical model in Fig. 1 needs continuous quantities but its execution with clingo forces the level of water to be expressed using integers.

Table 1 shows how the additional precision necessary in the F2LP encoding, to avoid failure, increases the execution run-time of clingo by orders of magnitude. On the other hand, s(CASP) does not have to adapt its encoding/queries and its performance does not change.

An undesirable effect of rounding in ASP is that rounding may not only make programs fail, but it may make them succeed with wrong answers. For example, with precision(10), the query holdsAt(level(110),T) holds with T=133 (which would correspond to t = 13.3). This value is not right, and it is due to arithmetic rounding performed during the program execution (the correct value is t = 13.25).

References

[1] Joaquín Arias, Manuel Carro, Zhuo Chen & Gopal Gupta (2022): Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming. Theory and Practice of Logic Programming 22(1), pp. 51–80, doi:10.1017/S1471068421000156.

[2] Joaquín Arias, Manuel Carro, Elmer Salazar, Kyle Marple & Gopal Gupta (2018): Constraint Answer Set Programming without Grounding. Theory and Practice of Logic Programming 18(3-4), pp. 337–354, doi:10.1017/S1471068418000285. Available at https://arxiv.org/abs/1804.11162.

[3] Robert Kowalski & Marek Sergot (1989): A Logic-Based Calculus of Events. In: Foundations of knowledge base management, Springer, pp. 23–55, doi:10.1007/978-3-642-83397-7_2.

[4] Joohyung Lee & Ravi Palla (2009): System F2LP – Computing Answer Sets of First-Order Formulas. In: Logic Programming and Nonmonotonic Reasoning, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 515–521, doi:10.1007/978-3-642-04238-6_51.

[5] Erik T. Mueller (2014): Commonsense reasoning: an event calculus based approach. Morgan Kaufmann, doi:10.1016/B978-0-12-801416-5.00002-4.

[6] Murray Shanahan (1999): The Event Calculus Explained. In: Artificial Intelligence Today, Springer, pp. 409–430, doi:10.1007/3-540-48317-9_17.

Extended Abstract: What do you really want to do? Towards a Theory of Intentions for Human-Robot Collaboration

Consider a robot delivering objects to particular places or people, or stacking objects in desired configurations on a tabletop. Such robots have to reason with different descriptions of uncertainty and prior domain knowledge. Information about the domain often includes commonsense knowledge in the form of statements describing some domain attributes, robot attributes, actions, and defaults such as "books are usually in the library, but cookbooks may be in the kitchen". In addition, the robot extracts information from sensor inputs using algorithms that quantify uncertainty probabilistically, e.g., "I am 95% certain the robotics book is on the table". Although it is difficult to equip robots with comprehensive domain knowledge or provide elaborate supervision, reasoning with incomplete or incorrect information can lead to incorrect or sub-optimal outcomes, particularly in response to unexpected outcomes. For example, a robot that can move only one object at a time may be asked to move two books from the office to the library. After moving the first book to the library, if the robot observes the second book is already in the library or in another room on the way back to the office, it should stop executing the current plan, reason about this unexpected observation, and compute a new plan if necessary. One way to achieve this behavior is to reason about all observations of domain objects and events during plan execution, but this approach becomes computationally unfeasible in complex domains. The architecture described in this paper, on the other hand, achieves the desired behavior by introducing an adapted theory of intentions (ATI) that builds on the fundamental principles of non-procrastination and persistence in the pursuit of a goal. It enables the robot to reason about mental actions and states, automatically identifying and considering the domain observations relevant to the current action and the goal during planning and execution ([3]). We refer to actions in such plans as intentional actions. Our architecture may be viewed as comprising a controller, a logician, and an executor that are tightly- and formally-coupled; a simplified block diagram is provided below. The key characteristics of our architecture are:

• The domain's transition diagrams at two different resolutions are described in an action language, with the fine-resolution diagram defined formally as a refinement of the coarse-resolution diagram. At the coarse resolution, the logician performs non-monotonic logical reasoning with incomplete commonsense domain knowledge, which includes a theory of intentions, producing a sequence of intentional abstract actions for any given goal.
• Each abstract action is implemented as a sequence of concrete actions by the controller by automatically zooming to and directing the logician to reason with the part of the fine-resolution description relevant to the coarse-resolution transition and goal. Each concrete action is executed by the executor using probabilistic uncertainty models; the controller adds the observed and inferred outcomes to the coarse/fine-resolution history.
• The logician reasons with the updated history and continues with the current activity comprising intentional abstract actions only if it will achieve the desired goal. If not, a new activity is computed by the logician and implemented by the controller, which maintains the overall beliefs regarding the state of the domain, and transfers control and information between the components.

Our architecture (see above) builds on the complementary strengths of prior work that used declarative programming to encode a theory of intention and reason about intended actions to achieve a given goal ([1]), and an architecture that introduced step-wise refinement of transition diagrams at two resolutions to support non-monotonic logical reasoning and probabilistic reasoning on robots ([4]). Prior work on the theory of intentions did not consider the uncertainty in sensing and actuation, and did not scale to complex domains. Prior work on the refinement-based architecture, on the other hand, did not include a theory of intentions. The key contributions of our architecture are thus to:

• Enable planning with intentional abstract actions, and with mental states, actions, and beliefs, in the presence of incomplete commonsense domain knowledge, partial observability, and non-deterministic action outcomes; and
• Support scalability to complex domains by restricting fine-resolution reasoning to knowledge and observations relevant to the goal or coarse-resolution abstract action at hand, and by using probabilistic models of uncertainty only when executing concrete actions.

Assume that robot rob_1 is in the kitchen initially, holding book_1 in its hand, and believes that book_2 is in office_2 and the library is unlocked.

1. The goal is to have book_1 and book_2 in the library. The plan is the same for ATI and TP:
   
   move(rob_1, library), putdown(rob_1, book_1), move(rob_1, kitchen), move(rob_1, office_2),
   pickup(rob_1, book_2), move(rob_1, kitchen), move(rob_1, library), putdown(rob_1, book_2)
   
   
2. Assume that as the robot is putting book_1 down in the library, book_2 has been moved (e.g., by a human or other external agent) to the library.
3. With ATI, the robot observes book_2 in the library, reasons and explains the observation as the result of an exogenous action, realizes the goal has been achieved and stops planning and execution.
4. With TP, the robot does not use the observation of book_2, wastes time executing subsequent steps of the plan until it is unable to find book_2 in the library, replans (potentially including prior observation of book_2), and eventually achieves the goal.
5. In a variant of this scenario, the robot does not find book_2 in the library after moving book_1 there. When it moves book_2 to the library, it finds book_1 is no longer there. With TP, the robot stops after the plan is executed, With ATI, the robot realizes that the goal and underlying intention have not been achieved, and computes and executes a new plan.

References

1. Justin Blount, Michael Gelfond & Marcello Balduccini (2015): A theory of intentions for intelligent agents. In: International Conference on Logic Programming and Nonmonotonic Reasoning, Springer, pp. 134-142.
2. Michael Gelfond & Daniela Inclezan (2013): Some Properties of System Descriptions of AL d. Journal of Applied Non-Classical Logics, Special Issue on Equilibrium Logic and Answer Set Programming, 23(1-2), pp. 105-120.
3. Rocio Gomez, Mohan Sridharan & Heather Riley (2021): What do you really want to do? Towards a Theory of Intentions for Human-Robot Collaboration. Annals of Mathematics and Artificial Intelligence, special issue on commonsense reasoning 89, pp. 179-208.
4. Mohan Sridharan, Michael Gelfond, Shiqi Zhang & Jeremy Wyatt (2019): REBA: A Refinement-Based Architecture for Knowledge Representation and Reasoning in Robotics. Journal of Artificial Intelligence Research 65, pp. 87-180.

Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set Programming (Extended Abstract)

s(CASP) [3] is a novel non-monotonic reasoner that evaluates Constraint Answer Set Programs without a grounding phase, either before or during execution. s(CASP) supports predicates and thus retains logical variables (and constraints) both during the execution and in the answer sets. The operational semantics of s(CASP) relies on backward chaining, which is intuitive to follow and lends itself to generating explanations that can be translated into natural language [1]. The execution of an s(CASP) program returns partial stable models: the subsets of the stable models [4] which include only the (negated) literals necessary to support the initial query. s(CASP) has already been applied in relevant fields related to explainable artificial intelligence rule-based systems.

However, in the standard implementation of s(CASP), the global constraints (to which we refer as denials to avoid ambiguity) in a program are checked when a tentative but complete model is computed. This strategy takes a large toll on the performance of programs that generate many tentative models and use denials to discard those that do not satisfy the specifications of the problem.

In [2], we propose a technique termed Dynamic Consistency Checking (DCC) that anticipates the evaluation of denials to discard inconsistent models as early as possible. Before adding a literal to the tentative model, DCC checks whether any denial is violated. If so, this literal is discarded and the evaluation backtracks to look for other alternatives. Using several examples we show that this preliminary implementation can speed up s(CASP) by a factor of up to 90x.

Motivation

A denial such as :- p, q, expresses that the conjunction of atoms p ∧ q cannot be true: either p, or q, or both, have to be false in any stable model. In predicate ASP, the atoms have variables and a denial such as :- p(X), q(X,Y) means that: false ← ∃x, y ( p(x) ∧ q(x, y) ). I.e., p(X) and q(X,Y) cannot be simultaneously true for any possible values of X and Y in any stable model. To ensure that the tentative partial model is consistent with this denial, the compiler generates a rule of the form ∀x, y (chki ↔ ¬( p(x) ∧ q(x, y) ) ), and to ensure that each sub-check (chki ) is satisfied, they are included in the rule nmr_check ← chk1 ∧ ... ∧ chkk ∧ ..., which is transparently called after the program query.

However, this generate-and-test strategy has a high impact on the performance of programs that create many tentative models and use denials to discard those that do not satisfy the constraints of the problem. Well-known examples where this happens, widely used to benchmark LP systems and to highlight the expressiveness of ASP, are the Hamiltonian path problem (hamiltonian.pl) and the n queens benchmark (n_queens.pl).

Outline of the DCC Approach

The main idea behind our proposal is to anticipate the evaluation of the denials to fail and backtrack as early as possible. When an atom involved in a denial is a candidate to be added to a tentative model, the denial is checked to ensure that it is not already violated. By contrast, the classical implementation of s(CASP) checked the tentative model as a whole once it had been completely built. The latter is akin to the generate-and-test approach to combinatorial problems, while the former tries to cut the search early.

In the most general case, DCC can take the form of a constraint-and-test instance. While detecting some denial violations can be performed by just checking the current state of the (partial) candidate model, better, more powerful algorithms can impose additional constraints on the rest of the atoms belonging to the partial model and also on the parts of the denials that remain to be checked.

Evaluation

The implementation of s(CASP) + DCC is available as part of the source code of s(CASP) at https://gitlab.software.imdea.org/ciao-lang/scasp. The benchmarks used or mentioned in this paper are available at http://platon.etsii.urjc.es/~jarias/papers/dcc-padl21.

Table 1 shows the results of the performance comparison (in seconds) and the speedup of s(CASP) with DCC w.r.t. s(CASP) without DCC. For the Hamiltonian path problem, s(CASP) with DCC obtains a speedup ranging from 10.0x to 41.1x, depending on the size of the graph (the larger the graph, the more speedup). The program for the n-queens problem is especially interesting, as it does not have a finite grounding, since the size of the board is not fixed in the code, and thus it cannot be run by other implementations of the stable model semantics. We compare two different versions. The n_queens version includes denials to restrict the acceptable models, while the n_queen_attack includes an attack/3 predicate which checks whether a queen can be placed before actually placing it, and therefore it has no denials.

From the numbers in the table we observe: (i) a speedup for n_queens that ranges from 4.3x to 90.8x, (ii) that the execution time of n_queens_attack does not significantly change whether DCC is used or not, and (iii) that the execution using DCC when denials exist is more efficient (4.1x) than the hand-crafted code, even with the current, preliminary implementation.

Table 2 sheds some additional light on the reasons for the effectiveness of DCC. It shows how many stable models exist, how many candidate models were discarded by nmr_check after they were generated (column "#models discarded – s(CASP)"), how many (partial) candidate models were discarded using DCC (column "#models discarded – s(CASP) + DCC") and how many times the dynamic consistency checking detects an inconsistency and backtracks (column "#DCC detected").

In the n_queens benchmark, as the size of the generated and discarded by s(CASP) without using DCCs grows exponentially; this is of course the reason why its execution time also increases very quickly. If we look at the column "#models discarded – s(CASP) + DCC" we see that, when DCC is active, none of final models is discarded by nmr_check. That means that all models not consistent with the denials were removed early in the execution, while they were being built. We also see that the number of times that DCC rules were activated is much smaller than the number of times that nmr_check was executed – early pruning made it possible to avoid attempting to generate many other candidate models.

The Hamiltonian path benchmark is different and very interesting. The number of models discarded by nmr_check is the same regardless of whether DCC is activated or not, i.e., the DCC could not detect inconsistencies in partially-built, candidate models. The reason for the speedup is that the denials in the Hamiltonian path not only check, but also generate new atoms which are in turn checked by the DCC. This accelerates the execution of nmr_check, making it fail earlier, and it is the cause of the speedup of the Hamiltonian path benchmark.

References

[1] Joaquín Arias, Manuel Carro, Zhuo Chen & Gopal Gupta (2020): Justifications for Goal-Directed Constraint Answer Set Programming. In: Proceedings 36th International Conference on Logic Programming (Technical Communications), EPTCS 325, Open Publishing Association, pp. 59–72, doi:10.4204/EPTCS.325.12.

[2] Joaquín Arias, Manuel Carro & Gopal Gupta (2022): Towards Dynamic Consistency Checking in Goal-Directed Predicate Answer Set Programming. In: 24th International Symposium Practical Aspects of Declarative Languages, PADL 2022, LNCS 13165, Springer, pp. 117–134, doi:10.1007/978-3-030-94479-7_8.

[3] Joaquín Arias, Manuel Carro, Elmer Salazar, Kyle Marple & Gopal Gupta (2018): Constraint Answer Set Programming without Grounding. Theory and Practice of Logic Programming 18(3-4), pp. 337–354, doi:10.1017/S1471068418000285. Available at https://arxiv.org/abs/1804.11162.

[4] Michael Gelfond & Vladimir Lifschitz (1988): The Stable Model Semantics for Logic Programming. In: 5th International Conference on Logic Programming, pp. 1070–1080, doi:10.2307/2275201. Available at http://www.cse.unsw.edu.au/~cs4415/2010/resources/stable.pdf.

Abduction in Probabilistic Logic Programs

Abstract

The representation of scenarios drawn from real-world domains is certainly favored by the presence of simple but powerful languages capable of capturing all facets of the problem. Probabilistic Logic Programming (PLP) [5,11] plays a fundamental role in this thanks to its ability to represent uncertain and complex information [3,10] and the possibility to be integrated in sub-symbolic systems to help the explainability of the models [9]. Several probabilistic logic programming languages based on the so-called distribution semantics [14] have been proposed over the years, among which are PRISM [14], Logic Programs with Annotated Disjunctions (LPADs) [15], and ProbLog [6].

An extension of Logic Programming that can manage incompleteness in the data is given by Abductive Logic Programming (ALP) [7,8]. The goal of abduction is to find the best hypotheses that explain an observed fact, given a set of possible hypotheses called abducibles. With ALP, users can perform logical abduction from an expressive logic model possibly subject to constraints.

An important aspect of real-world data is that observations are often noisy and/or uncertain. Therefore, there is the need to define probabilistic observations to allow ALP to handle this kind of scenarios. This extension can be defined by taking inspiration from probabilistic logic languages.

In the paper titled ``Abduction with Probabilistic Logic Programming under the Distribution Semantics'' [2] published in the International Journal of Approximate Reasoning, we consider the language of LPADs and introduce probabilistic abductive logic programs (PALPs), i.e., probabilistic logic programs including a set of abducible facts and a (possibly empty) set of (possibly probabilistic) integrity constraints (IC). This kind of constraints allows the representation of how strongly one believes that the constraint is true. A PALP defines a probability distribution over abductive logic programs inspired by the distribution semantics of PLP [14] in which, given a query, the goal is to maximize the joint probability of the query and the constraints by selecting the minimal subsets of abducible facts, called probabilistic abductive explanations, to be included in the abductive logic program while ensuring that constraints are not violated.

Consider the following example, used as the running example of the paper: suppose that you want to study some natural phenomena that may happen in the island of Stromboli, which is located at the intersection of two geological faults, one in the southwest-northeast direction, the other in the east-west direction, and contains one of the three volcanoes that are active in Italy. In the model, there may be some variables that describe the land morphological characteristics and some variables that relate the possible events that can occur, such as eruption or earthquake. Moreover, you want to force that some of these cannot be observed together (or it is unlikely that they will be). The goal may consist in finding the optimal combination of variables (representing possible events) that best describes a possible scenario and maximizes its probability. The following program ([4]), which can be tested at https://cplint.eu/e/eruption_abduction.pl, models the possibility that an eruption or an earthquake occurs at Stromboli:
(C1) eruption:0.6;earthquake:0.3 :- sudden_er, fault_rupture(X).
(C2) sudden_er:0.7.
(C3) abducible fault_rupture(southwest_northeast).
(C4) abducible fault_rupture(east_west).
If there is a sudden energy release (sudden_er) under the island and there is a fault rupture (represented as fault_rupture(X)), then there can be an eruption of the volcano on the island with probability 0.6 or an earthquake in the area with probability 0.3. The energy release occurs with probability 0.7 and ruptures may occur along both faults (C3 and C4 are abducibles). The query $q$ = eruption has probability $0.588$ and probabilistic abductive explanation $\Delta_0$ = {fault_rupture(southwest_northeast), fault_rupture(east_west)} If we add an IC to the program stating that a fault rupture cannot happen along both directions at the same time, i.e.,
:- fault_rupture(southwest_northeast), fault_rupture(east_west).
the probabilistic abductive explanations that maximize the probability of the query $q$ and satisfy the IC are either $\Delta_1$ = {fault_rupture(southwest_northeast)} or $\Delta_2$ = {fault_rupture(east_west)}, with probability equal to $0.42$ in both cases. Note that the probabilistic abductive explanation $\Delta_0$ is now forbidden by the constraint.

To perform inference on PALP, we present an extension to the PITA system [13]: given a probabilistic logic program in the form of an LPAD, a set of abducible facts, and a set of (possibly probabilistic) integrity constraints, we want to compute minimal sets of abducible facts (the probabilistic abductive explanation) such that the joint probability of the query and the constraints is maximized. The algorithm is based on Binary Decision Diagrams (BDDs) and was tested on several datasets.

One of the key points of this extension is that it has the version of PITA used to make inference on LPADs as a special case: when both the set of abducibles and the set of constraints are empty, the program is treated as a probabilistic logic program. This has an important implication: we do not need to write an ad hoc algorithm to treat the probabilistic part of the LPAD, we just need to extend the already-existing algorithm. Furthermore, (probabilistic) integrity constraints are implemented by means of operations on BDDs and so they can be directly incorporated in the representation. The extended system has been integrated into the web application ``cplint on SWISH'' [1, 12], available online at https://cplint.eu/.

To test our implementation, we performed several experiments on five synthetic datasets. Empirical results show that the versions with and without constraints have comparable runtimes: this may be due to the constraint implementation that discards some of the solutions. Moreover, PALP with probabilistic or deterministic integrity constraints often require similar inference time. Lastly, through a series of examples, we compare inference on PALP with other related tasks, such as Maximum a Posteriori (MAP), Most Probable Explanation (MPE), and Viterbi proof.

References

1. Marco Alberti, Elena Bellodi, Giuseppe Cota, Fabrizio Riguzzi & Riccardo Zese (2017): cplint on SWISH: Probabilistic Logical Inference with a Web Browser. Intelligenza Artificiale 11(1), pp. 47-64, doi: 10.3233/IA-170105.
2. Damiano Azzolini, Elena Bellodi, Stefano Ferilli, Fabrizio Riguzzi & Riccardo Zese (2022): Abduction with probabilistic logic programming under the distribution semantics. International Journal of Approximate Reasoning 142, pp. 41-63, doi:10.1016/j.ijar.2021.11.003.
3. Damiano Azzolini, Fabrizio Riguzzi & Evelina Lamma (2019): Studying Transaction Fees in the Bitcoin Blockchain with Probabilistic Logic Programming. Information 10(11), p. 335, doi:10.3390/info10110335.
4. Elena Bellodi & Fabrizio Riguzzi (2015): Structure Learning of Probabilistic Logic Programs by Searching the Clause Space. Theory and Practice of Logic Programming 15(2), pp. 169-212, doi:10.1017/S1471068413000689.
5. Luc De Raedt, Paolo Frasconi, Kristian Kersting & Stephen Muggleton, editors (2008): Probabilistic Inductive Logic Programming. LNCS 4911, Springer.
6. Luc De Raedt, Angelika Kimmig & Hannu Toivonen (2007): ProbLog: A Probabilistic Prolog and Its Application in Link Discovery. In Manuela M. Veloso, editor: 20th International Joint Conference on Artificial Intelligence (IJCAI 2007), 7, AAAI Press/IJCAI, pp. 2462-2467.
7. Antonis C. Kakas & Paolo Mancarella (1990): Abductive logic programming. In: Proceedings of NACLP Workshop on Non-Monotonic Reasoning and Logic Programming.
8. Antonis C. Kakas & Paolo Mancarella (1990): Database updates through abduction. In: Proceedings of the 16th VLDB, Morgan Kaufmann, pp. 650-661.
9. Robin Manhaeve, Sebastijan Dumancic, Angelika Kimmig, Thomas Demeester & Luc De Raedt (2018): Deepproblog: Neural probabilistic logic programming. In: Advances in Neural Information Processing Systems, pp. 3749-3759.
10. Arnaud Nguembang Fadja & Fabrizio Riguzzi (2017): Probabilistic Logic Programming in Action. In Andreas Holzinger, Randy Goebel, Massimo Ferri & Vasile Palade, editors: Towards Integrative Machine Learning and Knowledge Extraction, Lecture Notes in Computer Science 10344, Springer, pp. 89-116, doi:10.1007/978-3-319-69775-8_5.
11. Fabrizio Riguzzi (2018): Foundations of Probabilistic Logic Programming: Languages, semantics, inference and learning. River Publishers, Gistrup, Denmark.
12. Fabrizio Riguzzi, Elena Bellodi, Evelina Lamma, Riccardo Zese & Giuseppe Cota (2016): Probabilistic Logic Programming on the Web. Software: Practice and Experience 46(10), pp. 1381-1396, doi: 10.1002/spe.2386.
13. Fabrizio Riguzzi & Terrance Swift (2010): Tabling and Answer Subsumption for Reasoning on Logic Programs with Annotated Disjunctions. In: Technical Communications of the 26th International Conference on Logic Programming (ICLP 2010), LIPIcs 7, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 162-171, doi:10.4230/LIPIcs.ICLP.2010.162.
14. Taisuke Sato (1995): A Statistical Learning Method for Logic Programs with Distribution Semantics. In Leon Sterling, editor: Logic Programming, Proceedings of the Twelfth International Conference on Logic Programming, Tokyo, Japan, June 13-16, 1995, MIT Press, pp. 715-729.
15. Joost Vennekens, Sofie Verbaeten & Maurice Bruynooghe (2004): Logic Programs With Annotated Disjunctions. In Bart Demoen & Vladimir Lifschitz, editors: 20th International Conference on Logic Programming (ICLP 2004), Lecture Notes in Computer Science 3131, Springer, pp. 431-445, doi:10.1007/978-3-540-27775-0_30.

Implementing Stable-Unstable Semantics with ASPTOOLS and Clingo (Extended Abstract)

This extended abstract is a report of the original publication [15] that was presented at the 24th International Symposium on Practical Aspects of Declarative Languages (PADL) 2022.

Answer set programming (ASP) is a declarative programming paradigm for solving search problems efficiently (see, e.g., [5,16] for an overview). The formal semantics of ASP rests on the notion of stable models first proposed for normal logic programs (NLPs) [11] and later generalized for disjunctive logic programs (DLPs) [12]. The known complexity results [6,19] indicate that NLPs subject to stable model semantics cover reasoning problems from the first level of polynomial time hierarchy (PH) in a natural way while DLPs reach one level beyond. In the latter case, however, the access to underlying NP oracle(s) is somewhat implicit and best understood via the so-called saturation technique from the original complexity result [6]. When using saturation, a programmer must essentially express oracles as Boolean satisfiability problems, which differs from NLPs with respect to both syntax and semantics. In spite of this mismatch, saturation has been successfully applied when expressing properties pertaining to the second level of PH [7,9], e.g., when using meta-programming techniques together with saturation.

The stable-unstable semantics [2] relieves the problem identified above by (i) enabling the use of (standard) NLPs when encoding oracles, (ii) making subprograms acting as oracles explicit, and (iii) changing the mode of reasoning from stability to instability for oracles.¹ If this idea is applied in a nested fashion by merging NLPs recursively as combined programs, any level of PH can be reached with NLPs only, in analogy to quantified Boolean formulas (QBFs). In a nutshell, according to the stable-unstable semantics, we seek a stable model M for the main NLP P such that the NLP Q acting as the oracle has no stable model N that agrees with M about the truth values of atoms shared by P and Q. In contrast with QBFs, this leaves the quantification of atoms implicit, i.e., the atoms of P are existentially quantified while the local atoms of Q are effectively universal. There are follow-up approaches [1,8] that make the quantification of atoms explicit, but the semantics of quantified programs is still aligned with the stable-unstable semantics, see [1, Theorem 7] and [8, Appendix B] for details. For the purposes of this work, however, implicit quantification is very natural, since the quantification of atoms can be controlled in terms of #show-statements directly supported by the grounder of the Clingo system.

Currently, no native implementations of stable-unstable semantics have emerged except via translations toward QBFs [2,8]. The goal of this work is to alleviate this situation with a translation of (effectively) normal programs that combines a main program P with any fixed number of oracle programs $P_1\,,\ldots,\,P_n$ subject to stable-unstable semantics. This is a slight generalization of the (original) stable-unstable semantics facilitating the incorporation of several oracles although, in principle, they could be merged into a single oracle first. The resulting DLP can be fed as input for answer set solvers supporting proper disjunctive rules. Thus we are mainly concentrating on search problems that reside on the second level of polynomial hierarchy and use Clingo as the intended back-end ASP solver.

One central goal of our approach is to hide saturation from the programmer altogether, even though it is exploited in one translation step internally. This is because saturation encodings are error-prone when using non-ground positive rules with first-order variables of the form

$$\mathtt{u}\mid\mathtt{p}_1(\vec{X}_1)\,\mid\ldots\mid\,\mathtt{p}_k(\vec{X}_k) ~\leftarrow ~\mathtt{p}_{k+1}(\vec{X}_{k+1})\,,\ldots,\,\mathtt{p}_{k+m}(\vec{X}_{k+m}), ~\mathtt{d}_1(\vec{Y}_1)\,,\ldots,\,\mathtt{d}_n(\vec{Y}_n).$$

where the special atom $\mathtt{u}$ stands for unsatisfiability, $\mathtt{p}_i$:s are application predicates subject to saturation, and $\mathtt{d}_j$:s are domain predicates. The argument lists $\vec{X}_i$:s and $\vec{Y}_j$:s consist of first-order terms and the domain predicates in the rule body restrict the possible values of variables occurring in the rule. Modern grounders infer part of this information from the occurrences of predicates elsewhere in a program. Now, the saturating rules $\mathtt{p}_i(\vec{t})\leftarrow\mathtt{u}$ should be generated for every ground (non-input) atom $\mathtt{p}_i(\vec{t})$ appearing in the ground rules of the oracle. This requires an understanding of which ground rules are actually produced for the oracle. Thus, it may become difficult to find non-ground counterparts for the saturating rules for individual predicates $\mathtt{p}_i(\vec{X})$ and the number of such rules may also get high. In any case, it is an extra burden for the programmer to keep these rules in synchrony with the rules encoding the oracle.

Our implementation of stable-unstable semantics deploys translators and linkers available under the ASPTOOLS² collection: the main program and oracles are treated as program modules [18] that can be grounded and processed in separation and finally linked together for solving. Since the grounder of the Clingo system is used to instantiate rules, we may relax most restrictions on the main program and thus utilize extended rule types, proper disjunctive rules, and optimization as needed. As regards oracles, the translation-based approach of [14] sets the limits for their support. Due to existing normalization tools [3,4], aggregates can be used. However, the use of disjunction in rule heads is restricted, i.e., only head-cycle-free disjunctions can be tolerated, as they can be translated away using a dedicated translator for shifting disjunctive rules. Finally, optimization does not make sense in the case of oracles.

Besides giving an overall introduction to stable-unstable semantics [2], modularity in ASP [18], the translation of NLPs into propositional clauses [13], and saturation [6], the main contributions of [15] are:

• The translation of a set of clauses $S$ into a positive disjunctive program $\mathrm{Tr}_{\text{UNSAT}}(S)$ possessing a stable model iff $S$ is unsatisfiable where any subset of atoms can be distinguished as input atoms.

• The implementation of $\mathrm{Tr}_{\text{UNSAT}}$ as a saturating translator unsat2lp distributed under ASPTOOLS.

• Given a main module $\Pi$ and oracle modules $\Pi_1\,,\ldots,\,\Pi_n$, the overall translation-based method for computing the respective set of stable-unstable models
  $$\mathrm{SM}(\mathrm{Tr}_{\text{ST-UNST}}(\Pi,\Pi_1\,,\ldots,\,\Pi_n))= \mathrm{SM}(\Pi)\Join(\bowtie_{i=1}^{n}\mathrm{SM}(\mathrm{Tr}_{\text{UNSAT}}(\mathrm{Tr}_{\text{SAT}}(\Pi_i))))$$
  where the stable models of $\Pi$ get accepted by the joins only if each oracle $\Pi_i$ has no stable models as detected by the translation $\mathrm{Tr}_{\text{UNSAT}}(\mathrm{Tr}_{\text{SAT}}(\Pi_i))$ of $\Pi_i$ into clauses and subsequently into a DLP.

• The illustration of practical modeling with stable-unstable semantics in terms of the point of no return problem involving a non-trivial oracle which is challenging to encode in ASP directly.

As regards future work, it it is possible to plug in alternative translations from NLPs to SAT, e.g., for improving performance. Moreover, there is still the quest for native implementations of stable-unstable semantics. Such implementations are expected to mimic the design of GnT [17] with interacting solvers, but use conflict-driven nogood learning (CDNL) [10] instead of traditional branch-and-bound search. Moreover, if solvers are integrated with each other recursively, following the original idea of combined programs from [2], the levels beyond the second one of PH can also be covered.

Acknowledgments

This research is supported by Academy of Finland (grants #327352 and #335718).

References

1. Giovanni Amendola, Francesco Ricca & Miroslaw Truszczynski (2019): Beyond NP: Quantifying over Answer Sets. 19(5-6), pp. 705–721, doi:10.1017/S1471068419000140.

2. Bart Bogaerts, Tomi Janhunen & Shahab Tasharrofi (2016): Stable-unstable semantics: Beyond NP with normal logic programs. 16(5-6), pp. 570–586, doi:10.1017/S1471068416000387.

3. Jori Bomanson, Martin Gebser & Tomi Janhunen (2014): Improving the Normalization of Weight Rules in Answer Set Programs. In: Proceedings of JELIA 2014, pp. 166–180, doi:10.1007/978-3-319-11558-0_12.

4. Jori Bomanson, Tomi Janhunen & Ilkka Niemelä (2020): Applying Visible Strong Equivalence in Answer-Set Program Transformations. 21(4), pp. 33:1–33:41, doi:10.1145/3412854.

5. Gerhard Brewka, Thomas Eiter & Miroslaw Truszczynski (2011): Answer set programming at a glance. 54(12), pp. 92–103, doi:10.1145/2043174.2043195.

6. Thomas Eiter & Georg Gottlob (1995): On the Computational Cost of Disjunctive Logic Programming: Propositional Case. 15(3–4), pp. 289–323, doi:10.1007/BF01536399.

7. Thomas Eiter & Axel Polleres (2006): Towards automated integration of guess and check programs in answer set programming: a meta-interpreter and applications. 6(1-2), pp. 23–60, doi:10.1017/S1471068405002577.

8. Jorge Fandinno, François Laferrière, Javier Romero, Torsten Schaub & Tran Cao Son (2021): Planning with Incomplete Information in Quantified Answer Set Programming. 21(5), pp. 663–679, doi:10.1017/S1471068421000259.

9. Martin Gebser, Roland Kaminski & Torsten Schaub (2011): Complex optimization in answer set programming. 11(4-5), pp. 821–839, doi:10.1017/S1471068411000329.

10. Martin Gebser, Benjamin Kaufmann & Torsten Schaub (2012): Conflict-driven answer set solving: From theory to practice. 187, pp. 52–89, doi:10.1016/j.artint.2012.04.001.

11. Michael Gelfond & Vladimir Lifschitz (1988): The Stable Model Semantics for Logic Programming. In: Proceedings of ICLP, MIT Press, pp. 1070–1080.

12. Michael Gelfond & Vladimir Lifschitz (1991): Classical Negation in Logic Programs and Disjunctive Databases. 9(3/4), pp. 365–386, doi:10.1007/BF03037169.

13. Tomi Janhunen (2006): Some (in)translatability results for normal logic programs and propositional theories. 16(1-2), pp. 35–86, doi:10.3166/jancl.16.35-86.

14. Tomi Janhunen (2018): Cross-Translating Answer Set Programs Using the ASPTOOLS Collection. 32(2-3), pp. 183–184, doi:10.1007/s13218-018-0529-9.

15. Tomi Janhunen (2022): Implementing Stable-Unstable Semantics with ASPTOOLS and Clingo. In: Proceedings of PADL, Springer, pp. 135–153, doi:10.1007/978-3-030-94479-7_9.

16. Tomi Janhunen & Ilkka Niemelä (2016): The Answer Set Programming Paradigm. 37(3), pp. 13–24, doi:10.1609/aimag.v37i3.2671.

17. Tomi Janhunen, Ilkka Niemelä, Dietmar Seipel, Patrik Simons & Jia-Huai You (2006): Unfolding partiality and disjunctions in stable model semantics. 7(1), pp. 1–37, doi:10.1145/1119439.1119440.

18. Tomi Janhunen, Emilia Oikarinen, Hans Tompits & Stefan Woltran (2009): Modularity Aspects of Disjunctive Stable Models. 35, pp. 813–857, doi:10.1613/jair.2810.

19. Viktor Marek & Mirek Truszczyński (1991): Autoepistemic Logic. 38(3), pp. 588–619, doi:10.1145/116825.116836.

Rushing and Strolling among Answer Sets - Navigation Made Easy (Extended Abstract)

1 Introduction

Background. We follow standard definitions of propositional answer set programs and assume familiarity with disjunctive logic programs and stable model semantics [8, 9]. A disjunctive logic program $\Pi$ is a finite set of rules of the form $\alpha_0\,|\, \ldots \,|\, \alpha_k \leftarrow \alpha_{k+1}, \dots, \alpha_m, \sim \alpha_{m+1}, \dots, \sim \alpha_n$ over atoms $\alpha_i$ with $0 \leq k \leq m \leq n$. We denote answer sets of a program $\Pi$ by $\mathit{AS}(\Pi)$. Further, we denote brave consequences by $\mathit{BC}(\Pi) := \bigcup \mathit{AS}(\Pi)$ and cautious consequences by $\mathit{CC}(\Pi) := \bigcap \mathit{AS}(\Pi)$. We denote the facets of $\Pi$ by $F(\Pi) := F^+(\Pi) \cup F^-(\Pi)$ where $F^+(\Pi) := \mathit{BC}(\Pi) \setminus \mathit{CC}(\Pi)$ denotes inclusive facets and $F^-(\Pi) := \{\overline{\alpha} \mid \alpha \in F^+(\Pi)\}$ denotes exclusive facets of $\Pi$. For further details on faceted answer set navigation, we refer to [1].

2 Weighted Faceted Navigation

Example 1 Consider $\Pi_1 = \{a\,|\,b; c\,|\,d; d \leftarrow b; e\}$. We have $\mathit{AS}(\Pi_1) = \{\{a, e\}, \{b, c, e\}, \{b, d, e\}\}$ and $F(\Pi_1) = \{a, \overline{a}, b, \overline{b}, c, \overline{c}, d, \overline{d}\}$. As illustrated by Figure $1$, facets $b$ and $\overline{c}$ have the same absolute weight of $1$, that is, we zoom-in by one solution, but their facet-counting weights differ. While $b$ hast facet-counting weight $4$, the facet counting weight of $\overline{c}$ is $2$. The reason is that counting facets indicates to what amount solutions converge, that is, since the solutions in $\mathit{AS}(\Pi_1^{\langle b \rangle}) = \{\{b, c, e\}, \{b, d, e\}\}$ with facets $\{c, \overline{c}, d, \overline{d}\}$ are more similar to each other than the solutions in sub-space $\mathit{AS}(\Pi_1^{\langle \overline{c} \rangle}) = \{\{a, e\}, \{b, d, e\}\}$ with facets $\{a, \overline{a}, b, \overline{b}, d, \overline{d}\}$, inclusive facet $b$ has a higher facet-counting weight than exclusive facet $\overline{c}$.

Figure 1: Navigating on several routes through answer sets of program $\Pi_1$. Dashed lines indicate redirections where red colored facets were retracted.

Figure 2: Making sense of moves in the famous $8$-queens problem. White queens represent moves with the respective maximal weight, and black
queens represent moves with the respective minimal weight among possible moves (inclusive facets).

Experiments. To study the feasibility of our framework, we implemented fasb [5], an interactive prototype of our framework on top of the clingo solver[7, 6]. We conducted experiments [4] in order to (i) demonstrate the feasibility of our approach by navigating through the solution space of a PC configuration encoding with more than a billion solutions; and (ii) demonstrate that the feasibility of our approach depends on the complexity of the given program, by analyzing runtimes of navigation over two encodings of different complexity but with an identical solution space.

3 Conclusion

References

1. Christian Alrabbaa, Sebastian Rudolph & Lukas Schweizer (2018): Faceted Answer-Set Navigation. In Christoph Benzmüller, Francesco Ricca, Xavier Parent & Dumitru Roman, editors: Proc. of the 2nd Int. Joint Conf. on Rules and Reasoning (RuleML+RR'18), Springer, pp. 211-225. doi:10.1007/978-3-319-99906-7_14.
2. Gerhard Brewka, Thomas Eiter & Miroslaw Truszczyński (2011): Answer set programming at a glance. Communications of the ACM 54(12), pp. 92-103. doi:10.1145/2043174.2043195.
3. Johannes K Fichte, Markus Hecher, Michael Morak & Stefan Woltran (2017): Answer set solving with bounded treewidth revisited. In Marcello Balduccini & Tomi Janhunen, editors: Proc. of the 14th Int. Conf. on Logic Programming and Nonmonotonic Reasoning (LPMNR 2017), LNCS 10377, Springer, pp. 132-145. doi:10.1007/978-3-319-61660-5_13.
4. Johannes Klaus Fichte, Sarah Alice Gaggl & Dominik Rusovac (2021): Rushing and Strolling among Answer Sets - Navigation Made Easy (Experiments). doi:10.5281/zenodo.5780050.
5. Johannes Klaus Fichte, Sarah Alice Gaggl & Dominik Rusovac (2021): Rushing and Strolling among Answer Sets - Navigation Made Easy (Faceted Answer Set Browser fasb). doi:10.5281/zenodo.5767981.
6. Martin Gebser, Roland Kaminski, Benjamin Kaufmann & Torsten Schaub (2014): Clingo = ASP + Control: Preliminary Report. CoRR abs/1405.3694. doi:10.48550/arXiv.1405.3694.
7. Martin Gebser, Roland Kaminski, Arne König & Torsten Schaub (2011): Advances in gringo series 3.. In James P. Delgrande & Wolfgang Faber, editors: Proc. of the Int. Conf. on Logic Programming and Nonmonotonic Reasoning (LPMNR'11), Springer, pp. 345-351. doi:10.1007/978-3-642-20895-9_39.
8. Michael Gelfond & Vladimir Lifschitz (1988): The Stable Model Semantics For Logic Programming. In Robert A. Kowalski & Kenneth A. Bowen, edtiors: Proc. of the 5th Int. Conf. and Symposium on Logic Programming (ICLP/SLP'88), 2, MIT Press, pp. 1070-1080.
9. Michael Gelfond & Vladimir Lifschitz (1991): Classical Negation in Logic Programs and Disjunctive Databases. New Generation Comput. 9(3/4), pp. 1070-1080. doi:10.1007/BF03037169.

Tractable Reasoning using Logic Programs with Intensional Concepts (Report)

In this extended abstract, we summarize the contributions made in ([11]). In that paper, we develop a solution that allows tractable reasoning with intensional concepts, such as time, space and obligations, providing defeasible/non-monotonic inferences in the presence of large quantities of data.

Initiatives such as the Semantic Web, Linked Open Data, and the Web of Things, as well as modern Geographic Information Systems, resulted in the wide and increasing availability of machine-processable data and knowledge in the form of data streams and knowledge bases. To truly take advantage of this kind of knowledge, it is paramount to be able to reason in the presence of intensional or modal concepts, which has resulted in an increased interest in formalisms, often based on rules with defeasible inferences, that allow for reasoning with time ([1,9,4,2,6,17]), space ([5,18,12,16]), and possibility or obligations ([15,8,10,3]). Examples of such concepts may be found in applications with data referring for example to time (e.g., operators such as "next", "at time", "during interval T") or space (e.g., "at place P", "within a given radius", "connected to"), but also legal reasoning (e.g., "is obliged to", "is permitted").

Example 1. In a COVID-19-inspired setting, we consider an app for contact-tracing. It tracks where people move and stores their networks of persons, i.e., their colleagues and family whom they meet regularly. Once a person tests positive, the app informs anyone at risk (e.g. someone who was in the proximity of an infected person for a longer amount of time or because someone in their network is at risk) that they have to stay in quarantine for 10 days. If a negative test result can be given, this quarantine is not obligatory anymore. It is important that the app can explain to persons being ordered in quarantine the reason for their being at risk (e.g. since they were in contact with an infected person for a longer amount of time) while preserving anonymity to abide with laws of data protection (e.g. someone being ordered into quarantine should not be able to see who is the reason for this).

In this context, efficient reasoning with non-monotonic rules over intensional concepts is indeed mandatory, since a) rules allow us to encode monitoring and intervention guidelines and policies in a user-friendly and declarative manner; b) conclusions may have to be revised in the presence of newly arriving information; c) different intensional concepts need to be incorporated in the reasoning process; d) timely decisions are required, even in the presence of large amounts of data, as in streams; e) intensional concepts can preserve anonymity, e.g. in user-friendly explanations without having to change the rules. However, relevant existing work usually deals with only one kind of intensional concepts (as detailed before), and, in general, the computational complexity of the proposed formalisms is too high, usually due to both the adopted underlying formalism and the unrestricted reasoning with expressive intensional concepts.

In this paper, we introduce a formalism that allows us to seamlessly represent and reason with defeasible knowledge over different intensional concepts. We build on so-called intensional logic programs ([13]), extended with non-monotonic default negation, and equip them with a novel three-valued semantics with favorable properties. In more detail, intensional logic programs consist of rules of the form $A\leftarrow A_1,\ldots,A_n,\sim B_1,\ldots,\sim B_m$ where $A,A_1,\ldots,A_n,B_1,\ldots,B_m$ are intensional atoms, i.e. atoms $p$ possibly preceded by a modal operator $\nabla$. The two-valued semantics for such programs are given in terms of valuations mapping formulas to sets of possible worlds, generalizing Kripke frames, and intuitively representing the worlds in which a formula is true. Neighborhood functions ([pacuit2017neighborhood]) mapping worlds $w$ to sets of sets of worlds assign meaning to modal operators $\nabla$ by specifying in which worlds an atom $p$ has to be true such that the modal version of that atom $\nabla p$ is true at a given world $w$. Three-valued semantics are defined similarly, now defining valuations as mappings of formulas to pairs of sets of worlds, which represent the worlds in which an (intensional) atom is true, respectively not false. Satisfaction of rules in worlds, reducts as well as stable semantics are generalized to our setting.

We then define the well-founded model as the least precise stable model, in the line of the well-founded semantics for logic programs ([7]). Provided the adopted intensional operators satisfy certain properties, which turn out to be aligned with practical applications such as the one outlined in Ex. 1, the well-founded model is unique, minimal among the three-valued models, in the sense of only providing derivable consequences, and, crucially, its computation is tractable. Our approach allows us to add to relevant related work in the sense of providing a well-founded semantics to formalisms that did not have one so far, which we illustrate on a relevant fragment of LARS programs ([2]).

Acknowledgments The authors acknowledge partial support by FCT project RIVER (PTDC/CCI-COM/30952/2017) and by FCT project NOVA LINCS (UIDB/04516/2020). J. Heyninck was also supported by the German National Science Foundation under the DFG-project CAR (Conditional Argumentative Reasoning) KE-1413/11-1.

References

1. Darko Anicic, Sebastian Rudolph, Paul Fodor & Nenad Stojanovic (2012): Stream reasoning and complex event processing in ETALIS. Semantic Web 3(4), pp. 397–407, doi:10.3233/SW-2011-0053.
2. Harald Beck, Minh Dao-Tran & Thomas Eiter (2018): LARS: A Logic-based framework for Analytic Reasoning over Streams. Artif. Intell. 261, pp. 16–70, doi:10.1016/j.artint.2018.04.003.
3. Mathieu Beirlaen, Jesse Heyninck & Christian Straßer (2019): Structured argumentation with prioritized conditional obligations and permissions. Journal of Logic and Computation 29(2), pp. 187–214, doi:10.1093/logcom/exy005.
4. Sebastian Brandt, Elem Güzel Kalayci, Vladislav Ryzhikov, Guohui Xiao & Michael Zakharyaschev (2018): Querying Log Data with Metric Temporal Logic. J. Artif. Intell. Res. 62, pp. 829–877, doi:10.1613/jair.1.11229.
5. Christopher Brenton, Wolfgang Faber & Sotiris Batsakis (2016): Answer Set Programming for Qualitative Spatio-Temporal Reasoning: Methods and Experiments. In: Technical Communications of ICLP, OASICS 52. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, pp. 4:1–4:15, doi:10.4230/OASIcs.ICLP.2016.4.
6. Gerhard Brewka, Stefan Ellmauthaler, Ricardo Gonçalves, Matthias Knorr, João Leite & Jörg Pührer (2018): Reactive multi-context systems: Heterogeneous reasoning in dynamic environments. Artif. Intell. 256, pp. 68–104, doi:10.1016/j.artint.2017.11.007.
7. Allen Van Gelder, Kenneth A. Ross & John S. Schlipf (1991): The Well-Founded Semantics for General Logic Programs. J. ACM 38(3), pp. 620–650, doi:10.1145/116825.116838.
8. Ricardo Gonçalves & José Júlio Alferes (2012): Specifying and reasoning about normative systems in deontic logic programming. In: Procs. of AAMAS. IFAAMAS, pp. 1423–1424. Available at https://dl.acm.org/doi/abs/10.5555/2343896.2344039.
9. Ricardo Gonçalves, Matthias Knorr & João Leite (2014): Evolving Multi-Context Systems. In: ECAI, Frontiers in Artificial Intelligence and Applications 263. IOS Press, pp. 375–380, doi:10.3233/978-1-61499-419-0-375.
10. Guido Governatori, Antonino Rotolo & Régis Riveret (2018): A Deontic Argumentation Framework Based on Deontic Defeasible Logic. In: International Conference on Principles and Practice of Multi-Agent Systems. Springer, pp. 484–492, doi:10.1007/978-3-030-03098-8_33.
11. Jesse Heyninck, Ricardo Gonçalves, Matthias Knorr & João Leite (2021): Tractable Reasoning Using Logic Programs with Intensional Concepts. In: European Conference on Logics in Artificial Intelligence. Springer, pp. 329–345, doi:10.1007/978-3-030-75775-5_22.
12. Yusuf Izmirlioglu & Esra Erdem (2018): Qualitative Reasoning About Cardinal Directions Using Answer Set Programming. In: Procs. of AAAI. AAAI Press, pp. 1880–1887. Available at https://ojs.aaai.org/index.php/AAAI/article/view/11568.
13. Mehmet A Orgun & William W Wadge (1992): Towards a unified theory of intensional logic programming. The Journal of Logic Programming 13(4), pp. 413–440, doi:10.1016/0743-1066(92)90055-8.
14. Eric Pacuit (2017): Neighborhood semantics for modal logic. Springer, doi:10.1007/978-3-319-67149-9.
15. Sofia Panagiotidi, Juan Carlos Nieves & Javier Vázquez-Salceda (2009): A Framework to Model Norm Dynamics in Answer Set Programming.. In: MALLOW, CEUR Workshop Proceedings 494. CEUR-WS.org. Available at http://ceur-ws.org/Vol-494/famaspaper8.pdf.
16. Jakob Suchan, Mehul Bhatt, Przemyslaw Andrzej Walega & Carl P. L. Schultz (2018): Visual Explanation by High-Level Abduction: On Answer-Set Programming Driven Reasoning About Moving Objects. In: Procs. of AAAI. AAAI Press, pp. 1965–1972. Available at https://dl.acm.org/doi/abs/10.5555/3504035.3504274.
17. Przemyslaw Andrzej Walega, Mark Kaminski & Bernardo Cuenca Grau (2019): Reasoning over Streaming Data in Metric Temporal Datalog. In: Procs. of AAAI. AAAI Press, pp. 3092–3099, doi:10.1609/aaai.v33i01.33013092.
18. Przemyslaw Andrzej Walega, Carl P. L. Schultz & Mehul Bhatt (2017): Non-monotonic spatial reasoning with answer set programming modulo theories. TPLP 17(2), pp. 205–225, doi:10.1017/S1471068416000193.

On Paraconsistent Belief Revision: the Case of Priest's Logic of Paradox

Belief revision aims at incorporating a new piece of information into the beliefs of an agent. This process can be modelled by the standard Katsuno and Mendelzon's (KM) rationality postulates. However, these postulates suppose a classical setting and do not govern the case where (some parts of) the beliefs of the agent are not consistent. In this work we discuss how to adapt these postulates when the underlying logic is Priest's Logic of Paradox, in order to model a rational change, while being a conservative extension of KM belief revision. This paper is a summary of [5].

Introduction

Belief revision accommodates into an agent's beliefs ϕ a new, reliable, piece of evidence μ, where both ϕ and μ are represented as propositional formulae. A revision operator is expected to satisfy a set of properties called KM postulates (denoted by (R1-R6)) [1, 3]. These postulates translate the three core principles of belief change: primacy of update, consistency, and minimality of change. Every revision operator can be constructed by associating each ϕ with a (plausibility) total preorder ≤_ϕ over worlds: when revising ϕ by μ, one takes as a result the models of μ that are minimal in ≤_ϕ.

An issue with the KM framework is that it does not govern the case of inconsistent inputs, whether it be the agent's beliefs ϕ or the new information μ. So a solution is to use a paraconsistent logic, define the revision to be the conjunction, that allows one to derive sensible conclusions. But this is not a belief change operation. As an example, consider that the current beliefs of the agents are p ∧ ¬p ∧ q and that the new piece of information is ¬q. In this case, it is arguable to consider that the variables p and q are independent, and that the expected result could be p ∧ ¬ p ∧ ¬q, i.e., one may want to keep holding the conflict on p, while changing the beliefs on the truth value of q. Simply speaking, we want to do more than just conjunction.

For this purpose, we rephrase the KM postulates in a particular paraconsistent setting: Priest's Logic of Paradox [4] (LP for short), a three-valued logic, with the third value meaning 'inconsistent' ('both true and false'), that allows to isolate inconsistencies in the concerned propositional variables. In LP, a world (which we call LP world), is a three-valued interpretation. An LP world is an LP model of a formula α if it makes α 'true' or 'both'. The LP entailment relation is defined in terms of inclusion between sets of LP models, i.e., α ⊨_LP β iff ⟦α⟧ ⊆ ⟦β⟧, where ⟦α⟧ denotes the set of LP models of α. And α ≡_LP β denotes the case where ⟦α⟧ = ⟦β⟧.

We discuss how to adapt the KM postulates in order to model a rational change, while being a conservative extension of KM belief revision. This requires in particular to adequately adapt the definition of belief expansion, since its direct translation is not adequate for non-classical settings. We provide a representation theorem for this class of revision operators in terms of plausibility preorders on LP worlds (faithful assignments). And we define a whole family of distance based operators that generalize Dalal revision in this setting.

Proposal

Representative LP models

First, it is useful to see that all LP worlds can be partially ordered, i.e., ω ≤_LP ω' if whenever ω' associates a variable with a classical value 'true' of 'false', ω associates that variable with the same classical value. Thus ω ≤_LP ω' could be read as ω' is 'less classical' than ω. In particular, the LP worlds that are minimal with respect to ≤_LP form the set of all classical worlds. A crucial observation is that if an LP world ω is an LP model of a formula α, then all LP worlds ω' such that ω ≤_LP ω' are also LP models of α. This means that the only 'meaningful' LP models of a formula α are the set of its minimal elements w.r.t. ≤_LP, denoted by ⟦α⟧_*. We call the set ⟦α⟧_* the representative set of LP models of α, and we can show that ⟦α⟧ = ⟦β⟧ if and only if ⟦α⟧_* = ⟦β⟧_*.

Belief Expansion in LP

The notion of representative set allows one to formalize the notion of expansion in the LP setting, an operation on which belief revision relies. The expansion of ϕ by μ, denoted by ϕ + μ, simply consists in 'adding' μ into ϕ. In particular, ϕ + μ is a formula that does not question what could be already derived from ϕ, and in particular it may be an inconsistent formula (in the classical sense). In the classical case, expansion corresponds to the conjunction ϕ ∧ μ. But while in the classical case, all classical worlds have the same status, this is not the case in LP: as we have seen before, some LP worlds are more 'important' than others to characterize the LP models of a formula. So in LP, we rather focus on the representative set of LP models of ϕ to perform the selection: we define the LP-expansion ϕ +_LP μ as a formula whose representative set is characterized by ⟦ϕ +_LP μ⟧_* = ⟦ϕ⟧_* ∩ ⟦μ⟧. That is, one selects the representative LP models of ϕ that are LP models of μ. When this set is non-empty, we say that the expansion is conclusive. Interestingly, in the same way conjunction is the only operator satisfying the Gärdenfors expansion postulates in the classical setting [2], we show that +_LP as defined above is the only operator that satisfies (an adaptation of) the expansion postulates to the LP setting.

Based on our LP-expansion operator, we propose the following set of postulates for LP revision:

• (LP1) ϕ ○ μ ⊨_LP μ
• (LP2) If ϕ +_LP μ is conclusive, then ϕ ○ μ ≡_LP ϕ +_LP μ
• (LP4) If ϕ ≡_LP ϕ' and μ ≡_LP μ', then ϕ ○ μ ≡_LP ϕ' ○ μ'
• (LP5) (ϕ ○ μ) +_LP μ' ⊨_LP ϕ ○ (μ ∧ μ')
• (LP6) If (ϕ ○ μ) +_LP μ' is conclusive, then ϕ ○ (μ ∧ μ') ⊨_LP (ϕ ○ μ) +_LP μ'

These postulates are similar to the original KM ones, except that we use the LP entailment in place of the classical entailment, and we use the LP-expansion instead of the classical expansion (i.e., instead of the conjunction). Thus, each postulate (LPi) above is a direct translation of the original KM postulate (Ri). Noteworthy, (LP3) does not appear in the list. Indeed, the KM postulate (R3) says that the revised result ϕ ○ μ should be consistent whenever the new information μ is consistent. When interpreting the notion of consistency in terms of non-emptiness of set of models, a direct adaptation of this postulate to LP would not make sense anymore: since every formula has a non-empty set of (representative) LP models, it is trivially satisfied. However, we discuss some possible adaptation of (R3), and show that the set of all postulates (including the adaptation of (R3)) can be viewed as a conservative extension of the KM postulates in LP (see [5] for details).

Representation Result

Similarly to the classical case, every LP revision operator can be characterized in terms of an LP faithful assignment, i.e., by associating each ϕ with a total preorder over LP worlds ≤_ϕ. This time, the first level of each total preorder ≤_ϕ corresponds to the representative set of LP models of ϕ. To revise ϕ by a formula μ, one takes as a result a formula ϕ ○ μ whose LP models are the LP-closure of the LP models of μ that are minimal in ≤_ϕ, where the LP-closure of a set of LP worlds S, denoted by Cl(S), is defined by Cl(S) = {ω | ∃ ω' ∈ S, ω' ≤_ϕ ω} (accordingly for every set of LP worlds S, there is always a formula α such that ⟦α⟧ = Cl(S)).

Theorem 1 An operator ○ is an LP revision operator (i.e., it satisfies (LP1-LP6)) if and only if there is an LP faithful assignment associating every formula ϕ with a total preorder over LP worlds ≤_ϕ such that for all formulae ϕ, μ, ⟦ϕ ○ μ⟧ = Cl(min(⟦μ⟧, ≤_ϕ)).

Distance-Based LP Revision

Lastly, we introduce a class of LP revision operators that are based on a distance between LP worlds. In the classical case, an interesting example of distance is the Hamming distance between worlds, which defines the well-known Dalal revision operator. We propose to extend that distance to the LP case. In the classical case, Hamming distance consists in counting the number of differences, of 'changes', between two classical worlds. But in the three-valued LP setting, we have three values, and the 'change' between 'true' and 'both' may not be the same as the change between 'true' and 'false'. So to be as general as possible, we consider a distance which counts the number of changes between two LP worlds, where this change is given by a distance d_b between two truth values: d(ω, ω') = ∑_xi d_b(ω(x_i), ω'(x_i)). For instance, the choice of a value for d_b(true, both) represents, for the underlying agent, the cost of change from the value 'true' to 'both' for any variable. We show that under very natural conditions on d_b, the only value that matters in the definition of such a distance-based operator is the cost of change C from a classical truth value ('true' or 'false') to the value 'both'. This means that overall, to define a distance-based operator, one has a one-dimensional choice space which corresponds to whether one wants to model a revision behavior that is reluctant to change (a high value for C), or inclined to change (a low value for C).

References

1. C. E. Alchourrón, P. Gärdenfors & D. Makinson (1985): On the logic of theory change: partial meet contraction and revision functions. Journal of Symbolic Logic 50, pp. 510-530, doi:10.2307/2274239.
2. P. Gärdenfors: Knowledge in Flux. MIT Press.
3. H. Katsuno & A. O. Mendelzon (1991): Propositional knowledge base revision and minimal change. Artificial Intelligence 52, pp. 263-294, doi:10.1016/0004-3702(91)90069-V.
4. G. Priest (1979): The logic of paradox. Journal of Philosophical Logic 8(1), pp. 219-241, doi:10.1007/BF00258428.
5. N. Schwind, S. Konieczny & R. Pino Pérez (2022): On paraconsistent belief revision in LP. In: Proceedings of the 36th AAAI Conference on Artificial Intelligence (AAAI'22), pp. 5879-5887, doi:10.1609/aaai.v36i5.20532.

On Syntactic Forgetting under Uniform Equivalence (Report)

Forgetting, also known as variable elimination, aims at reducing the language of a knowledge base while preserving all direct and indirect semantic relationships over the remaining language. In Answer Set Programming (ASP), forgetting has also been extensively studied, where its non-monotonic nature has created unique challenges resulting in a wide variety of different approaches ([4,7,8,10,13,17,19,20,21,22]). Among the many proposals of operators and desirable properties (cf. the surveys on forgetting in ASP ([11,5])), arguably, forgetting in ASP is best captured by strong persistence ([17]), a property which requires that the answer sets of a program and its forgetting result be in correspondence, even in the presence of additional rules over the remaining language. However, it is not always possible to forget and satisfy strong persistence ([12,14]).

Recently, forgetting has also gained interest in the context of modular ASP ([2,6,15,16,18]). In general, modular programming is fundamental to facilitate the creation and reuse of large programs, and modular ASP allows the creation of answer set programs equipped with well-defined input-output interfaces whose semantics is compositional on the individual modules. For modules with input-output interfaces, strong persistence can be relaxed to uniform persistence that only varies additional sets of facts (the inputs), and it has been shown that forgetting for modular ASP can always be applied and preserves all dependencies over the remaining language ([10]).

Uniform persistence is closely related to uniform equivalence, which in turn is closely connected to one of the central ideas of ASP: a problem is specified in terms of a uniform encoding, i.e., an abstract program combined with varying instances, represented by sets of facts, to obtain concrete solutions. Thus, arguably, uniform persistence seems the better alternative when considering forgetting in ASP in general, but its usage is hindered by the lack of practically usable forgetting operators: the definition of a result in ([10]) is based solely on an advanced semantic characterization in terms of HT-models, so computing an actual result is a complicated process and the result, though semantically correct w.r.t. uniform persistence, commonly bears no syntactic resemblance to the original program. What is missing is a syntactic operator that computes results of forgetting, ideally only by manipulating the rules of the original program that contain the atoms to be forgotten.

Concrete syntactic forgetting operators have been considered infrequently in the literature. Zhang and Foo ([22]) define two such operators in the form of strong and weak forgetting, but neither of them does even preserve the answer sets of the original program (modulo the forgotten atoms) ([8]). Eiter and Wang ([8]) present a syntactic operator for their semantic approach to forgetting, but it only preserves the answer sets themselves and does not satisfy uniform nor strong persistence. Knorr and Alferes ([17]) provide an operator that aims at aligning with strong persistence which is not possible in general. Thus, it is only defined for a non-standard class of programs, and cannot be iterated in general, as the operator is not closed for this non-standard class, nor does it satisfy uniform persistence. Berthold et al. ([4]) introduce an operator that satisfies strong persistence whenever possible, but it does not satisfy uniform persistence, nor is it closed for the non-standard class defined in ([17]). Finally, based on the idea of forks ([1]), a forgetting operator is provided ([3]) that introduces so-called anonymous cycles when forgetting in the sense of strong persistence is not possible. However, rather than reducing the language, this operator introduces new auxiliary atoms to remove existing ones, though only in a restricted way. Thus, no syntactic forgetting operator exists in the literature that satisfies uniform persistence.

Our contributions can be summarized as follows:

• We show that there is no forgetting operator that preserves uniform equivalence (modulo the forgotten atoms) between the given program and its forgetting result, by only manipulating the rules of the original program that contain the atoms to be forgotten.
• We argue that forgetting an atom for which there are rules of the form $p\leftarrow not~not~p$ is indeed not suitable in a syntactic manner, even for cases where such result could still be constructed based alone on the rules of the original program that contain the atoms to be forgotten.
• We present a forgetting operator that preserves uniform equivalence while forgetting, and is syntactic whenever this is possible. We show that this operator can indeed be iterated in the general case.
• In addition, we present a special case of our operator for stratified programs, without disjunction and loops over (double) negation, and show that syntactic forgetting is always possible while preserving uniform equivalence.
• We also show that, for stratified programs, this operator corresponds to an existing forgetting operator that aims at preserving all semantic dependencies whenever possible, and we establish this class of programs as the largest known class where forgetting while preserving all semantic dependencies is always possible.

Acknowledgments Authors R. Gonçalves, M. Knorr, and J. Leite were partially supported by FCT project FORGET (PTDC/CCI-INF/32219/2017) and by FCT project NOVA LINCS (UIDB/04516/2020). T. Janhunen was partially supported by the Academy of Finland projects ETAIROS (327352) and AI-ROT (335718).

This is a report of the original publication ([9]).

References

1. Felicidad Aguado, Pedro Cabalar, Jorge Fandinno, David Pearce, Gilberto Pérez & Concepción Vidal (2019): Forgetting auxiliary atoms in forks. Artif. Intell. 275, pp. 575–601, doi:10.1016/j.artint.2019.07.005.
2. Chitta Baral, Juraj Dzifcak & Hiro Takahashi (2006): Macros, Macro Calls and Use of Ensembles in Modular Answer Set Programming. In: Sandro Etalle & Miroslaw Truszczynski: Procs. of ICLP, LNCS 4079. Springer, pp. 376–390, doi:10.1007/11799573_28.
3. Matti Berthold, Ricardo Gonçalves, Matthias Knorr & João Leite (2019): Forgetting in Answer Set Programming with Anonymous Cycles. In: EPIA, LNCS 11805. Springer, pp. 552–565, doi:10.1007/978-3-030-30244-3_46.
4. Matti Berthold, Ricardo Gonçalves, Matthias Knorr & João Leite (2019): A Syntactic Operator for Forgetting that Satisfies Strong Persistence. Theory Pract. Log. Program. 19(5-6), pp. 1038–1055, doi:10.1017/S1471068419000346.
5. Ricardo Gonçalves, Matthias Knorr & João Leite (2021): Forgetting in Answer Set Programming A Survey. Theory and Practice of Logic Programming, pp. 1–43, doi:10.1017/S1471068421000570.
6. Minh Dao-Tran, Thomas Eiter, Michael Fink & Thomas Krennwallner (2009): Modular Nonmonotonic Logic Programming Revisited. In: Patricia M. Hill & David Scott Warren: Procs. of ICLP, LNCS 5649. Springer, pp. 145–159, doi:10.1007/978-3-642-02846-5_16.
7. James P. Delgrande & Kewen Wang (2015): A Syntax-Independent Approach to Forgetting in Disjunctive Logic Programs. In: Blai Bonet & Sven Koenig: Procs. of AAAI. AAAI Press, pp. 1482–1488. Available at https://dl.acm.org/doi/abs/10.5555/2886521.2886526.
8. Thomas Eiter & Kewen Wang (2008): Semantic forgetting in answer set programming. Artif. Intell. 172(14), pp. 1644–1672, doi:10.1016/j.artint.2008.05.002.
9. Ricardo Gonçalves, Tomi Janhunen, Matthias Knorr & João Leite (2021): On Syntactic Forgetting Under Uniform Equivalence. In: JELIA, LNCS 12678. Springer, pp. 297–312, doi:10.1007/978-3-030-75775-5_20.
10. Ricardo Gonçalves, Tomi Janhunen, Matthias Knorr, João Leite & Stefan Woltran (2019): Forgetting in Modular Answer Set Programming. In: AAAI. AAAI Press, pp. 2843–2850, doi:10.1609/aaai.v33i01.33012843.
11. Ricardo Goncalves, Matthias Knorr & João Leite (2016): The Ultimate Guide to Forgetting in Answer Set Programming. In: Chitta Baral, James Delgrande & Frank Wolter: Procs. of KR. AAAI Press, pp. 135–144. Available at https://dl.acm.org/doi/abs/10.5555/3032027.3032044.
12. Ricardo Gonçalves, Matthias Knorr & João Leite (2016): You can't always forget what you want: on the limits of forgetting in answer set programming. In: Maria S. Fox & Gal A. Kaminka: Procs. of ECAI. IOS Press, pp. 957–965, doi:10.3233/978-1-61499-672-9-957.
13. Ricardo Gonçalves, Matthias Knorr, João Leite & Stefan Woltran (2017): When you must forget: Beyond strong persistence when forgetting in answer set programming. TPLP 17(5-6), pp. 837–854, doi:10.1017/S1471068417000382.
14. Ricardo Gonçalves, Matthias Knorr, João Leite & Stefan Woltran (2020): On the limits of forgetting in Answer Set Programming. Artif. Intell. 286, pp. 103307, doi:10.1016/j.artint.2020.103307.
15. Amelia Harrison & Yuliya Lierler (2016): First-order modular logic programs and their conservative extensions. TPLP 16(5-6), pp. 755–770, doi:10.1017/S1471068416000430.
16. Tomi Janhunen, Emilia Oikarinen, Hans Tompits & Stefan Woltran (2009): Modularity Aspects of Disjunctive Stable Models. J. Artif. Intell. Res. (JAIR) 35, pp. 813–857, doi:10.1613/jair.2810.
17. Matthias Knorr & José Júlio Alferes (2014): Preserving Strong Equivalence while Forgetting. In: Eduardo Fermé & João Leite: Procs. of JELIA, LNCS 8761. Springer, pp. 412–425, doi:10.1007/978-3-319-11558-0_29.
18. Emilia Oikarinen & Tomi Janhunen (2008): Achieving compositionality of the stable model semantics for smodels programs. TPLP 8(5-6), pp. 717–761, doi:10.1017/S147106840800358X.
19. Yisong Wang, Kewen Wang & Mingyi Zhang (2013): Forgetting for Answer Set Programs Revisited. In: Francesca Rossi: Procs. of IJCAI. IJCAI/AAAI, pp. 1162–1168. Available at https://dl.acm.org/doi/abs/10.5555/2540128.2540295.
20. Yisong Wang, Yan Zhang, Yi Zhou & Mingyi Zhang (2014): Knowledge Forgetting in Answer Set Programming. J. Artif. Intell. Res. (JAIR) 50, pp. 31–70, doi:10.1613/jair.4297.
21. Ka-Shu Wong (2009): Forgetting in Logic Programs. The University of New South Wales.
22. Yan Zhang & Norman Y. Foo (2006): Solving logic program conflict through strong and weak forgettings. Artif. Intell. 170(8-9), pp. 739–778, doi:10.1016/j.artint.2006.02.002.

Graph-based Interpretation of Normal Logic Programs

1 Introduction

Recently, we have devised a novel graph-based approach to compute answer sets of a normal logic program [4]. Our goal in this paper is to show that this approach can also be used for computing models under other semantics, in particular, the well-founded semantics and the co-stable model semantics (costable model semantics is similar to the stable model semantics, except that the greatest fixpoint is computed in the second step of the GL-transform). Our graph-based approach can be used for computing interesting properties of normal logic programs, for example, in providing justification for inclusion of an atom in a model.

At present, to compute the semantics of a normal logic program under different semantics, we have to encode the program in different formats and use different systems to compute the different model(s). For finding justification, one may have to use yet another system. Lack of a single system that can achieve all the aforementioned tasks is the main motivation of our research. Graph-based approaches have other additional benefits, such as partial models can be computed which are needed in some applications [3]. Elsewhere [1] the authors introduced a dependency graph-based approach to represent ASP programs and compute their models. The basic idea is to use dependency graph to represent rules and goals of an answer set program, and find models by reasoning over the graph. This graph-based representation is the basis for our work in this paper in interpreting a normal logic program under different semantics.

2 Graph-based Normal Logic Program Interpretations

Our novel graph-based method for computing the various semantics of a normal logic program uses conjunction nodes introduced in [4] to represent the dependency graph of the program. The dependency graph can be transformed in a semantics preserving manner and re-translated into an equivalent normal logic program. This transformed normal logic program can be augmented with a small number of rules written in ASP, and then a traditional SAT solver-based system used to compute its answer sets. Depending on how these additional rules are coded in ASP, one can compute models of the original normal logic program under the stable model semantics, the co-stable model semantics as well as the well-founded semantics.

Note that information regarding dependence between various literals in the program is made explicit in the graph representation (effective edge). This information is maintained in the ASP program that results from the transformation and can be made explicit in the answer sets of this transformed program. This explicit information on dependence can then be used to provide justification automatically. This graph-based transformation approach can be quite useful for the analysis of normal logic programs. In general, some interesting property of the program can be computed and the dependency graph annotated. The annotated graph can then be transformed into an answer set program with the annotation intact. Models of the transformed program can then be computed using traditional solvers. The annotations in the model can then be used for computing the program property of interest. Finding causal justification of literals in the model is but one example of this general technique.

2.1 The Co-stable Model Semantics Interpreter

We introduce the co-stable model semantics interpreter first, because it is the basis of the other two interpreters. The following ASP rules interpret the co-stable model semantics:

2.2 The Stable Model Semantics Interpreter

The following ASP rules compute the stable model semantics:

2.3 The Well-founded Semantics Interpretation

The following ASP rules compute the well-founded semantics:

We are unable to include more details including performance evaluation and proof of correctness of these interpreters due to lack of space, however, they can be found elsewhere [2].

References

[1] Fang Li (2021): Graph Based Answer Set Programming Solver Systems. In Andrea Formisano, Yanhong Annie Liu, Bart Bogaerts, Alex Brik, Veronica Dahl, Carmine Dodaro, Paul Fodor, Gian Luca Pozzato, Joost Vennekens & Neng-Fa Zhou, editors: Proceedings 37th International Conference on Logic Programming (Technical Communications), ICLP Technical Communications 2021, Porto (virtual event), 20-27th September 2021, EPTCS 345, pp. 276-285, doi:10.4204/EPTCS.345.44. Available at https://doi.org/10.4204/EPTCS.

[2] Fang Li, Elmer Salazar & Gopal Gupta (2021): Graph-based Interpretation of Normal Logic Programs. CoRR abs/2111.13249. Available at arXiv:2111.13249.

[3] Fang Li, Huaduo Wang, Kinjal Basu, Elmer Salazar & Gopal Gupta (2021): DiscASP: A Graph-based ASP System for Finding Relevant Consistent Concepts with Applications to Conversational Socialbots. In Andrea Formisano, Yanhong Annie Liu, Bart Bogaerts, Alex Brik, Veronica Dahl, Carmine Dodaro, Paul Fodor, Gian Luca Pozzato, Joost Vennekens & Neng-Fa Zhou, editors: Proceedings 37th International Conference on Logic Programming (Technical Communications), ICLP Technical Communications 2021, Porto (virtual event), 20-27th September 2021, EPTCS 345, pp. 205-218, doi:10.4204/EPTCS.345.35. Available at https://doi.org/10.4204/EPTCS.345.35.

[4] Fang Li, Huaduo Wang & Gopal Gupta (2021): grASP: A Graph Based ASP-Solver and Justification System. CoRR abs/2104.01190. Available at arXiv:2104.01190.

ASP-Based Declarative Process Mining (Extended Abstract)

Abstract

Contribution

Process Mining (PM) [1] is a research area concerned with analyzing event logs stored by (enterprise) information systems, with the aim of better understanding the (business) processes that produce the logs and how they are enacted in the organization owning the systems. A process can be thought of as a set of event sequences that reach a desired goal, whose observed sequences, called process traces, constitute the event log. Different formalisms have been proposed by the Business Process Management (BPM) community for modeling processes, including Petri nets and BPMN [10]. In Declarative Process Mining (DPM) [2] process models are specified declaratively, in a constraint-based fashion, i.e., as sets of constraints, which must be satisfied during the process execution. This type of specifications is particularly suitable for knowledge intensive processes [5] that include a large variety of behaviors and can be more compactly represented under an open world assumption (all behaviors that do not violate the constraints are allowed). Typical process modeling languages for specifying processes in a declarative way are DECLARE [2] and LTLf [6].

We consider three classical problems from (D)PM:

• Log generation [9], i.e., the problem of generating a set of traces of a given length, compliant with a process model;
• Conformance checking [3], i.e., the problem of checking whether the traces of a log are compliant with a process model;
• Query checking [8], i.e., the problem of finding properties of (the process associated to) a log by checking its conformance with the instantiation of candidate template formulas (also called queries).

The control-flow perspective focuses only on process activities, and the specification languages used in this setting include DECLARE or the more general LTLf. In the data-aware perspective, instead, also attributes and their values, i.e., the data, are taken into account, and richer logics are used, such as MP-DECLARE [3] or LTLf with local conditions (L-LTLf); this is the setting adopted in the paper.

To solve the problems of our interest, we exploit the fact that, analogously to the case of LTLf, for every L-LTLf formula, there exists a finite-state automaton (FSA) accepting exactly the traces that satisfy the formula. While every problem has its own specific features, they all share some common parts. As a consequence, the encoding approach of each problem includes the following steps:

• construction of the FSAs corresponding to each L-LTLf input specification;
• definition of an encoding schema for FSAs, as a set of ASP rules;
• definition of an encoding schema for traces, as a set of ASP facts;
• definition of ASP rules to simulate the execution of an FSA on a trace;
• definition of ASP generation and test rules (when needed) for the specific problem.

For all problems, we provide the ASP encoding, an experimental evaluation and, when possible, a comparison with SoA tools. The obtained results show that our approach considerably outperforms the SoA MP-DECLARE Log Generator [9] based on Alloy [7] (in turn based on SAT solvers), which does not exploit the FSA representation of formulas. Slightly worse results are obtained for Conformance Checking wrt the DECLARE Analyzer [3], which is however tailored to DECLARE and, differently from the ASP-based approach, cannot be used to check general LTLf formulas. As to Query Checking, this is the first solution in a data-aware setting, thus, while the experiments show the feasibility of the approach, no comparison with other tools is carried out. The ASP implementation of the approach is not optimized, as the focus of the work is on feasibility rather than performance, so further improvements are possible.

As an example of FSA encoding, consider the (control-flow) response constraint φ = G(a→Fb) saying that "whenever a occurs, it must be eventually followed by b"¹. The FSA shown in Figure 1 accepts all and only the traces that satisfy φ. The corresponding ASP representation is reported next to the automaton. Predicates init and accepting are used to model initial and accepting states, respectively. Predicate trans models state transitions and are labeled each with a unique integer, identifying the transition. Finally, predicate hold models which transitions are enabled by the trace event at time T. The automaton execution on the input trace is then simulated by reading the trace event by event, with the automaton starting in its initial state, and then following, at every step, the transition enabled by the read event. If the formulae labeling the transitions express more complex properties involving data conditions, these can be modeled in the body of the rules for predicate hold. For example, the following rule expresses that transition 1 is enabled at time T if a occurs at T, with a value less than 5 for attribute number: hold(1,T) ← trace(a,T), has_val(number,V,T),V < 5.

By showing how to handle LTLf specifications, namely by exploiting the FSA representation for reducing problems to reachability of accepting states, we have paved the way for the use of ASP as a solving approach to DPM problems and, potentially, to all problems involving temporal specifications over finite traces.

Acknowledgements

References

1. Wil M. P. van der Aalst (2016): Process Mining - Data Science in Action, Second Edition. Springer, doi:10.1007/978-3-662-49851-4.
2. Wil M. P. van der Aalst, Maja Pesic & Helen Schonenberg (2009): Declarative workflows: Balancing between flexibility and support Comput. Sci. Res. Dev. 23(2), pp. 99-113, doi:10.1007/s00450-009-0057-9.
3. Andrea Burattin, Fabrizio Maria Maggi & Alessandro Sperduti (2016): Conformance checking based on multi-perspective declarative process models Expert Syst. Appl. 65, doi:10.1016/j.eswa.2016.08.040.
4. Francesco Chiariello, Fabrizio Maria Maggi & Fabio Patrizi (2022): ASP-Based Declarative Process Mining. In: Proc. of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022.
5. Claudio Di Ciccio, Andrea Marrella & Alessandro Russo (2015): Knowledge-Intensive Processes: Characteristics, Requirements and Analysis of Contemporary Approaches. J. Data Semant., doi: 10.1007/s13740-014-0038-4.
6. Giuseppe De Giacomo & Moshe Y. Vardi (2013): Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. In: Proc. of the 23rd Int. Joint Conf. on Artificial Intelligence, IJCAI/AAAI.
7. Daniel Jackson (2012): Software Abstractions: logic, language, and analysis. MIT Press.
8. Margus Räim, Claudio Di Ciccio, Fabrizio Maria Maggi, Massimo Mecella & Jan Mendling (2014): Log-Based Understanding of Business Processes through Temporal Logic Query Checking In: On the Move to Meaningful Internet Systems: OTM 2014 Conferences, doi:10.1007/978-3-662-45563-0_5.
9. Vasyl Skydanienko, Chiara Di Francescomarino, Chiara Ghidini & Fabrizio Maria Maggi (2018): A Tool for Generating Event Logs from Multi-Perspective Declare Models. In: Proceedings of the Dissertation Award, Demonstration, and Industrial Track at BPM 2018.
10. Mathias Weske (2012): Business Process Management - Concepts, Languages, Architectures, 2nd Edition. Springer, doi:10.1007/978-3-642-28616-2.

¹ Differently from the generic traces usually considered with LTLf, here two activities cannot be true at the same time.