In this paper we report on the first attempts to customize and exploit in DLV, a state-of-the-art Answer Set Programming system, both novel and existing parallelization methods for the propositional search phase. These techniques, combined with the recently proposed strategies for parallel instantiation, will pave the way for obtaining a fully parallel DLV system. The results of an experimental analysis are also reported, showing the impact of parallel techniques on the performance of the DLV system.
Answer Set Programming (ASP) [
The idea of answer set programming is to represent a given
computational problem by a logic program the answer sets of which correspond to
solutions, and then, use an answer set solver to find such solutions [
However, the development of efficient ASP systems [
At the time of this writing, the majority of the available ASP implementations is not able to take advantage during all the steps of the computation from the latest hardware, featuring multi-core/multi-processor SMP (Symmetric MultiProcessing) technologies also for entry-level systems and PCs.
In particular, concerning the DLV system, a first step in this direction
has been recently done by applying parallelism to the preliminary program
instantiation phase [
In this paper we report on the first attempts to customize and exploit in
DLV both novel and existing parallelization methods for the propositional
search phase in order to obtain a fully parallel version of the DLV system.
We start by focusing on the computation of a single answer set, and try to
combine well-known parallel lookahead techniques [
The results of an experimental analysis are also presented, showing the impact of parallel techniques on the performance of the DLV system. 2
In this Section, first we provide a short description of the syntax and the
semantics of the kernel language of DLV which is disjunctive datalog under
the answer sets semantics [
Syntax. A variable or a constant is a term. An atom is a(t1, . . . , tn), where a is a predicate of arity n and t1, . . . , tn are terms. A literal is either a positive literal p or a negative literal not p, where p is an atom. Given a literal L, we define its complementary literal not .L as follows: not .L = p if L is of the form not p, otherwise not .L = not p.
A disjunctive rule (rule, for short) r is a formula a1 ∨ · · · ∨ an :– b1, · · · , bk, not bk+1, · · · , not bm. where a1, · · · , an, b1, · · · , bm are atoms and n ≥ 0, m ≥ k ≥ 0. The disjunction a1 ∨ · · · ∨ an is the head of r, while the conjunction b1, ..., bk, not bk+1, ..., not bm is the body of r. A rule without head literals (i.e. n = 0) is usually referred to as an integrity constraint. If the body is empty (i.e. k = m = 0), it is called a fact.
An ASP program P is a finite set of safe rules. An atom, a literal, a rule, or a program is ground if no variables appear in it.
Semantics. Let P be a program. The Herbrand Universe and the Herbrand Base of P are defined in the standard way and denoted by UP and BP , respectively.
1Actually, some studies on parallel instantiation were carried out in [
Given a rule r occurring in P, a ground instance of r is a rule obtained from r by replacing every variable X in r by σ(X), where σ is a substitution mapping the variables occurring in r to constants in UP ; ground(P) denotes the set of all the ground instances of the rules occurring in P. An interpretation for P is a set of ground atoms, that is, an interpretation is a subset I of BP . A ground positive literal p is true (resp., false) w.r.t. I if p ∈ I (resp., p 6∈ I). A ground negative literal not p is true w.r.t. I if p is false w.r.t. I; otherwise not p is false w.r.t. I. Let r be a ground rule in ground(P). The head of r is true w.r.t. I if H(r) ∩ I 6= ∅. The body of r is true w.r.t. I if all body literals of r are true w.r.t. I (i.e., B+(r) ⊆ I and B−(r) ∩ I = ∅) and is false w.r.t. I otherwise. The rule r is satisfied (or true) w.r.t. I if its head is true w.r.t. I or its body is false w.r.t. I.
A model for P is an interpretation M for P such that every rule r ∈ ground(P) is true w.r.t. M . A model M for P is minimal if no model N for P exists such that N is a proper subset of M . The set of all minimal models for P is denoted by MM(P).
Given a ground program P and an interpretation I, the reduct of P w.r.t.
I is the subset PI of P, which is obtained from P by deleting rules in which
a body literal is false w.r.t. I. Note that the above definition of reduct,
proposed in [
Let I be an interpretation for a program P. I is an answer set (or stable
model) for P if I ∈ MM(PI ) (i.e., I is a minimal model for the program PI )
[
Upon startup, the input specified by the user is parsed and transformed into the internal data structures of the system. In general, an input program P contains variables, and the first step of the DLV computation, performed by the Instantiator module, is to eliminate these variables, generating a bool ModelGenerator ( Interpretation& I ) {
I = Propagate ( I ); if ( I == L ) return false; (* inconsistency *) if ( “no atom is undefined in I” )
return IsAnswerSet(I); Literal L; if ( ! Select(I, L) ) return False; if ( MG ( I ∪ {L} ) return True; else return MG ( I ∪ {not .L} ); }; ground instantiation ground(P) of P. This process, called instantiation (or grounding), is much more than a simple variables-elimination; it allows to evaluate relevant programs fragments, and produces a ground program which has precisely the same answer sets as the theoretical instantiation, but it is sensibly smaller in size. Moreover, if the input program is disjunctionfree and stratified, then its evaluation is completely done by the instantiator which computes the single answer set.
The subsequent computations, which constitute the non-deterministic
part of the DLV system, are then performed on ground(P) by both the
Model Generator and the Model Checker. Roughly, the former produces
some “candidate” answer set, whose stability is subsequently verified by the
latter. The computation performed by the Model Generator exploits a
backtracking search algorithm, which works directly on the ground instantiation
of the input program. When the Model Generator produces an answer set
candidate, the Model Checker verifies whether it is an answer set for the
input program. Note that, the task performed by the Model Checker is
as hard as the problem solved by the Model Generator for disjunctive
programs, while it is trivial for non-disjunctive programs. However, there is
also a class of disjunctive programs, called Head-Cycle-Free programs [
The computation performed by the Model Generator, is outlined in Figure 2.
Note that the description here is quite simplified, since the details of the
actual implementation are not important for this paper. For instance, the
algorithm presented here decides whether an answer set exists, but it can
be straightforwardly extended to compute all or a fixed number of answer
sets as the DLV system does. A more detailed description can be found in
[
The ModelGenerator function is first called with parameter I set to the
empty interpretation. If the program P has an answer set, then the function
returns true setting I to the computed answer set; otherwise it returns false.
The Model Generator is similar to the Davis-Putnam procedure employed by
SAT solvers. It first calls a function Propagate, which returns the extension
of I with the literals that can be deterministically inferred (or the set of all
literals L upon inconsistency). This function is similar to a unit propagation
procedure employed by SAT solvers, but exploits the peculiarities of ASP for
making further inferences (e.g., it exploits the knowledge that every answer
set is a minimal model). If Propagate does not detect any inconsistency,
an undefined2 literal L is selected according to a heuristic criterion (by
a call to the Select procedure) and ModelGenerator is called on I ∪ {L}
and on I ∪ {not .L}. The literal L corresponds to a branching variable in
SAT solvers. And indeed, like for SAT solvers, the selection of a “good”
literal L is crucial for the performance of an ASP system. To this end
DLV employes look-ahead heuristics [
Looking ahead is a comparatively costly operation, the computation of
this kind of heuristics can be very expensive, since the number of literals
to be “looked-ahead” may be very large; thus, the lookahead step is a good
candidate for exploiting parallelism [
In this Section we present the first attempts to exploit parallelism in the Model Generator. In this preliminary work, we focus on the computation of a single answer set and we investigate two directions: first, we act on the evaluation of the heuristically best literal, by making use of techniques of parallel look-ahead; then we exploit a multi-heuristics parallel search strategy taking advantage of different heuristic criteria.
2The interpretations built during the computation are 3-valued, that is a literal can be true, false or undefined (if its value has not been set yet) w.r.t. to an interpretation I. 3.1
We now sketch a framework which exploits parallelism for the selection of branching literals, according to a heuristic criterion.
The general procedure evaluating the heuristically best literal is shown in Figure 3. Roughly, some threads are spawned which run function Lookahead (calls to pthread create). Each thread takes a different undefined literal A to perform a look-ahead step by considering first I ∪ {A} and then I ∪ {not .A}. Lookahead, either calculates the two heuristic values (results are stored in IA+ and IA−) by calling function Propagate, or if an inconsistency is encountered (IA+ = L or IA− = L), stores the complement of the propagated literal in the detChoices set. Once all threads have terminated (they reach the barrier), literals in detChoices, which can be deterministically assumed, are propagated. If an inconsistency arises at this point, then no literal can be chosen at this level (the assumption of both A and its complement not .A leads to inconsistency) and the function Select returns false, in order to cause a backtracking.3 Otherwise, the best literal according to a given heuristic criterion hC is selected among the candidate ones. 3.2
The heuristics for the selection of the branching literal dramatically affects the performance of an ASP system; and, obviously, there is no heuristics performing well in all cases, rather a heuristics can be more suitable than another one for a given problem typology, or even for a specific problem instance. In order to obtain an ASP solver which is able to always adopt the best known heuristics, we exploit a multi-heuristics strategy. More in detail, we run a number of Model Generator instances, each one adopting a different branching criterion. Since we are interested in looking for just one answer set, such a strategy corresponds to exploring different paths in the search space, concurrently. The computation stops when the first instance of Model Generator terminates, thus ensuring the best possible performance for the given problem instance.
In the following we briefly recall the exploited heuristic criteria. For fast
prototyping, we considered the ones already supported by the DLV system.
Further details can be found in [
Heuristic hsatz. This is an extension of the branching rule adopted
in the system SATZ [
Interpretation IA+, IA−; ListOfThreadsID thList = ∅; ThreadSafeSetOfLiterals DetChoices = ∅; foreach Literal A undefined w.r.t. I do
ThreadID id; pthread create(id, Lookahead, I, A, detChoices); th list.add(id); foreach ThreadID thread ∈ thList do
pthread join(thread); I = Propagate(I ∪ detChoices); if (I == L) return false; L = N U LL; foreach Literal A undefined w.r.t. I do if (L == N U LL)
L = A; else if (L <hC A)
L = A; return true; } } (* spawn lookahead threads *) (* barrier *) (* assume literals that can be deterministically propagated *) (* compute the heuristically best literal *) (* first literal, no comparison *) (* compare A against L w.r.t. the heuristics *) IA+ = Propagate(I ∪ {A}); if (IA+ == L)
detChoices.add(not .A); IA− := Propagate(I ∪ {not .A}); if (IA− == L) detChoices.add(A); (* look-ahead for A *) (* look-ahead for not .A *) void Lookahead( Interpretation I, Literal A, ThreadSafeSetOfLiterals& detChoices) { and stronger constraints on the interpretation so that a contradiction can be found earlier.
Heuristic hstd. This is the heuristics used as default in the DLV system.
It is based on a peculiar property of answer sets, the supportdness: for each
true atom A of an answer set I, there exists a rule r of the program such
that the body of r is true w.r.t. I and A is the only true atom in the head
of r [
In this Section we report the results of an experimental analysis carried out on a prototypical version of the DLV system exploiting the above described techniques. Parallelism is introduced in the system by exploiting the POSIX pthreads standard libraries. 4.1
We considered three well-known problems which are usually exploited for
evaluating Model Generator performances:
- 3SAT is a special case of SAT, one of the best researched problems
in AI, which amounts to verify if it exists a truth assignment which
satisfies a CNF formula having at most tree variables per clause. The
instances for 3SAT were randomly generated by using a tool by Selman
and Kautz [
For STRATCOMP, we randomly generated 20 instances for each problem size n, with n companies and n products.
The first two benchmarks (3SAT and HAMPATH) are well-known NPcomplete problems, while the third (STRATCOMP) is a Σ2P -complete problem. 4.2
The machine used for the experiments is a multi-processor Intel Xeon “Woodcrest” (quad core) 3GHz machine with 4MB of L2 Cache and 4GB of RAM, running Debian GNU Linux 4.0.
We have allowed at most 600 seconds (ten minutes) of execution time for each instance. The experimentation has been stopped (for each system) at the size at which some instance exceeded this time limit.
The results of our experiments are displayed in the graphs of Figure 4. For each problem domain we report two graphs, describing the behavior of the two tested parallel techniques: In both graphs the horizontal axis reports a parameter representing the size of the instance, while on the vertical axis we report the running time (expressed in seconds) averaged over the instances of the same size we have run.
Since our techniques focus on model generation, all the results of the experimental analysis refer only to the process of computing answer sets of ground programs.
Evaluation of Parallel Lookahead. In order to assess the impact of the
parallel lookahead we considered a number of variants of the same prototype:
• dl.X.satz DLV with lookahead exploiting hsatz and X = [
The results shown in Figure 4(a), in Figure 4(c) and in Figure 4(e) report the performance of those variants on the considered instances of 3SAT, HAMPATH and STRATCOMP, respectively.
Concerning 3SAT, the best heuristics is clearly hsatz, the entire group of dl.X.satz performed better than dl.X.std group, solving all the generated instances in less time; whereas all the dl.X.std were stopped when considering instances having more than 300 variables. Moreover, it can be noted that dl.2.satz is the absolute best variant in this domain, and dl.2.std is the best among the ones exploiting hstd. The lower performance of variants with three workers4 is due to the larger amount of time spent by threads in synchronization (perhaps a technological problem of our prototype that can be probably overcome by improving the implementation).
As far as HAMPATH is concerned, the results are clearly in favor of
the group exploiting the standard heuristics. Here the standard heuristics,
which takes into account peculiar properties of ASP programs, has an edge
on the sat-based one. Indeed, all the dl.X.satz variants were stopped before
reaching 100 nodes, while the best versions equipped with standard
heuristics could solve instances having up to 120 nodes. Unfortunately here the
effect of parallel lookahead is overshadowed by an internal optimization of
DLV, which considers as selectable literals only a subset the available ones
called PT literals (c.f.r. [
For STRATCOMP it is evident that the standard heuristics is the best, and that the effect of parallel lookahead made dl.2.std and dl.3.std to be the best variants (still dl.2 shows less overhead compared with dl.3), which were capable to solve instances having up to 290 companies; whereas, the hsatzbased systems were stopped before reaching 150 companies, and dl.1.std reaches at most 170 companies.
Summarizing, results clearly show that the benefits of parallel lookahead are maximized when at most two workers are employed, and the technique can bring interesting speedups on hard instances.
Evaluation of the Multi-Heuristics Approach. The results reported above, as one can expect, show that there is no heuristics performing well in all cases (e.g. hsatz is the best for 3SAT, while in the other two domains hstd is the winner). In order to evaluate the second strategy proposed in this paper, we considered a variant implementing the multi-heuristics approach and exploiting the best parallel lookahead settings (named dl2.MultiHeu). We compared dl2.MultiHeu with the best performer in each domain among the ones considered before; the result are shown in Figure 4(b), in Figure 4(d) and in Figure 4(f), which reports the performance of those variants on 3SAT, HAMPATH and STRATCOMP, respectively.
The picture here is very clear, dl2.MultiHeu is able to move forward the limit of the the largest instance solved in 10 minutes. Still the synchronization overhead, paid to stop the concurrent model generators remains evident, but the dramatic advantage of selecting the best possible criterion per instance allows for solving larger instances in less time. For instance dl2.MultiHeu solved instances with up to 160 nodes in HAMPATH where the competitor stopped at 120 nodes; and dl2.MultiHeu solved up to 3000 companies vs 2900. The overall performance leap becomes dramatic when 4We tried also variants with more than three workers confirming this statement; results have been omitted for the sake of readability.
dl.2satz dl.2MultiHeur 1 200
dl.1std dl.2MultiHeur ) s ( e m i T g n i n n u R : T A S 3 ) s ( e m i T g n i n n u R : H T A P M A H ) s ( e m i T g n i n n u R : P M O C T A R T S dl.2std dl.2MultiHeur
(d) 260 (a)
(c) 220 240 280 300 320 220 240 260 280 300 320 Number of Propositional Variables (b) 100 ) s ( e m i T g n i n n u R : A 10 T S 3 ) s ( e m i T g n i n n u R : H T A P M A H ) s ( e m i T g n i n n u R : P M O C T A R T S
(e)
(f) dl2.MultiHeu is compared with the original dl1.std: 300 vs 320 propositional variables for 3SAT; 120 vs 160 nodes for HAMPATH; and 1700 vs 3000 companies for STRATCOMP. 5
In this paper we reported on the first attempts to introduce parallelism in the DLV system. In particular, we focused on the Model Generator module and we experimented with two parallel techniques: parallel lookahead and multi-heuristic search strategy. The results show that great benefits can be already obtained by exploiting simple parallelization strategies in the expensive phase of the answer sets computation. Nevertheless our work is still in a preliminary stage: much has to be done in order to obtain an efficient and solid implementation; moreover, more sophisticated parallelization techniques, specifically conceived for DLV have to be designed, probably requiring stronger modifications to the original system implementation. This is subject of future work. Once a more stable parallel system will be obtained, we plan to make a larger experimental activity considering more domains, more techniques (both novel and well-known), and involving comparison with other already well-assessed parallel systems.
This work has been partially supported by the Regione Calabria and EU under POR Calabria FESR 2007-2013 within the PIA project of DLVSYSTEM s.r.l..