=Paper=
{{Paper
|id=Vol-1868/p5
|storemode=property
|title=A Parallel LPMLN Solver: Primary Report
|pdfUrl=https://ceur-ws.org/Vol-1868/p5.pdf
|volume=Vol-1868
|authors=Bin Wang,Zhizheng Zhang
|dblpUrl=https://dblp.org/rec/conf/lpnmr/WangZ17
}}
==A Parallel LPMLN Solver: Primary Report==
A Parallel LPMLN Solver: Primary Report Bin Wang and Zhizheng Zhang School of Computer Science and Engineering, Southeast University, Nanjing 211189, China, {kse.wang, seu zzz}@seu.edu.cn Abstract. LPMLN that incorporates Answer Set Programming (ASP) and Markov Networks is a powerful tool for handling uncertain and non- monotonic knowledge. In this paper, we propose a parallelized method for solving LPMLN programs. The main idea of the method is parti- tioning a ground LPMLN program into several corresponding programs, called augmented subsets, where each augmented subset will be trans- lated into an ASP program, hence stable models and their penalties of all these augmented subsets can be generated concurrently by calling ef- ficient ASP solvers. Then, the LPMLN solver computes the stable models and their weights of the LPMLN program from the stable models and their penalties of all augmented subsets of the LPMLN program, and gives the results of an inference task. We present the approaches to the partition and the translation, and give some theoretical results that guarantee the correctness of the parallelized method. Experimental results show that the parallelized method can improve performance of solving LPMLN programs. Keywords: parallel, LPMLN solver, Answer Set Programming 1 Introduction LPMLN [12] is a newly introduced knowledge representation language that com- bines the ideas of Answer Set Programming (ASP) [7] and Markov Logic Net- works (MLN) [18]. The researches in [10,12,13] show the powerful expressivity of LPMLN , which is able to embed MLN and several probabilistic logic languages, such as ProbLog [4], Pearls’ Causal Models [17], and P-log [2]. So far as we know, several approaches to the implementation of the LPMLN solver have been presented. The basic idea of all the approaches is to compile the LPMLN language into another formalism that has efficient solvers. Lee and Wang [12] extended the concept of completion and tightness from ASP to LPMLN , which can be used to translate a tight LPMLN program to an MLN program. Furthermore, through combining with the loop formulas technique [15,9], an arbitrary LPMLN program can be translated into an MLN program such that MLN solvers such as Alchemy [8], Tuffy [16] etc. can be used for solving LPMLN programs. Balai and Gelfond [1] presented a translation from a subset of LPMLN to P-log [2] that is a probabilistic extension of ASP such that LPMLN programs 2 Bin Wang and Zhizheng Zhang can be solved by using P-log solvers. Most recently, Lee and Yang [13] proposed a translation from LPMLN to a set of weak constraints [3] and choice formulas that can be translated into an ASP program, such that Maximum A Posteriori probability (MAP) estimates of an LPMLN program can be solved by calling ASP solvers such as CLASP [6], DLV [14] etc. The inference of LPMLN programs, especially exact inference, needs to compute all stable models of the program and then to do statistic computation on those stable models, which is time consuming. To implement an efficient LPMLN solver, this paper investigates the parallelized method for solving an LPMLN program. In this paper, we aim at presenting a parallelized method for solving LPMLN programs. The main idea of the method is partitioning a ground LPMLN program into several corresponding programs, called augmented subsets, where each aug- mented subset will be translated into an ASP program, hence stable models and their penalties of all these augmented subsets can be generated concurrently by calling efficient ASP solvers. Then, the LPMLN solver computes the stable mod- els and their weights of the LPMLN program from the stable models and their penalties of all augmented subsets of the LPMLN program, and gives the results of an inference task. Algorithm 1: parallel LPMLN Solver Input: M : an LPMLN program, n: number of processors, q: query Output: R: inference results 1 begin // stage 1: partition M into n augmented subsets 2 S =Partition(M, n) ; 3 for Si ∈ S do // for each processor do ... // stage 2:translate Si to an ASP program Π i 4 Π i =Translation(M, Si ); // stage 3: generate stable models and their penalties 5 P enalty i , AS i =ASPSolver(Π i ); 6 weight of AS i is W eightComputing(P enalty i ); // stage 4: synthesis stage SM = n i S 7 i=1 AS ; 8 R =AnswerQuery(SM, q); 9 return R; At a high abstract level, as shown in Algorithm 1, our parallel solver will work with four stages: Partition, Translation, Stable Model Generation, and Synthesis. In the partition stage, an LPMLN program is partitioned into several augmented subsets such that inference tasks of the LPMLN program can be addressed via solving these augmented subsets concurrently. In the translation stage, each augmented subset is translated into an ASP program, which is an extension of the translation introduced in [13]. In the stable model generation stage, ASP programs are solved by an ASP solver, which enumerates all stable A Parallel LPMLN Solver: Primary Report 3 models and computes their penalties. In the synthesis stage, the LPMLN solver collects all stable models with penalties and computes results of inference tasks. For now, there are two kinds of inference tasks supported by our solver: MAP task and PI task. MAP task requires solver to compute the most probable stable models of the input LPMLN program. And PI task requires solver to compute the marginal probabilities of some propositions w.r.t. the input LPMLN program. From Algorithm 1, we can see that the key problems in this work are how to partition an input program in the function Partition and how to translate an augmented subset into an ASP program in the function Translation such that the MAP task and PI task can be done. Our main contributions are as follows. Firstly, we present an approach to par- tition an LPMLN program into several augmented subsets, which contains some theoretical results and a practical algorithm. Secondly, we present a translation from an augmented subset into an ASP programs, which preserves all stable models of the augmented subset, and the weight degree of a stable model in the sense of LPMLN can be derived from the penalties of a stable model in the sense of ASP. The rest of this paper is organized as follows. Section 2 reviews LPMLN and weak constraints. Section 3 presents our partition approach including the theoretic foundation of partition and the corresponding algorithm. Section 4 presents our translation approach. Section 5 shows experimental results and gives some discussion on the partition. Section 6 concludes the paper by summarizing the obtained results and future work. 2 Preliminaries 2.1 LPMLN An LPMLN program is a finite set of rules of the form w : r, where w is either a real number or the symbol α denoting 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. A 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 rules of an LPMLN program M , i.e. M = {r|w : r ∈ M }. A ground LPMLN rule w0 : r0 is obtained from its corresponding non-ground rule w : r by replacing every variable of w : r with every ground term of a signature, and the weight of rule w0 : r0 is the same as the weight of rule w : r. 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 reduct of an LPMLN program M with respect to 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 . We use SM (M ) to denote the set of 4 Bin Wang and Zhizheng Zhang 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 ! X W (M, X) = exp w (2) w:r∈MX and the probability degree Ps (M, X) of X w.r.t. M is defined as W (M, X) Ps (M, X) = lim (3) α→∞ ΣX 0 ∈SM (M ) W (M, X 0 ) For a proposition β, its probability degree Pp (M, β) w.r.t. M is defined as X Pp (M, β) = Ps (M, X) (4) X∈SM (M ) and X|=β 2.2 Weak Constraints A weak constraint has the form : ∼ l1 , . . . , ln . [weight@level] (5) where ls are literals, weight is a real number and level is an integer. Let Π be an ASP program Π1 ∪ Π2 , where Π1 is a set of rules of the form (1) and Π2 is a set of weak constraints. We call X a stable model of Π if it is a stable model of Π1 . For a stable model X of Π, the penalty of X at level l, denoted by penalty(Π, X, l), is defined as X penalty(Π, X, l) = w (6) X6|= :∼l1 ,...,ln . [w@l] For any two stable models X1 and X2 of Π, we say X1 is dominated by X2 if - there is some integer l such that penalty(Π, X2 , l) < penalty(Π, X1 , l) and - for all integers k > l, penalty(Π, X2 , k) = penalty(Π, X1 , k). A stable model of Π is optimal if it is not dominated by another stable model of Π. 3 Partition In this section, we first present the concept of augmented subset and some related definitions that are the theoretic foundation of the partition stage of the solver. Then, we present a partition algorithm. A Parallel LPMLN Solver: Primary Report 5 3.1 Augmented Subsets and Related Notations Definition 1 (Augmented Subset). For a ground LPMLN program M , an augmented subset of M is a triple tuple S = (I, SAT, U N S), where I, SAT and U N S are three pairwise disjoint subsets of M that satisfy I ∪ SAT ∪ U N S = M . For example, let w : r be a rule of a ground LPMLN program M , (M − {w : r}, ∅, {w : r}) and (M, ∅, ∅) are both augmented subsets of M . Definition 2 (Stable Models of an Augmented Subset). For an aug- mented subset S = (I, SAT, U N S) of a ground LPMLN program M , a set X of ground literals is a stable model of S iff X is a stable model of I that satisfy SAT and does not satisfy any rule in U N S. From the definition of stable models of an augmented subset, we can observe that the satisfiability of rules in set SAT and U N S are determinate, while the satisfiability of rules in set I are indeterminate. Hence, the rules in I are called indeterminate rules, and the rules in SAT and U N S are called determinate rules. By SM 0 (S), we denote all stable models of an augmented subset S of an LPMLN program M . For a set X ∈ SM 0 (S), the weight degree W 0 (S, X) of X w.r.t. S is defined as ! X W 0 (S, X) = exp w (7) w:r∈IX ∪SAT and the weight degree Wp0 (S, β) of a proposition β w.r.t. S is defined as X Wp0 (S, β) = W 0 (S, X) (8) X∈SM 0 (S) and X|=β Definition 3 (Split). For an LPMLN program M and an augmented subset S of M , a set SP = {Si | 1 ≤ i ≤ n} of augmented subsets of M is called a split of S, iff [n 0 SM (S) = SM 0 (Si ) (9) i=1 where SM 0 (Si ) ∩ SM 0 (Sj ) = ∅ for any i 6= j, and for any stable model X ∈ SM 0 (Si ) W 0 (S, X) = W 0 (Si , X) (10) where 1 ≤ i ≤ n. Suppose S1 = (I1 , SAT1 , U N S1 ) and S2 = (I2 , SAT2 , U N S2 ) are two aug- mented subsets of an LPMLN program M , and w : r is a rule in M , we say S1 and S2 are complementary on the rule w : r iff (1) I1 = I2 , and (2) SAT1 −SAT2 = {w : r}(or SAT2 −SAT1 = {w : r}). In addition, if S1 and S2 are complementary on a rule w : r, then we can define the union of two augmented subsets S1 t S2 = (I1 ∪ {w : r}, SAT1 − {w : r}, U N S1 − {w : r}). For example, suppose S1 = (M − {w : r}, ∅, {w : r}), and S2 = (M − {w : r}, {w : r}, ∅), then S1 and S2 are complementary on the rule w : r, and S1 t S2 = (M, ∅, ∅). 6 Bin Wang and Zhizheng Zhang Definition 4 (Substitute). For an LPMLN program M , a set ST of augmented subsets of M is called a substitute of an augmented subset S of M with regard to a rule w : r if ST contains only two elements S1 and S2 such that S1 and S2 are complementary on the rule w : r and S1 t S2 = S. Lemma 1. For a ground LPMLN program M and an augmented subset S of M , a substitute ST = {S1 , S2 } of S is a split of S. Proof. By the definition of split, the proof of Lemma 1 has three parts. Firstly, by the definition of substitute, it is easy to show that SM 0 (S1 ) ∩ SM 0 (S2 ) = ∅. Secondly, by the definition of substitute and stable models of augmented subsets, we can show that SM 0 (S) = SM 0 (S1 ) ∪ SM 0 (S2 ). Finally, by the definition of weight degrees of stable models w.r.t. an augmented subset, we can show that W 0 (S, X) = W 0 (S 0 , X), where S 0 ∈ {S1 , S2 } and X ∈ SM 0 (S 0 ) (the complete proofs of all lemmas and theorems can be found in the extended version of the paper 1 ). t u Lemma 2. For an LPMLN program M and the augmented subset S0 = (M, ∅, ∅) of M , stable models and their weights of S0 and M coincide, which means SM (M ) = SM 0 (S0 ) and W (M, X) = W 0 (S0 , X) for any X ∈ SM (M ). Lemma 2 can be easily proven by the definition of stable models and their weights of LPMLN programs and augmented subsets. Combining with Lemma 1, Lemma 2 provides a way to compute stable models and their weights of an LPMLN program M via computing them of augmented subsets in a split w.r.t. M , which can be done concurrently. In addition, probability degrees of a stable model and a proposition defined by Equation (3) and (4) can be restated in terms of split. For an LPMLN program M , a split SP of (M, ∅, ∅), an augmented subset Si ∈ SP , and a stable model X ∈ SM 0 (Si ), the probability degree of X w.r.t. M can be restated as follows: W 0 (Si , X) Ps (M, X) = lim P P 0 0 (11) X 0 ∈SM 0 (Sj ) W (Sj , X ) α→∞ Sj ∈SP and the probability degree of a proposition β w.r.t. M can be restated as follows: 0 P Sk ∈SP W (Sk , β) Pp (M, β) = lim P P 0 0 (12) X 0 ∈SM 0 (Sj ) W (Sj , X ) α→∞ Sj ∈SP Let us recall two inference tasks supported by our solver in the view of split. For the MAP task, by the definition of split, we can find the most probable stable models of augmented subsets in a split, then find the most probable stable models of input program among those of augmented subsets. For the PI task, we can observe that part of Equation (11) and (12) can be evaluated from an augmented subset, which can be used to simplify the computing in the Synthesis stage. Hence both MAP task and PI task of an LPMLN program can be solved concurrently in the sense of split. 1 http://cse.seu.edu.cn/PersonalPage/seu zzz/publications/parallel-lpmln-solver.pdf A Parallel LPMLN Solver: Primary Report 7 3.2 Partition Algorithm Inference tasks of an LPMLN program M can be reduced to tasks of the aug- mented subset S0 = (M, ∅, ∅), where S0 can be partitioned into a split, which laid the theoretic foundation of our parallelized method for solving the program M . In this section, we present a method to obtain a split. Definition 5 (Transformer). For an LPMLN program M , a set T of aug- mented subsets of M is called a transformer of M if there exists a finite sequence of sets of augmented subsets T 1 , T 2 , . . . , T n satisfying - T i+1 = (T i − {Sk }) ∪ STk , and - T 1 = {(M, ∅, ∅)} and T n = T . where Sk ∈ T i and STk is a substitute of Sk . Theorem 1. For an LPMLN program M , if a set T of augmented subsets of M is a transformer of M , then T is a split of the augmented subset S0 = (M, ∅, ∅). Proof. By Lemma 2 and Lemma 1, Theorem 1 can be proved by mathematical induction. t u Theorem 1 leads to a method to partition an augmented subset of an LPMLN program into a split. The process showed in Algorithm 2 is an implementation of the method. Algorithm 2: Partition Input: M : an LPMLN program, n: size of the split Output: a split SP of the augmented subset (M, ∅, ∅) 1 begin 2 SP = {(M, ∅, ∅)}; 3 while |SP | ≤ n do 4 select an augmented subset Sk ∈ SP randomly; 5 select a substitute STk of Sk randomly; 6 SP = (SP − {Sk }) ∪ STk ; 7 return SP ; 4 Translation Inspired by the translation introduced by Lee and Yang in [13], we propose a new translation from augmented subsets of an LPMLN program M to ASP programs such that stable models and associated weights of an augmented subsets can be derived from the translation. And we also follow the point of [5] by identifying logic program rules as a special case of first order formulas under the stable model semantics. Hence, an LPMLN program can be viewed as a set of weighted formulas. Here, we first review the translation given in [13]. 8 Bin Wang and Zhizheng Zhang 4.1 Lee and Yang’s Translation For an LPMLN program M , the translation τ (M ) is defined as follows. Every weighted formula w : F is translated into a choice formula “F ∨ ¬F ” and a weak constraint “:∼ F. [weight@lev]”, where weight = −1 and lev = 1 if w is α, and weight = −w and lev = 0 otherwise. It has been shown that the stable models of M are exactly the stable models of τ (M ), and the most probable stable models of M are precisely the optimal stable models of τ (M ). Although the translation is designed for solving the MAP task for an LPMLN program, it can also be used for computing the weight for a stable model. For a stable model X of τ (M ), the sum of weights of formulas satisfied by X can be derived from the penalties of X, that is sum(M, X) = penalty(τ (M ), X, 1) ∗ α + penalty(τ (M ), X, 0) (13) The sum is an intermediate result for computing weight of X in the sense of LPMLN , and the weight degree of X can be restated as follows: W (M, X) = exp(−sum(M, X)) (14) Unfortunately, Lee and Yang’s translation is not enough for our situation. For an LPMLN program M , an augmented subset S = (I, SAT, U N S) of M consists of three kinds of formulas. The formulas in I are ordinary LPMLN formulas, which can be translated by using Lee and Yang’s method, while the formulas in SAT and U N S are determinate formulas, which need to be translated by using new translating method. Our new translation extends Lee and Yang’s translation and completely captures the stable models and their penalties of augmented subsets of an LPMLN program. 4.2 New Translation For an augmented subset S = (I, SAT, U N S) of a ground LPMLN program M , the translation τ 0 (S) of S is defined as follows. Firstly, we turn each weighted formula wk : Fk in I to Fk ∨ ¬Fk . Secondly, we turn each weighted formula wk : Fk in SAT to Fk . Finally, we turn each weighted formula wk : Fk in U N S to ¬Fk . Furthermore, we use weak constraints to compute the sum of weighted for- mulas satisfied by a stable model, which is slightly different from Lee and Yang’s translation. For each weighted formula wk : Fk in I, we add the following for- mulas into our translation τ 0 (S): Fk → sat(k) (15) ¬sat(k) → ¬Fk (16) where sat(k) is a fresh atom, and if wk : Fk is a hard formula, add a weak constraint :∼ sat(k). [1@1] (17) A Parallel LPMLN Solver: Primary Report 9 and if wk : Fk is a soft formula, add a weak constraint :∼ sat(k). [wk @0] (18) Theorem 2. For any augmented subset S = (I, SAT, U N S) of a ground LPMLN program M , the set SM 0 (S) and the set of stable models of τ 0 (S) coincide on the literals of M . And for a stable model X in SM 0 (S), the weight of X can be computed by X W 0 (S, X) = exp(sum(I, X) + w) (19) w:r∈SAT Theorem 2 tells us that an augmented subset S of a ground LPMLN program M can be solved by solving its translation τ 0 (S), and the weight of a stable model X of S can be computed by computing penalties of X. And the theorem can be proved by the Proposition 1 from [13]. 5 Experiments 5.1 Test Environment and Test Cases We tested our implementation on a Dell PowerEdge R920 server with an Intel Xeon E7-4820@2.00GHz with 32 cores and 24 GB RAM running the Ubuntu 16.04 operating system. We used Clingo 4.5.4 as our back-end ASP solver, and F2LP [11] to translate first order formulas into ASP programs. We used two problems: the Monty Hall problem and the Bird problem as our test cases, where hard rules of corresponding programs are treated as determi- nately satiable rules in this paper (the source code of the experiments can be found on GitHub2 ). The Bird problem and its LPMLN program are from Exam- ple 1 in [12]. Following the description of the Monty Hall Problem from [19], we encoded it in LPMLN as below. 1. One of three boxes contains a key to a car, and the possibility of each box containing the key is the same. 1 : has key(X) ← box(X). (20) In the Monty Hall Problem with three boxes, ground rules of the rule (20) are the following three rules. The weights of all these rules are the same, which expresses the possibility degrees of all boxes containing the key are the same. Actually, the value of the weight of the rule (20) can be any real number. 1 : has key(1) ← box(1). 1 : has key(2) ← box(2). 1 : has key(3) ← box(3). 2 https://github.com/wangbiu/lpmlnmodels 10 Bin Wang and Zhizheng Zhang 2. The player selects one of boxes randomly. 1 : select(X) ← box(X). (21) 3. The host opens one of unselected boxes that does not contain the key ran- domly. 1 : open(X) ← box(X), not cannot open(X). (22) cannot open(X) ← select(X). (23) cannot open(X) ← has key(X). (24) 4. If the player changes his mind, he switches to remaining boxes randomly. 1 : switch(X) ← can switch(X). (25) can switch(X) ← box(X), not select(X), not open(X). (26) 5. The winning rules under two cases are encoded by win stay and win switch. win stay ← select(X), has key(X). (27) win switch ← switch(X), has key(X). (28) 6. Finally, we encode that there are three boxes, and we can increase the number of boxes. box(1). box(2). box(3). . . . Additionally, there are some underlying restrictions: (a) the player can select only one box, (b) the host can open only one box too, (c) only one of those boxes contains the key, and (d) the player can switch his choice only once. These restrictions are encoded by following definite rules. ¬select(Y ) ← select(X), box(Y ), X 6= Y. (29) ← box(X), not select(X), not ¬select(X). (30) ¬open(Y ) ← open(X), box(Y ), X 6= Y. (31) ← box(X), not open(X), not ¬open(X). (32) ¬has key(Y ) ← has key(X), box(Y ), X 6= Y. (33) ← box(X), not has key(X), not ¬has key(X). (34) ¬switch(Y ) ← switch(X), can switch(Y ), X 6= Y. (35) ← can switch(X), not switch(X), not ¬switch(X). (36) In both problems, we can increase the number of the boxes or the birds to increase the size of problems. By montyN and birdN , we denote the Monty Hall problem with N boxes and the Bird problem with N birds, respectively. In our experiments, MAP task is to output all most probable stable models, and PI task is to output all literals and their probabilities. And the programs are grounded manually due to the lack of LPMLN grounder. A Parallel LPMLN Solver: Primary Report 11 5.2 Test Results In our experiments, each running time was the average of five tests. Firstly, we tested our implementation in a non-parallel mode. Table 1 shows that ASP solver accounts for most of the running time in solving an LPMLN program, and the running times of solving the problems increase as the sizes of the problems increase. Table 1. Running Time (seconds) in non-parallel mode (a) the Monty Hall problem (b) the Bird problem MAP PI MAP PI M M clingo total clingo total clingo total clingo total monty3 0.01 0.05 0.02 0.04 bird4 0.01 0.02 0.01 0.01 monty10 0.14 0.22 0.18 0.26 bird8 0.04 0.09 0.07 0.10 monty20 2.33 2.59 2.30 2.78 bird10 0.42 0.46 0.40 0.57 monty30 17.63 18.28 16.97 18.04 bird12 4.30 4.53 4.03 4.96 monty40 76.19 77.54 77.00 79.87 bird14 53.08 57.42 48.76 59.65 Secondly, we tested our implementation in a parallel mode. Figure 1 shows that running times of solving the bird14 problem are on the decline with an increase of the number of processors used, while running times of solving the monty40 problem shows an obvious fluctuation. But we can find that the general trend appears to be decrease. M A P ta s k M A P ta s k R u n n in g T im e (s e c o n d s ) 7 0 R u n n in g T im e (s e c o n d s ) 8 0 P I ta s k P I ta s k 6 0 7 0 5 0 6 0 4 0 5 0 3 0 0 5 1 0 1 5 2 0 2 5 3 0 3 5 0 5 1 0 1 5 2 0 2 5 3 0 3 5 n u m b e r o f p ro c e sso rs n u m b e r o f p ro c e sso rs (a) program monty40 (b) program bird14 Fig. 1. Running Time vs. number of processors used Finally, we tested our parallel solver by adding some heuristic information. In our experiments, we tried to avoid contradictions in an augmented subset and keep every augmented subset containing the same numbers of indeterminate rules. For example, rules ”0 : a” and ”0 : ¬a” are contradictory, hence, we do not put both of them in the set of determinately satiable rules of an augmented subset. For the Monty Hall problem, rules of the form (30), (32), (34), (36) and other corresponding rules may lead to contradictions. We can see from Figure 2 that running times of both programs show a more steady improvement with the increase of processors used. 12 Bin Wang and Zhizheng Zhang 9 0 M A P ta s k M A P ta s k 6 0 R u n n in g T im e (s e c o n d s ) R u n n in g T im e (s e c o n d s ) 8 0 P I ta s k P I ta s k 7 0 5 0 6 0 5 0 4 0 4 0 3 0 2 0 3 0 0 5 1 0 1 5 2 0 2 5 3 0 3 5 0 5 1 0 1 5 2 0 2 5 3 0 3 5 n u m b e r o f p ro c e sso rs n u m b e r o f p ro c e sso rs (a) program monty40 (b) program bird14 Fig. 2. Running Time vs. number of processors used (heuristic partition) 5.3 Discussion Our data suggests that solving a split of an LPMLN program can improve the efficiency of solving the LPMLN program. The results in Table 1 illustrate that the more indeterminate rules an LPMLN program contains, the harder solving the program will be. Hence, by decreasing numbers of indeterminate rules of an augmented subset, our parallel solver can make an augmented subset more easy to solve. The results in Figure 2 and Figure 1 also illustrate that the partition method in our parallel solver is specially important for the parallelized solving, and the random partition method used in the paper is not a good choice. A possible reason is that Algorithm 2 cannot always generate a balanced split w.r.t. an input program. A balanced split w.r.t. an LPMLN program means every augmented subset of the split is solved by taking approximately the same length of time. For now, the partition method to generate a balanced split still remains unclear, hence, it is worthy to find such a method. 6 Conclusion and Future Work We implemented a parallel LPMLN solver, which computes the stable models as well as their weights in a parallel way. And we presented some theoretic discus- sion on the implementation containing the partition method and the translation method. Experimental results show that our parallelized method can improve performance of the LPMLN solver. Besides, we made a preliminary attempt on how different partition methods influence our parallelized solving. Experimental results show that the partition method using some heuristic information is better than the stochastic method on our two test cases. For the future, we plan to make an elaborative investigation on heuristic partition methods to make our parallel solver faster. And we also plan to test our solver further by modeling with LPMLN in more real-world applications. A Parallel LPMLN Solver: Primary Report 13 7 Acknowledgments We are grateful to the anonymous referees for their useful comments. This work was supported by the National High Technology Research and Development Program of China (Grant No.2015AA015406), the National Science Founda- tion of China (Grant No.60803061), the National Science Foundation of China (Grant No.61272378), and the Natural Science Foundation of Jiangsu (Grant No.BK2008293). References 1. Balai, E., Gelfond, M.: On the Relationship between P-log and LPMLN . In: Proceedings of the 25th International Joint Conference on Artificial Intelligence. (2016) 915–921 2. Baral, C., Gelfond, M., Rushton, N.: Probabilistic reasoning with answer sets. Theory and Practice of Logic Programming 9(1) (2009) 57–144 3. Calimeri, F., Faber, W., Gebser, M., Ianni, G., Kaminski, R., Krennwallner, T., Leone, N., Ricca, F., Schaub, T.: ASP-Core-2 Input language format. (2012) 4. De Raedt, L., Kimmig, A., Toivonen, H.: ProbLog: A probabilistic prolog and its application in link discovery. In: Proceedings of the 20th International Joint Conference on Artificial Intelligence. Volume 7. (2007) 2468–2473 5. Ferraris, P., Lee, J., Lifschitz, V.: Stable models and circumscription. Artificial Intelligence 175(1) (2010) 236–263 6. Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: CLASP: A Conflict-Driven Answer Set Solver. In: Logic Programming and Nonmonotonic Reasoning. (2007) 260–265 7. Gelfond, M., Lifschitz, V.: The Stable Model Semantics for Logic Programming. In: Logic Programming, Proceedings of the Fifth International Conference and Symposium. (1988) 1070–1080 8. Kok, S., Sumner, M., Richardson, M., Singla, P., Poon, H., Lowd, D., Wang, J., Domingos, P.: The Alchemy System for Statistical Relational AI. Technical re- port, Department of Computer Science and Engineering, University of Washington, Seattle, WA. (2009) 9. Lee, J., Lifschitz, V.: Loop Formulas for Disjunctive Logic Programs. In: Logic Programming, 19th International Conference. (2003) 451–465 10. Lee, J., Meng, Y., Wang, Y.: Markov logic style weighted rules under the stable model semantics. In: Proceedings of the Technical Communications of the 31st International Conference on Logic Programming. (2015) 11. Lee, J., Palla, R.: System f2lp Computing Answer Sets of First-Order Formulas. In: Logic Programming and Nonmonotonic Reasoning: 10th International Conference, LPNMR 2009, Potsdam, Germany, September 14-18, 2009. Proceedings. Springer Berlin Heidelberg (2009) 515–521 12. Lee, J., Wang, Y.: Weighted Rules under the Stable Model Semantics. In: Prin- ciples of Knowledge Representation and Reasoning: Proceedings of the Fifteenth International Conference, KR 2016, AAAI Press (2016) 145–154 13. Lee, J., Yang, Z.: LPMLN , Weak Constraints, and P-log. In: Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence. (2017) 14 Bin Wang and Zhizheng Zhang 14. Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., Scarcello, F.: The DLV system for knowledge representation and reasoning. Acm Transactions on Computational Logic 7(3) (2006) 499–562 15. Lin, F., Zhao, Y.: ASSAT: Computing answer sets of a logic program by SAT solvers. Artificial Intelligence 157(1-2) (2004) 115–137 16. Niu, F., Ré, C., Doan, A., Shavlik, J.: Tuffy: Scaling up Statistical Inference in Markov Logic Networks using an RDBMS. Proceedings of the VLDB Endowment 4(6) (2011) 373–384 17. Pearl, J.: Causality: Models, reasoning, and inference. 29 (2000) 18. Richardson, M., Domingos, P.M.: Markov logic networks. Machine learning 62(1-2) (2006) 107–136 19. Selvin, S.: A problem in probability (letter to the editor). The American Statisti- cian 29(1) (1975) 67