Answer Set Programming (ASP) is a logic programming language widely used in non monotonic automated reasoning. Thanks to its popularity, in the last years there has been a great interest towards the developing of e cient solvers, required to deal with complex problems, like planning and NP problem solving. These solvers can be unable to deal with programs that are \grounded" on huge amount of data, possibly resident in di erent sites. To address this problem, in this paper we present a distributed approach to ASP problems, which involves all the phases of the overall solving process: from a distributed grounder (which can also be used as a solver for strati ed programs) to two different techniques to deal with the pure solving phase (for non-strati ed program too), both of them using the non-standard graph coloring algorithm to characterize answer sets. We show three proposals for solving the issue, two of them developed with the high-level framework Apache Spark, while the the third one is a C++ direct implementation of the rst one.
The Answer Set Programming (ASP) language has become very popular in the
last years thanks to the availability of more and more e cient solvers (e.g.,
Clingo [
To address this problem, we present in this paper our working project in this direction, namely three distributed tools that exploit the shared resources of a distributed system to deal with such programs, thus overcoming the limitation of a single machine.
In chronological order, the rst tool is a solver called mASPreduce [
The paper is organized as follows. In Section 2 we explain the Graph Coloring Algorithm for solving, implemented in di erent ways by both mASPreduce and DASC. From Section 3 to 5 we present the three tools. Some experimental results and comparison between them are reported in Section 6. The reader can nd our conclusions in Section 7. 2
We brie y present the Coloring Algorithm for computation of answer sets [
A labeled graph is a pair (G; `) where G = (V; E) is a directed graph and ` : E ! L is a map from edges to a set of labels L = f0; 1g (intuitively 0 will represent a positive dependency and 1 a negative dependency). (G; `) can be represented by the triple (V; E0; E1), where Ei = fe 2 E j `(e) = ig for i = 0; 1. Given a labeled graph G = (V; E0; E1), an i{subgraph of G for i = 0; 1 is a subgraph of the graph Gi = (V; Ei)|i.e. a graph G0 = (W; F ) s.t. W V , and F Ei \ (W 2). If x; y 2 V , an i{path is a path from x to y in the graph Gi.
Let be a ground logic program; its rule dependency graph (RDG) = ( ; E0; E1) is the labeled graph where nodes are the (number of) program rules and
E0 = f(r; r0) j r; r0 2 E1 = f(r; r0) j r; r0 2 ; head(r) 2 body+(r0)g ; head(r) 2 body (r0)g A (partial/total) coloring of is a partial/total map C : ! f ; g, where and are two colors. We will denote C = fr j r 2 ; C(r) = g and C = fr j r 2 ; C(r) = g, and a (partial) coloring as (C ; C ). Let us de ne with C the set of all (partial) colorings, and de ne a partial order over C as follows: let C; C0 be partial coloring of . We say that C v C0 i C C0 and C C0 . The empty coloring (;; ;) is the bottom of the partial order C . Colors represent enabling ( ) and disabling ( ) of rules. Intuitively, we are interested in nding all possible subsets of generating rules, leading us to all the possible answer sets of a logic program.
De nition 1 (Generating Rules of an answer set). Given a set of atoms X from a program , the set R (X) of generating rules is given by R (X) = fr 2 j body+(r)
X; body (r) \ X = ;g:
Let be a logic program, and let be the corresponding RDG. We
dene the notion of admissible coloring as follows: if X 2 AS( ), then C =
(R (X); n R (X)) is an admissible coloring of (i.e., all the rules
satis ed by X are colored positively, and the other rules negatively). Moreover,
head(C ) = X [
By de nition, admissible colorings are total and one-to-one with answer sets.
As shown in [
Let be a program and C a coloring of : = ( ; E0; E1). For r 2 { r is supported in ( ; C), if body+(r) fhead(r0) j (r0; r) 2 E0; r0 2 C g; { r is unsupported in ( ; C), if there is q 2 body+(r) s.t. fr0 j (r0; r) 2
E0; head(r0) = qg C ; { r is blocked in ( ; C), if there exists r0 2 C s.t. (r0; r) 2 E1; { r is unblocked in ( ; C), if r0 2 C for all (r0; r) 2 E1.
We also de ne the sets of supported S( ; C), unsupported S( ; C), blocked B( ; C), and unblocked B( ; C) rules. By de nition, S( ; C) \ S( ; C) = ; and B( ; C)\B( ; C) = ;. With C total coloring, a rule is unsupported or unblocked i it is not supported or blocked, respectively. This is not true, in general, for partial colorings.
The above de ned notions can be used to de ne an operational semantics to
compute the stable models of a logic program. We will only give an overview of
the characterization implemented in our solver. For a deeper analysis of several
other operational characterizations, we refer the reader to [
Let be the RDG of a logic program and C be a partial coloring of . The coloring operator D : C ! C, where 2 f ; g, is de ned as follows: 1. D 2. D = (C [ frg; C ) for some r 2 S( ; C) n (C = (C ; C [ frg) for some r 2 S( ; C) n (C [ C ); [ C ).
Operator D will be used to encode a branching path in the visit of the coloring tree, in fact, representing a non-deterministic choice (restricting our choice to the supported rules). Since support is a local property of a node (it only depends on information coming from the neighborhood), the coloring operator can be e ciently applied.
Let be the RDG of a logic program and C be a (partial) coloring of . Let us de ne the operators P ; T ; V : C ! C as follows
P (C) = (C T (C) = (C V (C) = (C ; [ (S( ; C) \ B( ; C)); C [ (S( ; C) n C ); C ) n V ) [ (S( ; C) [ B( ; C))) where V = T (C ) and T (C) is the v-smallest coloring containing C and closed under T . A coloring C is closed under the operator op if C = op(C). Finally, let (PV) (C) be the v-smallest coloring containing C and being closed under P and V .
Theorem 21 (Operational Answer Set Characterization, III) Let be the RDG of a logic program and let C be a total coloring . Then, C is an admissible coloring of i there exists a coloring sequence C0; C1; : : : ; Cn such that: (1) C0 = (PV) ((;; ;)), (2) Ci+1 = (PV) (D (Ci)) for some 2 f ; g and 0 i < n, (3) Cn = C.
Given an admissible coloring C (point 3), head(C ) returns its corresponding
answer set. The proof of the above theorem can be found in [
The mASPreduce solver is based on the MapReduce distributed programming
paradigm rst introduced in [
A bare-bones implementation of MapReduce works on a generic collection of homogeneus data, and provides a basic interface consisting of two methods: 1. map( ) that maps a function over a collection of objects. It outputs a collection of \key-value" tuples; 2. reduce( ) that takes as input a collection of key-value pairs and merges the values of all entries with the same key. The merging operation is user-de ned. The user de nes a MapReduce program as a sequence of map/reduce calls; modern implementations provide additional operators usually built on top of the primitives map/reduce (e.g., lters, xpoints).
We used Apache Spark as a state-of-the-art in-memory MapReduce
framework to implement the solver [
As a further astraction over MapReduce, Spark o ers two di erent families of high-level operators: 1. transformations, which create a new dataset from an existing one; 2. actions, which aggregate elements of a RDD with a custom function and return a single results to the caller.
In this case, map is a simple example of transformation because it executes a user-de ned function on each node and returns a new RDD; reduce is an action that aggregates all the elements of the RDD using the provided function. Transformations are lazily executed, in that they do not compute their results until an action needs to be executed.
We implemented the rule dependency graph and the graph coloring algorithm
for the computation of answer sets using the GraphX module [
Apart from giving access to a complete distributed graph implementation,
GraphX also provides a Pregel API [
The software is written in Scala and the RDG of a logic program is implemented as a subclass of Graph[VD,ED], GraphX built-in class that gives access to the property graph. The original Graph[VD,ED] class is parametrized over vertex and edge property labels (VD and ED respectively). In the case of the RDG class, nodes keep track of rules and edges keep track of support and blockage relations between rules. RDG is in turn enclosed in a wrapper class which keeps track of the atom table (provided by the grounder) and the answer sets computed so far.
As described before, the RDG coloring process alternates between two phases: 1. Non-deterministic coloring : it is basically encoded as a visit over the colorings tree. Di erent heuristics will change the way we visit the tree, achieving better performances on di erent programs; 2. Deterministic coloring : deterministic propagation of the colors to avoid a blind visit of the colorings tree.
The main recursive procedure encodes the non-deterministic search and the backpropagation process to compute all possible answer sets. At any time, it goes through the vertices and (randomly) choose an uncolored supported rule. If none exists, we reached an admissible total coloring and we can build the corresponding answer set. In case an uncolored supported rule r exists, the computation branches. In the rst case, r is colored with and the color is deterministically propagated; nally, the function calls itself on the new graph. The second case is similar, but r is colored with .
Deterministic and non-deterministic operators are implemented as map/reduce routines, while xpoint operators are implemented using Pregel. 4
Strati ed programs re ect the following intuition: at the point of the inference process where a rule is used, each negative reference should regard only atoms such that a complete information about their foundedness is available. This entails that a program is strati ed if and only if it is possible to de ne an ordering on the evaluation of the rules such that whenever we encounter a naf literal its membership to the answer set is already determined.
The stable model is unique and can be obtained by iterating minimum
xpoint procedures at each strata [
[
The DASC solver has been developed with the purpose of improving the poor performance and scaling of mASPreduce, caused by the limitation of the highlevel framework Spark (as witnessed by the results on strati ed programs explained in the next section). To reach this goal, we opted for a C++ implementation, with the help of the Parallel Boost Graph Library (brie y, PBGL) for the distributed graph data structure, and the boost MPI library for the communication stage. Thanks to the latter, we have complete control over the messages sent on the network and the synchronization between the di erent computational nodes. Since the bad scaling of mASPreduce resides on the communication stage, our optimization starts from that.
The way PBGL distributes the graph is pretty straightforward: vertices are divided between the computational nodes in Round Robin way, stored in a node list, and each unit keeps track of the edges connected to its local vertices with adjacency lists. Vertex properties are stored in a property map. 5.1
Design choices The rst and most visible change with respect to mASPreduce is a modi cation of the RDG structure, which has two noticeable e ects: it is more suitable to address the notif y change implementation of propagation, explained in the next subsection, and it potentially reduces the number of edges of an unbound number, at the cost of doubling up the nodes. From now on, we refer to such a graph as RDG'.
De nition 2 (New Rule Dependency Graph: RDG'). Given a logic program we de ne the RDG' as the graph (V; E0; E1; E2) where { V = [ atoms( ) { E0 = f(a; r) j a 2 atoms( ) ^ r 2 ; a 2 body+(r)g { E1 = f(a; r) j a 2 atoms( ) ^ r 2 ; a 2 body (r)g { E2 = f(r; a) j r 2 ^ a 2 atoms( ); head(r) = ag
The reason why this graph is more suitable to our algorithm is that we rely only on information local to a node to decide whether the latter is supported or blocked.
For instance, a rule r is blocked if we are sure that in the actual coloring an atom a belonging to body (r) does not belong to the answer set, i.e, for all rules r0 such that a = head(r0), then r0 2 C . To perform this check without forcing r to query all its neighbors, we could use a counter for each atom in body (r) to keep count of how many r0 were disabled. Since it is not a good idea to keep variable size data structures inside a node, we opted to use atom nodes, each one with its own single counter.
The other reason to choose this RDG structure is that it can strongly decrease the number of edges, which is a very good point in a distributed graph: fewer edges between di erent computational nodes, less amount of communication.
To address performance and reduce communication, a completely di erent strategy was developed in DASC to implement the propagation operators.
MapReduce paradigm has a big downside when dealing with a distributed system. Querying a neighbor stored in another computational node is a very expensive operation, and this situation always happens, even if the considered vertex would never be touched by the actual propagation. We refer to nodes connected to other computational units as border nodes; since MapReduce relies g 6
on the fact that each node queries all of its neighbors, this implies that also in the case of a local propagation, which theoretically does not need to send any message on the network, edges connected to border nodes are crossed, causing useless tra c inside the cluster.
To x the problem, the idea is to develop an algorithm in which only the nodes really a ected by the actual propagation (plus their neighbors) are touched: we will refer to this implementation as notif y change algorithm, since it will be duty of an a ected node to notify its neighbors of an eventual change in its coloring state, and not the opposite. The reader can nd the pseudocode in Figure 1. v o i d n o t i f y c h a n g e ( node v ) f //v i s e v e n t u a l l y c o l o r e d by p r o p a g a t i o n o p e r a t o r s i f ( v has j u s t been c o l o r e d ) then
n o t i f y c h a n g e ( u ) f o r a l l u such t h a t t h e r e i s a edge ( v , u ) ; e l s e
r e t u r n ; In Figure 2 the reader can nd a quick comparison between DASC and mASPreduce. Each DASC test is executed with all possible combinations of distribution options.
STRASP solver supports both the maximal strati ed subprogram and the fully strati ed program resolution; moreover, we implemented a rst naive form of distributed grounding, by exploiting the component and rule level parallelism in order to distribute among the available nodes the computation and resolution of the ground predicates.
STRASP performance as solver for strati ed programs can be seen in Figure 3. We tested it by using the same logic (strati ed) program, where the base stratum is composed of predicates such as a(1..20).. The upper strata de ne predicates with rules referring to the lower strata with combinations leading to an exponentially large grounding. Each test instance is obtained from the previous by increasing (+10%) the ranges of the base stratum. The comparison with Clingo shows that the two time series have similar trends, diverging only by a constant factor; unfortunately this constant is too large.
Although the shape of the graph of the running times with this approach is the same w.r.t. Clingo on the same strati ed programs, the di erence in terms of constants showed that the approach is still unfeasible. E ciency is probably lost in the various abstraction levels that separates Apache users from the machine.
Since strati ed programs can be fully evaluated at grounding time, the computation of the maximal strati ed subprogram can be used as a starting point for a more general distributed grounding, by rst grounding and solving the maximal strati ed subprogram with the distributed procedure implemented in STRASP, and then considering the non deterministic part of the program. 1 2 3 4 5 6 7
RD RR RD RR RD RR RD RR RD RR RD
NR 0.36 NR 1N.R83 SE 7N.R03 to 2N1R.99 to 5N8R.90 to
DASC MR Since this project started with mASPreduce, we made some steps forward in building a tool capable of exploiting distributed systems resources in order to manage huge size programs. Yet, we are still far from achieve the goal of large problems handling, and a lot of work has to be done to make our tools competitive with state-of-the-art solvers. Heuristics implementation and a variant of clause learning would probably be the main task to perform in order to closing the gap with them. At that point, DASC could be used to handle ground programs too big for single machine solvers.
In order to handle the overall solving process, STRASP is a good starting point for the grounding phase, even if performance are averagely 1000 time slower then Clingo in strati ed programs. This gap is probably due to Spark ine ciency, ) s d n o c e s ( e m i T 2;000 1;000
0 5
Test 1 3 7 9 1 3
5
7 9 so we expect much better results with a direct implementation, how it happened between mASPreduce and DASC. However, STRASP performance can still be improved by implementing the last level (Single rule level) of parallelism, in order to handle huge programs.