=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== https://ceur-ws.org/Vol-1868/p5.pdf
     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