We report about aspmc, which is the working prototype implementation of recent advances in Algebraic Answer Set Counting (AASC). AASC refers to counting the answer sets of a normal answer set program with weights over a semiring. This includes many problems that have recently received growing attention, among them probabilistic reasoning, parameter learning, and most probable explanation inference for answer set programs. aspmc employs a treewidth-aware cycle-breaking to reduce AASC to Algebraic Model Counting (AMC) over a propositional formula with only a slightly increased treewidth. This allows us to lift the performance bounds for AMC in terms of treewidth to AASC. The experimental evaluation of aspmc reveals that these bounds are not only of theoretical interest but also allow us to improve upon the efficiency of other exact counters on standard benchmarks. 1
Recently, there has been a rising interest in reasoning problems for Answer Set Programming (ASP) that go beyond the classical consistency problem. For example, LPMLN[2], P-log [3], PrASP [4], PASP [5] and Problog [6] allow for probabilistic reasoning. Weight Constraints and more generally the asprin framework [7] consider preferential reasoning over answer sets. Finally, algebraic Prolog [8] and Weighted LARS [9] capture and generalize both of these ideas in Algebraic Answer Set Counting (AASC), i.e. weighted answer set counting over semirings. While there are many frameworks allowing such specifications, the corresponding choice of solvers is limited: the clingo solver [10] performs answer set counting by enumeration, which becomes infeasible for millions of answer sets. The dynASP2.5 solver [11] focuses on programs of low treewidth. The Problog solver [12] reduces the problem to Algebraic Model Counting (AMC) [13], for which efficient solvers exist [ 14, 15, 16]. Other solutions exist for approximate probabilistic queries [17] or most probable answer set inference [18], which are outside of our scope as we aim for exact weighted answer set counting.
While Problog does not accept arbitrary ASP programs as input, we still consider its strategy to be the most promising approach. The basic idea, described in detail in [19], is the following. First one breaks the cyclic dependencies in the input program, obtaining a tight program, where the answer sets are the models of its Clark completion [20]. The Clark completion can then be compiled it into an equivalent d-DNNF/SDD representation, where AMC is possible in linear time [13]. This approach allows for practically relevant instances to be solved [21]. However, the way cycles in the program’s positive dependency graph are broken can have a negative effect on the treewidth.
Cycle breaking is well studied in the ASP community. Among others, Hecher’s [22] translation from ASP to SAT guarantees that the treewidth of the SAT instance is ( log()), where is the original treewidth and is the minimum of and the size of the largest strongly connected component of the dependency graph of the program. Unfortunately, this translation does not preserve models bijectively. In contrast, cycle breaking used in Problog [23, 21] and others [24] preserve models without strong treewidth bounds. We address this and provide the following: • We show that every program of treewidth can be translated into an acyclic program with treewidth at most · cbs(DEP(Π)), where cbs(DEP(Π)), is the component-boosted backdoor size of the dependency graph of Π; notably, cbs(.) is a novel parameter on directed graphs combining backdoor sets and decomposability to measure the cyclicity. • We provide a prototype implementation aspmc that performs AASC by exploiting the constructive proof of the above result. Our experimental results show that when a program has many answer sets, aspmc outperforms Problog, clingo and lp2sat [24].
We assume familiarity with the basics of Answer Set Programming (ASP) [25] and use (Π) and (Π) for the atoms and answer sets of a program Π, respectively.
We introduce AASC by using the following minimal instantiation Π of the smokers program, which is a standard example from probabilistic logic programming [6].
{stress()} ← smokes() ←
stress() {influences(, )} ← smokes() ← influences(, ), smokes() for = 1, 2 for = 1, 2 for + 1 = mod 2 for + 1 = mod 2 This encodes that for person 1 and 2 it is randomly determined whether they are stressed. If they are, they smoke. Furthermore, if one influences the other, which is again random, and smokes, then they also smoke. In order to introduce probabilities, we use algebraic measures. Definition 1 (Measure). A (factorized algebraic) measure = ⟨Π, , ⟩ consists of an answer set program Π, a weight function and a set of extensional atoms ⊆ (Π). The weight (ℐ) of an answer set ℐ and the weight () of ∈ (Π) are defined respectively as (ℐ) := ∏︁ () ·
∏︁ (¬) and () := ∈ ∩ℐ ∈ ∖ℐ
∑︁ ℐ∈(Π),∈ℐ (ℐ).
Measures “measure” values associated with answer set. AASC is then to evaluate (), i.e., to sum up the weights of all answer sets that satisfy . We do not focus on any particular application of AASC.
Usually, measures are not necessarily factorized and allow complex terms of sums and products to define the weight of an answer set. Furthermore, they are defined not only for weights over the reals but over any semiring. We stick to the restricted definition above for simplicity.
We can assign probabilities using the measure = ⟨Π, , ⟩, where
(stress()) = 0.4 (influences(, )) = 0.3 (¬stress()) = 0.6
= 1, 2
(¬influences(, )) = 0.7
+ 1 ≡ mod 2
This means that the probability of a person being stressed is 0.4 and the probability that a
person influences their friend is 0.3. Therefore, the answer set ℐ = {stress(
Ground Π
Π′
Currently, the most promising strategy to perform AASC is the one used by Problog [19]. Here, the general idea is to compile the program Π into an equivalent tractable circuit representation , like SDD [26] or sd-DNNF [27]. When this succeeds, AASC is possible in linear time in the size of the circuit . However, while there are so called knowledge compilers that perform this task, they can only work on propositional formulas.
The whole pipeline that we and (similarly) Problog use is therefore as in Figure 1. Given an algebraic measure , we first ground the logical part of the measure, obtaining a ground program Π. Next, Π is translated into an equivalent program Π′, which is acyclic, i.e., which does not contain rules with cyclic positive dependencies. For such programs it is known [20] that the Clark completion of Π′ results in a propositional formula , whose models correspond one-to-one to the answer sets of Π′. Thus, by compiling into a tractable circuit representation , using a tool like c2d [28], we can obtain the probability as the final result.
Our contribution in [1] focused on the second step in this pipeline, by introducing an algorithm that breaks cycles in a treewidth-aware fashion. Finding an equivalent and acyclic program Π′ of low treewidth can be beneficial since there are performance guarantees for knowledge compilation based on treewidth [26]. This motivates our main result for cycle-breaking: Theorem 2. For any measure = ⟨Π, , ⟩, there exists a measure ′ = ⟨Π′, , ⟩ with an acyclic program Π′ s.t.
• for all ∈ (Π) it holds that () = ′(), • the treewidth of Π′ is bounded by · cbs(DEP(Π)), where is the treewidth of Π.
Here, cbs(DEP(Π)) is a novel parameter, called component-boosted backdoor size, which intuitively measures the cyclicity of the dependency graph of Π. It is defined as follows: Definition 3. Let be a digraph. Then, the component-boosted backdoor size cbs() is • 1, if is acyclic (which includes () = ∅) • 2, if is a polytree, i.e. the undirected version of is connected and acyclic • max{cbs() | ∈ SCC()}, if is cyclic but not strongly connected • min{cbs( ∖ ) · (|| + 1) | ⊆ ()} otherwise
As the name suggests, generalizes the idea of backdoors, which have already been considered in the context of ASP [29]. In our context, a backdoor for a digraph is a vertex set , such that ∖ is a polytree, polyforest or dag. The backdoor size of is the minimum size of a backdoor for plus 1. Note that our parameter additionally considers that ∖ may consist of separate SCCs that can be handled recursively and is therefore bounded by backdoor size.
The proof of Theorem 2 is constructive, in the sense that it allows the formulation of an
algorithm that computes Π′. Broadly speaking, the idea is to gradually introduce copies
(
← 1, . . . , , not 1, . . . , not and replace them by
() ← (11), . . . , (), not 1, . . . , not , thus expressing the truth of ()) in terms of already known approximations of 1, . . . , . Theorem 2 guarantees that, if we consider the atoms in the correct order, a fixed point can be reached after considering each atom at most cbs(DEP(Π)) times. We cannot go into details here due to lack of space but refer interested readers to the full paper [1]. Nevertheless, we can apply Theorem 2 to our running example and obtain Π′ as
{stress()} ←
{influences(, )} ←
for = 1, 2
for + 1 = mod 2
smokes(
The remaining two ideas preserve answer sets bijectively. As such, Janhunen’s [24] was considered for the implementation of Problog (cf. [31]) and Mantadeli’s and Janssen’s [23] is even still part of the standard Problog implementation. While the original papers did not consider the effects that these translations have on treewidth, the strategy to bound treewidth used in [1, 22] can be applied to these translation as well. This results in treewidth upper-bounds of log2(max) and , respectively, where max is the size of the largest strongly connected component of the dependency graph of Π and is the largest number of simple (directed) cycles that any atom is contained in.
One can show that (.) is always bounded by and possible exponentially smaller, since on a clique of size , we have ≥ 2− 1, whereas (.) of a clique of size is . Therefore, Theorem 2 provides strictly better treewidth bounds in general. Observe, however, that for the ifrst translation, the factor grows logarithmically in max. It follows that for a clique of size the upper-bound log2() of the first translation is exponentially lower than , which is our bound. On the other hand for a polytree with vertices ( ) = 2, whereas log2() is not constant.
We implemented a system that adheres to the evaluation procedure above, resulting in the prototypical solver aspmc1. aspmc is written in Python3 and allows for Problog programs Π as input in order to compute the answers to probabilistic (resp. algebraic) queries in Π. Benchmark Setting. In order to evaluate the performance of aspmc, we compare the computation of probabilities for atoms of Problog programs. For solvers that are not able to evaluate probabilistic queries we compute the number of answer sets.
Compared Solvers. In our experiments, we mainly compare against Problog 2.1.0.42 with the arguments “-k sdd”, clingo 5.4.0, where we used arguments “-q -n 0” in order to count answer sets, as well as lp2sat+c2d, where instances are translated [32] to CNFs by lp2normal 2.18 in combination with lp2atomic 1.17 and lp2sat 1.24 with answer sets being counted with c2d version 2.2 [28]. Our system is aspmc+c2d, which breaks the cycles and performs AASC on a tractable circuit representation of the constructed CNF, obtained via c2d 2.2.
Benchmark Instances. The instances we used are the benchmarks from [33] and were kindly provided to us by the authors via personal communication. They adhere to typical benchmark domains consisting of 490 instances of the standard smoker’s example, 50 instances of the gene’s problem [34] and 63 web knowledge base instances [35].
Benchmark Platform. All our solvers ran on a cluster consisting of 12 nodes. Each node of the cluster is equipped with two Intel Xeon E5-2650 CPUs, where each of these 12 physical 1available at github.com/raki123/aspmc (open source). 1800 1600 1400 ]s1200 [ e itm1000 k c lco 800 llaw 600 400 200 0 0 aspmc+c2d problog lp2sat+c2d* clingo* 50 100 numb1e5r0of instances200 250 300 cores runs at 2.2 GHz clock speed and has access to 256 GB shared RAM. Results are gathered on Ubuntu 16.04.1 powered on kernel 4.4.0-139 with hyperthreading disabled and Python 3.7.6. Experimental Results & Discussion. In our evaluation, we mainly compare total wall clock time and number of solved instances. Concerning benchmark limits, we consider a timeout of 1800 seconds and an 8 GB RAM limit per instance and solver.
Figure 2 (left) shows a plot over all instances, which indicates that aspmc+c2d solves more instances faster than any of the other configurations that we benchmarked. The detailed results in Figure 2 (right) indicate that cycle breaking works well for probabilistic reasoning.
Other experiments [1] showed that clingo is extremely fast at enumerating solutions. Thus, on instances with not that many solutions, clingo is faster than any of the compilation-based approaches we considered. On the other hand, when there are more solutions, considering each of them once as in enumeration, is outperformed by the compilation-based approaches lp2sat+c2d, aspmc+c2d and Problog that solve significantly more instances in this case.
For any program Π, there is an equivalent acyclic program, whose treewidth is at most cbs(DEP(Π)) times bigger, where cbs(.) is a novel parameter that measures the cyclicity of directed graphs. The bound on the treewidth provides us with worst case guarantees for the knowledge compilation step in AASC. Our experimental evaluation of the prototype implementation aspmc shows that this idea does not only provide interesting theoretical results but provides a significant speedup on standard Problog benchmarks compared to other solvers.
The work is supported by Austrian Science Fund (FWF), Grants Y698, P32830 and W1255-N23, the Vienna Science and Technology Fund, Grant WWTF ICT19-065. BCP, in: International Conference on Theory and Applications of Satisfiability Testing, Springer, 2006, pp. 424–429. [17] D. Tuckey, A. Russo, K. Broda, Pasocs: A parallel approximate solver for probabilistic logic programs under the credal semantics, arXiv preprint arXiv:2105.10908 (2021). [18] M. Nickles, diff-sat–a software for sampling and probabilistic reasoning for sat and answer set programming, arXiv preprint arXiv:2101.00589 (2021). [19] D. Fierens, G. Van den Broeck, J. Renkens, D. Shterionov, B. Gutmann, I. Thon, G. Janssens, L. De Raedt, Inference and learning in probabilistic logic programs using weighted boolean formulas, Theory and Practice of Logic Programming 15 (2015) 358–401. [20] F. Fages, Consistency of Clark’s completion and existence of stable models, Journal of
Methods of logic in computer science 1 (1994) 51–60. [21] J. Vlasselaer, G. Van den Broeck, A. Kimmig, W. Meert, L. De Raedt, Tp-compilation for inference in probabilistic logic programs, International Journal of Approximate Reasoning 78 (2016) 15–32. [22] M. Hecher, Treewidth-aware Reductions of Normal ASP to SAT - Is Normal ASP Harder than SAT after All?, in: Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, 2020, pp. 485–495. URL: https://doi.org/10. 24963/kr.2020/49. doi:10.24963/kr.2020/49. [23] T. Mantadelis, G. Janssens, Dedicated tabling for a probabilistic setting, in: Technical Communications of the 26th International Conference on Logic Programming, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2010. [24] T. Janhunen, Representing normal programs with clauses, in: ECAI, volume 16, Citeseer, 2004, p. 358. [25] T. Eiter, G. Ianni, T. Krennwallner, Answer set programming: A primer, in: Reasoning
Web International Summer School, Springer, 2009, pp. 40–110. [26] A. Darwiche, Sdd: A new canonical representation of propositional knowledge bases, in:
Twenty-Second International Joint Conference on Artificial Intelligence, 2011. [27] A. Darwiche, P. Marquis, A knowledge compilation map, Journal of Artificial Intelligence
Research 17 (2002) 229–264. [28] A. Darwiche, New advances in compiling CNF into decomposable negation normal form, in: ECAI, IOS Press, 2004, pp. 328–332. [29] J. K. Fichte, S. Szeider, Backdoors to tractable answer set programming, Artif. Intell. 220 (2015) 64–103. URL: https://doi.org/10.1016/j.artint.2014.12.001. doi:10.1016/j. artint.2014.12.001. [30] F. Lin, J. Zhao, On tight logic programs and yet another translation from normal logic programs to propositional logic, in: International Joint Conference on Artificial Intelligence, 2003. [31] D. Fierens, G. Van den Broeck, I. Thon, B. Gutmann, L. D. Raedt, Inference in probabilistic logic programs using weighted cnf’s, in: Proceedings of the Twenty-Seventh Conference on Uncertainty in Artificial Intelligence, 2011, pp. 211–220. [32] J. Bomanson, lp2normal - A normalization tool for extended logic programs, in: LPNMR, volume 10377 of Lecture Notes in Computer Science, Springer, 2017, pp. 222–228. [33] E. Tsamoura, V. Gutiérrez-Basulto, A. Kimmig, Beyond the Grounding Bottleneck: Datalog Techniques for Inference in Probabilistic Logic Programs, in: Conference on Artificial Intelligence (AAAI), AAAI Press, 2020, pp. 10284–10291. URL: https://aaai.org/ojs/index. php/AAAI/article/view/6591. [34] O. Ourfali, T. Shlomi, T. Ideker, E. Ruppin, R. Sharan, Spine: a framework for signalingregulatory pathway inference from cause-effect experiments, Bioinformatics 23 (2007) i359–i366. [35] J. Davis, P. Domingos, Deep transfer via second-order markov logic, in: Proceedings of the 26th annual international conference on machine learning, 2009, pp. 217–224.