# splitting_an_lpmln_program__5ec62856.pdf Splitting an LPMLN Program Bin Wang, Zhizheng Zhang, Hongxiang Xu, Jun Shen School of Computer Science and Engineering Southeast University, Nanjing 211189, China {kse.wang, seu zzz, xhx1693, junshen}@seu.edu.cn The technique called splitting sets has been proven useful in simplifying the investigation of Answer Set Programming (ASP). In this paper, we investigate the splitting set theorem for LPMLN that is a new extension of ASP created by combining the ideas of ASP and Markov Logic Networks (MLN). Firstly, we extend the notion of splitting sets to LPMLN programs and present the splitting set theorem for LPMLN. Then, the use of the theorem for simplifying several LPMLN inference tasks is illustrated. After that, we give two parallel approaches for solving LPMLN programs via using the theorem. The preliminary experimental results show that these approaches are alternative ways to promote an LPMLN solver. Introduction The notion of splitting sets introduced by Lifschitz and Turner (1994) has been regarded as one of the most important tools on both theoretical and practical aspects in Answer Set Programming (ASP) (Gelfond and Lifschitz 1988). Intuitively, a splitting set of an ASP program is a set of literals, by which the program can be divided into two parts, called bottom part and top part . Then, the stable models of the original ASP program can be computed by solving these two parts. It has been shown in several works (Lifschitz and Turner 1994; Ji et al. 2015) that the splitting set theorem can be used to simplify ASP programs and the proofs of some properties of ASP, and to develop more effective ASP solvers. Meanwhile, it is also shown that the splitting set theorem is a useful property for several extensions of ASP such as CR-Prolog (Balduccini 2009), Epistemic Specification (Watson 2000) etc. LPMLN (Lee and Wang 2016) is a new extension of ASP that incorporates the idea of Markov Logic Networks (MLN) (Richardson and Domingos 2006) and can be viewed as a weighted ASP program. In recent years, several results on LPMLN have been presented. In the theoretical aspect, the relationships between LPMLN and some other knowledge representation languages have been investigated. For example, Lee and Wang (2016) presented the translations from MLN, P-log (Baral, Gelfond, and Rushton 2009), Prob Log (De Raedt, Kimmig, and Toivonen 2007) and ASP Corresponding author Copyright c 2018, Association for the Advancement of Artificial Intelligence (www.aaai.org). All rights reserved. with weak constraints (Calimeri et al. 2012) to LPMLN respectively. Lee and Yang (2017) also presented a translation from LPMLN to ASP with weak constraints. Balai and Gelfond (2016) presented a translation from LPMLN to P-log. These results demonstrate the expressivity of LPMLN and open a way to implement an LPMLN solver. In the practical aspect, several solvers of LPMLN have been developed through using the above translations, such as LPMLN2ASP, LPMLN2MLN (Lee, Talsania, and Wang 2017), and LPMLN-Models (Wang and Zhang 2017). In particular, LPMLN-Models is a parallel LPMLN solver. These implementations also stimulate the study and use of LPMLN conversely. Usually, an LPMLN program is much harder to solve than its unweighted ASP counterpart. Hence, to use LPMLN in more practical scenarios, we need to investigate more useful properties to simplify the inference tasks for an LPMLN program, and develop more effective ways to promote an LPMLN solver. Our goal in this paper is to investigate the splitting set theorem for LPMLN programs and show the usefulness of the theorem in simplifying the inference tasks for LPMLN and promoting an LPMLN solver. In this paper, we propose the splitting set theorem for LPMLN firstly, which shows that the tasks of computing stable models and their weight degrees of an LPMLN program can be converted into the same kind of tasks of the corresponding top part and bottom part . Secondly, we investigate a special kind of LPMLN programs called independently divisible LPMLN programs, and derive the splitting set theorem for such kind of programs. This special theorem directly implies that all basic LPMLN inference tasks discussed in this paper can be simplified for an independently divisible LPMLN program. Finally, we give two parallel approaches for solving normal and independently divisible LPMLN programs respectively, which is a straightforward application of the splitting set theorem. The preliminary experimental results show that these approaches are alternative ways to promote an LPMLN solver. Preliminaries An LPMLN program is a finite set of weighted rules w : r, where w is either a real number or the symbol α denoting The Thirty-Second AAAI Conference on Artificial Intelligence (AAAI-18) the infinite weight , and r is an ASP rule of the form l1 ... lk lk+1, ..., lm, not lm+1, ..., not ln. (1) where ls are literals, is epistemic disjunction, and not is default negation. For an ASP rule r of the form (1), head(r) = {li|1 i k}, body+(r) = {li|k + 1 i m}, body (r) = {li|m + 1 i n}, and lit(r) = head(r) body+(r) body (r). For an ASP program Π, we have head(Π) = r Π head(r), body+(Π) = r Π body+(r), body (Π) = r Π body (r), and lit(Π) = head(Π) body+(Π) body (Π). An LPMLN rule w : r is called soft if w is a real number, and hard if w is α. We use M to denote the set of unweighted ASP counterpart of an LPMLN program M, i.e. M = {r|w : r M}. And an LPMLN program is called ground if its rules contain no variables. For a ground LPMLN program M, we use W(M) to denote the weight degree of M, i.e. W(M) = exp w:r M w . Usually, a non-ground LPMLN program is considered as a shorthand for the corresponding ground program. So for simplicity, we restrict attention to ground LPMLN programs only. A ground LPMLN rule w : r is satisfied by a consistent set X of ground literals, denoted by X |= w : r, if X |= r by the notion of satisfiability in ASP. An LPMLN program M is satisfied by X, denoted by X |= M, if X satisfies all rules in M. We use MX to denote the LPMLN reduct of an LPMLN program M w.r.t. X, i.e. MX = {w : r M | X |= w : r}. X is a stable model of the program M if X is a stable model of MX. And we use SM(M) to denote the set of all stable models of an LPMLN program M. For a stable model X of an LPMLN program M, the weight degree W(M, X) of X w.r.t. M is defined as W(M, X) = exp and the probability degree Ps(M, X) of X w.r.t. M is defined as Ps(M, X) = lim α W(M, X) ΣX SM(M)W(M, X ) (3) For a proposition β, its probability degree Pp(M, β) w.r.t. M is defined as X SM(M) and X|=β Ps(M, X) (4) For an LPMLN program M and a literal l, we say that the tuple (l, Pp(M, l)) is a probabilistic consequence of M, denoted by M |= (l, Pp(M, l)), if Pp(M, l) = 0. Usually, there are four kinds of basic inference tasks (Lee, Talsania, and Wang 2017). For an LPMLN program M, - MAP (Maximum A Posteriori) inference is to compute the most probable stable models of M; - MAPL (Maximum A Posteriori for Literals) inference is to check if some literals are in the most probable stable models of M, which can be converted to MAP inference; - MPS (Marginal Probability of Stable models) inference is to compute probability degrees of all stable models of M; - MPL (Marginal Probability of Literals) inference is to compute the probability degree of a literal w.r.t. M, which is to add the probability degrees of the stable models of M that contains the literal. Splitting Sets for ASP The notion of splitting sets for ASP is introduced by Lifschitz and Turner (1994). A splitting set U for a ground ASP program Π is a set of literals such that, for each rule r Π, if head(r) U = then lit(r) U. The bottom part of Π w.r.t. U is the set b(Π, U) = {r Π | head(r) U = }, and the top part of Π w.r.t. U is the set t(Π, U) = Π b(Π, U). Let U, X be sets of literals, and Π an ASP program, we use d(Π, U, X) to denote the set of rules r Π such that body+(r) U X or body (r) U X = , called deleting set, and we use e(Π, U, X) to denote the set of rules obtained from Π by deleting: 1. all rules in d(Π, U, X); 2. all formulas of the form l or not l in the bodies of the remaining rules, where l U. The process containing above two steps that compute the set e(Π, U, X) is called the partial evaluation for ASP. Let U be a splitting set of an ASP program Π, a solution of Π w.r.t. U is a pair X, Y of the sets of literals such that - X is a stable model of b(Π, U); - Y is a stable model of e(t(Π, U), U, X); - X Y is consistent. The splitting set theorem for ASP shows that, for an ASP program Π and a splitting set U of Π, a set S is a stable model of Π iff S = X Y for a solution X, Y of Π w.r.t. U. Splitting Sets for LPMLN In this section, we describe the notations and theorem related to splitting sets for LPMLN. Without loss of generality, we consider only grounded finite LPMLN programs in rest of the paper. The Definition of Splitting Sets for LPMLN Definition 1 (Splitting Sets for LPMLN). For a ground LPMLN program M, a set U of ground literals is called a splitting set of M, if for each LPMLN rule w : r M, head(r) U = implies lit(r) U. It is obvious that the definition of the splitting sets for LPMLN is quite similar to the definition of the splitting sets for ASP. Analogously, we can define the bottom part b(M, U) and top part t(M, U) of an LPMLN program M w.r.t. one of its splitting sets U as b(M, U) = {w : r M | head(r) U = } (5) t(M, U) = M b(M, U) (6) Example 1. Consider the following program M1: 1 : a b, not c. (r1) 1 : b c, not a. (r2) 1 : c. (r3) Figure 1: Dependency Graph of the Program in Example 1 Trivially, both and lit M1 = {a, b, c} are splitting sets of M1. Besides, the set U1 = {c} is also a splitting set of M1, and we have b(M1, U1) = {r3} and t(M1, U1) = {r1, r2}. Let us reconsider the top part and the bottom part of an LPMLN program from the side of dependency graph. A dependency graph of an LPMLN program M is a directed graph whose vertices are literals in M, and there is an arc from p to q if there is a rule w : r M such that p head(r) and q body+(r) body (r). For example, the graph shown in Figure 1 is the dependency graph of the program M1 in Example 1. By the definition of splitting sets, if U is a splitting set of the program M, then U head(t(M, U)) = . On one hand, it means there are no edges that are from literals in U to literals in the head of the top part. On the other hand, it means literals in the bottom part cannot be derived by any rules in the top part. Splitting Set Theorem for LPMLN Now, we explore the use of the splitting sets in dividing the tasks of computing the stable models and their weight degrees of an LPMLN program. First of all, we define some notions for convenient description. Definition 2 (Deleting Set). Let U, X be sets of ground literals, and M a ground LPMLN program, the deleting set d(M, U, X) of M w.r.t. U and X is d(M, U, X) = {w : r M | body+(r) U X or body (r) U X = } (7) Definition 3 (Partial Evaluation Reduct). For an LPMLN rule w : r and a set U of literals, the partial evaluation reduct pred(w : r, U) of the rule w.r.t. U is obtained by - deleting all formulas of the form l and not l, where l U; - dropping the weight w. Definition 4 (Grouping Set). For an LPMLN program M and a set U of literals, the grouping set g(M, U) of M w.r.t. U is a set of rule sets defined as follows. g(M, U) ={M M | w1 : r1, w2 : r2 M , w3 : r3 M M , pred(w1 : r1, U) = pred(w2 : r2, U), pred(w3 : r3, U) = pred(w1 : r1, U)} We can observe that, for each rule set M g(M, U), all rules in M have the same partial evaluation reduct pred(w : r, U) w.r.t. U, where w : r M . Definition 5 (Representative Rule). Let M be an LPMLN program, and U a set of literals. For each rule set M g(M, U), the rule w : r , denoted by rep(M , U), is the representative rule w.r.t. M , where r is the partial evaluation reduct of a rule in M w.r.t. U, and w is obtained by w:r M w (9) Based on the concepts of deleting set, grouping set and representative rule, we define the partial evaluation for LPMLN. Definition 6 (Partial Evaluation for LPMLN). For an LPMLN program M and two sets U, X of literals, the set e(M, U, X) of rules obtained by the partial evaluation for LPMLN is e(M, U, X) ={rep(M , U) | M g(M d(M, U, X), U)} (10) Now we define the solutions to an LPMLN program M w.r.t. a splitting set of M. Definition 7 (Solutions for LPMLN). For an LPMLN program M and a splitting set U of M, a solution to M w.r.t. U is a pair X, Y of sets of literals such that - X is a stable model of b(M, U); - Y is a stable model of e(t(M, U), U, X); - X Y is consistent. Example 2. Consider the LPMLN program M1 in Example 1, the set U1 = {c} is a splitting set of M1. Firstly, by the definition of the stable models of an LPMLN program, X = {c} is a stable model of the bottom part b(M1, U1). Then, we have the deleting set d(t(M1, U1), U1, X) = {r1}, the grouping set g(t(M1, U1) d(t(M1, U1), U1, X), U1) = {{r2}}, and by the partial evaluation for LPMLN, we have e(t(M1, U1), U1, X) = {b not a.}. Finally, Y = {b} is a stable model of e(t(M1, U1), U1, X), and X Y is consistent. Hence, the pair X, Y is a solution to the program M1 w.r.t. the splitting set U1. Theorem 1 (Splitting Set Theorem for LPMLN). Let U be a splitting set for an LPMLN program M. A set S of literals is a stable model of M iff S = X Y for a solution X, Y to M w.r.t. U. And the weight degree W(M, S) of S w.r.t. M can be reformulated as W(M, S) =W(b(M, U), X) W(e(t(M, U), U, X), Y ) W(d(t(M, U), U, X)) (11) Example 3. Continue Example 2, by Theorem 1, we can derive that S = X Y = {c, b} is a stable model of M, and the weight degree W(b(M1, U1), X) = e1, W(e(t(M1, U1), U1, X), Y ) = e1, and W(d(t(M1, U1), U1, X)) = e1. By the Equation (11), W(M1, S) = e1 e1 e1 = e3. It is easy to check that the above computing results coincide with the related definitions of LPMLN. Apparently, Theorem 1 contains two parts. One is about weight degrees evaluation of the stable models. Another is about stable models generation. In the rest of this subsection, we give the basic ideas of the proof of Theorem 1 (the complete proof of the theorem can be found in the extended version of the paper1). - For the first part, we give the intuitive meanings of the above definitions such that the soundness of the weight degree evaluation is clear. - For the second part, we prove that there is a one-to-one mapping between the splitting sets of an LPMLN program and its ASP translation, which makes the soundness of this part clear. Here are the intuitive meanings of the above definitions. Consider an LPMLN program as a set of weighted evidence for decision making and a rule is a piece of weighted evidence, then the strength of a piece of evidence is the sum of all the weights of rules that have the same unweighted form. The partial evaluation reduct of a rule w.r.t. a set U can be viewed as a piece of reduced evidence by removing the factors in U. Under such an assumption, a group in a grouping set w.r.t. U is a set of weighted evidence that are same if reduced by U. Furthermore, the representative rule of a group is just a piece of reduced evidence obtained from the original LPMLN program w.r.t. U, and its weight is the sum of the strengths of a set of original evidence that can be reduced to it by U. Hence, we can find that the evaluation of weight of a representative rule is compatible with the computation of the strength of a piece of evidence in LPMLN. Now, we use Example 4 to illustrate it. Example 4. Consider an LPMLN program M3 that is obtained by adding following rule (r6) into the program M1 in Example 1. 1 : b not a. (r6) The set U = {c} is a splitting set of M3, the set X = {c} is a stable model of b(M3, U), the deleting set d(t(M3, U), U, X) = {r1}. Let M be t(M3, U) d(t(M3, U), U, X), the grouping set g(M , U) = {{r2, r6}}, and the rule set obtained by the partial evaluation for LPMLN is e(t(M3, U), U, X) = {2 : b not a.}. It is clear that the weights of the same reduced evidences are accumulated properly in partial evaluation for LPMLN. Now, let us see Equation (11), by which the computing of weight degree of a stable model is divided into three parts. Suppose S = X Y is a stable model of an LPMLN program M, and X, Y is a solution to M. By the definition, the weight degree of S depends on the rules in M satisfied by S, which means, to compute the weight degree of S, we have to consider rules in the bottom part, deleting set, and the set obtained by partial evaluation. It is easy to check that all rules in the corresponding deleting set can be satisfied by the stable model S. Therefore, Equation (11) is provably correct. From above discussion, we can define the equivalent of an LPMLN program. Definition 8. An LPMLN program M is equivalent to another program M , if 1http://cse.seu.edu.cn/Personal Page/seu zzz/publications/ lpmln-splitting-sets.pdf - SM(M) = SM(M ), and - for each stable model S SM(M), W(M, S) = W(M , S). Lemma 1. Let M1 and M2 be LPMLN programs. If M1 = M2, and for each rule r M1, w :r M1, and r =r w = w :r M2, and r =r w (12) then the program M1 is equivalent to M2. And we give an equivalent definition of the results obtained by partial evaluation for LPMLN, which is useful for the proof of stable models generation part. Definition 9. For an LPMLN program M and two sets U, X of literals, the set e (M, U, X) of rules is obtained from e(M, U, X) by replacing every rule w : r e(M, U, X) with an LPMLN program M such that - M = {r} and w = w :r M w ; - |M | = |M |, where M g(M d(M, U, X), U) and w : r is the representative rule of M . For the second part, the basic idea of the proof is to translate an LPMLN program into an ASP program and use the splitting set theorem for ASP programs. Firstly, we give a brief review of the translation from LPMLN to ASP. For an LPMLN program M, its ASP translation τ(M) is obtained by turning each rule wi : ri M, where ri is of the form (1), and i is the index of the rule, into following two ASP rules. unsat(i) lk+1, ..., lm, not lm+1, ..., not ln, not l1, ..., not lk. l1 ... lk lk+1, ..., lm, not lm+1, ..., not ln, not unsat(i). It has been shown in (Lee, Talsania, and Wang 2017) that there is a 1-1 correspondence φ between SM(M) and the set of stable models of τ(M). The proof of the second part of Theorem 1 is outlined as following Lemma 2 - 4. Lemma 2. For an LPMLN program M and a splitting set U of M, there exists a splitting set U of the translation τ(M) such that - U = U {unsat(i) | wi : ri b(M, U)}, - τ(b(M, U)) = b(τ(M), U ), and - for a stable model X SM(b(M, U)), τ(e (t(M, U), U, X)) = e(t(τ(M), U ), U , φ(X)). Lemma 3. Let U be a splitting set for an LPMLN program M. A set S of literals is a stable model of M iff S = X Y for a solution φ(X), φ(Y ) to the translation τ(M) w.r.t. U , where U is defined as in Lemma 2. Lemma 4. Let U be a splitting set for an LPMLN program M. A pair X, Y is a solution to M w.r.t. U iff φ(X), φ(Y ) is a solution to the translation τ(M) w.r.t. U , where U is defined as in Lemma 2. It is interesting that the stable models generation part of splitting set theorem for LPMLN is quite similar to the ones for ASP. By above proof, we can find that such similarity is not a coincidence. Splitting Sequence Theorem for LPMLN Similar to ASP, we can derive following splitting sequence theorem straightforwardly. Definition 10 (Splitting Sequence for LPMLN). Let U0, . . . , Un be a finite sequence of sets of literals, for an LPMLN program M, the sequence is called a splitting sequence of M, if it satisfies - for any 0 k n, Uk is a splitting set of M; and - for any 0 k < n, Uk Uk+1. Definition 11. Let U0, . . . , Un be a splitting sequence of an LPMLN program M, a solution to M w.r.t. the splitting sequence is a sequence X0, . . . , Xn+1 of sets of literals such that - X0 is a stable model of b(M, U0); - for any 0 < k n, Xk is a stable model of the program Mk, where Mk is obtained by Mk = e(b(M, Uk) b(M, Uk 1), Uk 1, 0 i