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.