=Paper=
{{Paper
|id=Vol-1451/paper2
|storemode=property
|title=JWASP: A New Java-Based ASP Solver
|pdfUrl=https://ceur-ws.org/Vol-1451/paper2.pdf
|volume=Vol-1451
|dblpUrl=https://dblp.org/rec/conf/aiia/AlvianoDR15
}}
==JWASP: A New Java-Based ASP Solver==
https://ceur-ws.org/Vol-1451/paper2.pdf
JWASP: A New Java-Based ASP Solver
Mario Alviano, Carmine Dodaro, and Francesco Ricca
Department of Mathematics and Computer Science,
University of Calabria, 87036 Rende (CS), Italy
{alviano,dodaro,ricca}@mat.unical.it
Abstract. Answer Set Programming (ASP) is a well-known declarative pro-
gramming language for knowledge representation and non-monotonic reasoning.
ASP solvers are usually written in C/C++ with the aim of extremely optimiz-
ing their performance. Indeed, C/C++ allow for several low level optimizations,
which however come at the price of a less portable implementation. This is a
problem for some real world use cases which do not actually require an extremely
efficient computation, but would benefit from a platform-independent and easily-
deployable implementation. Motivated by such use cases, we develop JWASP, a
new ASP solver written in Java and extending the open source library SAT 4 J in or-
der to process ASP programs with atomic heads. We also report on a preliminary
experiment assessing the performance of JWASP, whose results are encouraging:
JWASP is a good candidate as an alternative ASP solver for platform-independent
applications, which cannot rely on current ASP solvers.
1 Introduction
Answer Set Programming (ASP) [5] is a declarative programming paradigm, which has
been proposed in the area of non-monotonic reasoning and logic programming. The idea
of ASP is to represent a given computational problem by a logic program whose answer
sets correspond to solutions, and then use a solver to find them [5]. The availability of
solvers has made possible the application of ASP for solving complex problems arising
in several areas [1, 6], including AI, knowledge representation and reasoning, databases,
bioinformatics. Recently ASP has been also used to solve a number of industry-level
applications [7, 21].
Answer set programming is computationally hard, and modern ASP solvers are usu-
ally based on one of two alternative approaches. The first of these approaches consists
in implementing a native algorithm by adapting SAT solving techniques [22]. In par-
ticular, CDCL backtracking with learning, restarts, and conflict-driven heuristics is ex-
tended with ASP-specific propagation techniques such as support inference via Clark’s
completion, and well-founded inference via source pointers [23]. The second approach
resorts on rewriting techniques into SAT formulas, which are then evaluated by an off
the shelf SAT solver [13].
ASP solvers, like SAT solvers, are developed having in mind the (often well-deserved)
goal of maximizing performance. For this reason, ASP solvers are usually written in
C/C++, a programming language that is suited for implementing several low level opti-
mizations, but at the price of a reduced portability. This is a problem for some real world
16
M.Alviano et al. JWASP: A New Java-Based ASP Solver
use cases which do not actually require the highest available performance in computa-
tion, but would benefit from a platform-independent and easily-deployable implemen-
tation. For example, the iTravel system [20] takes advantage of some ASP-based web
services implemented as Java servlets interacting with DLV [16] via the DLV WRAP -
PER API [19]. Usually, Java servlets are easily exportable as WAR archives, which are
then deployable to different servers by simply copying the archives. Such a simplicity
was not possible with the ASP-based web services because different versions of DLV
were required for servers running different operating systems. A similar issue also af-
fects the distribution of ASPIDE [9], an IDE for ASP developed in Java which must
include different versions of an ASP solver for different operating systems. An ASP
solver implemented in Java would simplify the distribution of ASPIDE, not preventing
the possibility to run other ASP solvers written in C/C++ if needed.
If on the one hand Java provides all the means for implementing a platform-inde-
pendent ASP solver, on the other hand the following questions have to be answered:
How much overhead is introduced? Is the performance of an ASP solver written in Java
acceptable when compared with state of the art ASP solvers? Motivated by the needs
arising in different use cases, and in order to answer these two questions, we developed
JWASP (https://github.com/dodaro/jwasp.git), a new ASP solver writ-
ten in Java. JWASP is based on the open source library SAT 4 J [15]. In particular, JWASP
extends SAT 4 J in order to process ASP programs with atomic heads.
A preliminary experiment assessing the performance of JWASP has been conducted
on benchmarks from the previous ASP competitions [1, 6]. In particular, JWASP was
compared with the following state of the art ASP solvers: the native CLASP 3.1.1 [11]
and WASP [3]; the rewriting-based LP 2 SAT endowed by GLUCOSE [4]; and LP 2 SAT en-
dowed by SAT 4 J [15]. The results are encouraging. In fact, even if JWASP cannot match
the performance of CLASP, which is actually expected, it can compete with a prominent
rewriting-based ASP solver using GLUCOSE. Our experiment highlights that JWASP is
a good candidate as an alternative ASP solver for platform-independent applications,
where conventional solvers cannot be used or might not be comfortably integrated.
2 Preliminaries
Syntax and semantics of propositional logic and propositional ASP are briefly intro-
duced in this section.
2.1 Propositional Logic
Syntax. Let A be a fixed, countable set of (Boolean) variables, or (propositional) atoms,
including ⊥. A literal ℓ is either an atom a, or its negation ¬a. A clause is a set of
literals representing a disjunction, and a propositional formula ϕ is a set of clauses
representing a conjunction, i.e., only formulas in conjunctive normal form (CNF) are
considered here.
Semantics. An interpretation I is a set of literals over atoms in A \ {⊥}. Intuitively, lit-
erals in I are true, literals whose complement is in I are false and the remaining literals
17
M.Alviano et al. JWASP: A New Java-Based ASP Solver
are undefined. An interpretation I is total if there are no undefined literals, otherwise
I is partial. An interpretation I is inconsistent if for an atom a both a and ¬a are in I.
Relation |= is inductively defined as follows: for a ∈ A, I |= a if a ∈ I, and I |= ¬a
if ¬a ∈ I; for a clause c, I |= c if I |= ℓ for some ℓ ∈ c; for a formula ϕ, I |= ϕ if
I |= c for all c ∈ ϕ. If I |= ϕ then I is a model of ϕ, I satisfies ϕ, and ϕ is true w.r.t.
I. If I 6|= ϕ then I is not a model of ϕ, I violates ϕ, and ϕ is false w.r.t. I. Similar for
literals, and clauses. A formula ϕ is satisfiable if there is an interpretation I such that
I |= ϕ; otherwise, ϕ is unsatisfiable.
Example 1. Consider the following formula ϕ:
{a, ¬b} {b, ¬a} {¬a} {c} {c, ¬b}
ϕ is satisfiable and the interpretation I = {¬a, ¬b, c} is a model. ✁
2.2 Answer Set Programming
Syntax. Let ∼ denote negation as failure. A ∼-literal (or just literal when clear from
the context) is either an atom (a positive literal), or an atom preceded by ∼ (a negative
literal). A logic program Π is a finite set of rules of the following form:
a ← b1 , . . . , bk , ∼bk+1 , . . . , ∼bm (1)
where m ≥ 0, and a, b1 , . . . , bm are atoms in A. For a rule r of the form (1), set {a} is
called head of r, and denoted H(r); conjunction b1 , . . . , bm , ∼bk+1 , . . . , ∼bm is named
body of r, and denoted B(r); the sets {b1 , . . . , bk } and {bk+1 , . . . , bm } of positive and
negative literals in B(r) are denoted B + (r) and B − (r), respectively. A constraint is a
rule r such that H(r) = {⊥}.
Semantics. An interpretation I is a set of ∼-literals over atoms in A \ {⊥}. Relation |=
is extended as follows: for a negative literal ∼a, I |= ∼a if ∼a ∈ I; for a conjunction
ℓ1 , . . . , ℓn (n ≥ 0) of literals, I |= ℓ1 , . . . , ℓn if I |= ℓi for all i ∈ [1..n]; for a rule
r, I |= r if H(r) ∩ I 6= ∅ whenever I |= B(r); for a program Π, I |= Π if I |= r
for all r ∈ Π. The definition of a stable model is based on a notion of program reduct
[12]: Let Π be a normal logic program, and I an interpretation. The reduct of Π w.r.t.
I, denoted Π I , is obtained from Π by deleting each rule r such that B − (r) ∩ I 6= ∅,
and removing negative literals in the remaining rules. An interpretation I is an answer
set for Π if I |= Π and there is no total interpretation J such that J ∩ A ⊂ I ∩ A and
J |= Π I . The set of all answer sets of a program Π is denoted SM (Π). Program Π is
coherent if SM (Π) 6= ∅; otherwise, Π is incoherent.
Example 2. Consider the following program Π:
a←c a ← b, ∼e b ← a, ∼e
c ← ∼d d ← ∼c e ← ∼d
I = {a, ∼b, c, ∼d, e} is an answer set of Π. ✁
18
M.Alviano et al. JWASP: A New Java-Based ASP Solver
preprocessing choose undefined literal
[learnt loop formula]
unit propagation
[consistent]
well founded propagation
[inconsistent]
analyze conflict
learning
restore consistency [no undefined literals]
backjumping
[succeed]
[fail]
INCOHERENT COHERENT
Fig. 1. Computation of an answer set in JWASP.
3 Answer Set Computation in JWASP
In this section we first review the algorithms implemented in JWASP for the computa-
tion of an answer set, and then we describe how these were implemented by extending
SAT 4 J . The presentation is properly simplified to focus on the main principles.
3.1 Main Algorithms
The main algorithm is depicted in Figure 1.
Preprocessing. The first step is a preprocessing of the input program Π, that is trans-
formed into a propositional formula called the Clark’s completion of the program Π,
denoted Comp(Π). This step is performed since answer sets are supported models [17].
A model I of a program Π is supported if each a ∈ I ∩ A is supported, i.e., there exists
a rule r ∈ Π such that H(r) = a, and B(r) ⊆ I. In more detail, given a rule r ∈ Π,
let auxr denote a fresh atom, i.e., an atom not appearing elsewhere, the completion of
Π consists of the following clauses:
– {¬a, auxr1 , . . . , auxrn } for each atom a occurring in Π, where r1 , . . . , rn are the
rules of Π whose head is a; S S
– {H(r), ¬auxr } and {auxr } ∪ a∈B + (r) ¬a ∪ a∈B − (r) a for each rule r ∈ Π;
– {¬auxr , ℓ} for each r ∈ Π and ℓ ∈ B(r).
19
M.Alviano et al. JWASP: A New Java-Based ASP Solver
After computing the Clark’s completion Comp(Π), the input is further simplified ap-
plying classical preprocessing techniques of SAT solvers [8], and then the nondetermin-
istic search takes place.
CDCL Algorithm. The main ASP solving algorithm is similar to the CDCL procedure
of SAT solvers. In the beginning a partial interpretation I is set to ∅. Function unit
propagation extends I with those literals that can be deterministically inferred. This
function returns false if an inconsistency (or conflict) is detected, true otherwise. When
an inconsistency is detected, the algorithm analyzes the inconsistent interpretation and
learns a clause using the 1-UIP learning scheme [18]. The learned clause models the
inconsistency in order to avoid exploring the same search branch several times. Then,
the algorithm unrolls choices until consistency of I is restored, and the computation
resumes by propagating the consequences of the clause learned by the conflict analysis.
If the consistency cannot be restored, the algorithm terminates returning INCOHERENT.
When no inconsistency is detected, the well founded propagation (detailed in the fol-
lowing) checks whether I is unfounded-free. In case I is not unfounded-free a clause
is added to Comp(Π) and unit propagation is invoked. If I is unfounded-free and the
interpretation I is total then the algorithm terminates returning COHERENT and I is an
answer set of Π. Otherwise, an undefined literal, say ℓ, is chosen according to some
heuristic criterion. The computation then proceeds on I ∪ {ℓ}. Unit propagation and
well founded propagation are described in more detail in the following.
Propagation rules. JWASP implements two deterministic inference rules for pruning the
search space during answer set computation. These propagation rules are named unit
and well founded. Unit propagation is applied first. It returns false if an inconsistency
arises. Otherwise, well founded propagation is applied. Well founded propagation may
learn an implicit clause in Π, in which case unit propagation is applied on the new
clause. More in details, unit propagation is as in SAT solvers: An undefined literal ℓ is
inferred by unit propagation if there is a clause c that can be satisfied only by ℓ, i.e., c
is such that ℓ ∈ c is undefined and all literals in c \ {ℓ} are false w.r.t. I. Concerning
well founded propagation, we must first introduce the notion of an unfounded set. A
set X of atoms is unfounded if for each rule r such that H(r) ∩ X 6= ∅, at least
one of the following conditions is satisfied: (i) a literal ℓ ∈ B(r) is false w.r.t. I; (ii)
B + (r) ∩ X 6= ∅. Intuitively, atoms in X can have support only by themselves. Well
founded propagation checks whether the interpretation contains an unfounded set X. In
this case, it learns a clause forcing falsity of an atom in X. Clauses for other atoms in X
will be learned on subsequent calls to the function, unless an inconsistency arises during
unit propagation. In case of inconsistencies, indeed, the unfounded set X is recomputed.
3.2 Implementation
The implementation of a modern and efficient ASP solver requires the implementation
of at least three modules. The first module is the parser of a ground ASP program.
The second module computes the Clark’s completion. The third module implements
the CDCL backtracking algorithm extended by applying well founded propagation as
presented in Section 3.1. Concerning the parser, JWASP accepts as input normal ground
20
M.Alviano et al. JWASP: A New Java-Based ASP Solver
programs expressed in the numeric format of GRINGO [10]. The Clark’s completion is
computed after the whole program has been parsed. The third module is implemented
by JWASP exploiting the open source Java library SAT 4 J [15]. In particular, SAT 4 J pro-
vides an implementation of the base CDCL algorithm. JWASP extends this algorithm
by modifying the propagate function of SAT 4 J, which in our solver includes the well
founded inference rule. In particular, specific data structures and the algorithm for com-
puting unfounded sets are introduced in JWASP which are not provided by SAT 4 J.
4 Experiment
The performance of JWASP was compared with CLASP 3.1.1 and LP 2 SAT [13]. CLASP
is a native state of the art ASP solver, while LP 2 SAT is an ASP solver based on a rewrit-
ing of the ASP program into a SAT formula that is evaluated using a SAT solver. Two
variants of LP 2 SAT were considered, namely LP 2 GLUCOSE and LP 2 SAT 4 J, which use
GLUCOSE [4] and SAT 4 J [15] as SAT solver, respectively. All the ASP solvers use
GRINGO [10] as grounder. The experiment concerns a comparison of the solvers on
publicly available benchmarks used in the 3rd and 4th ASP competitions [1, 6]. The
experiment was run on a four core Intel Xeon CPU X3430 2.4 GHz, with 16 GB of
physical RAM, and operating system Debian Linux. Time and memory limits were set
to 600 seconds and 15 GB, respectively. Performance was measured using the tools
pyrunlim and pyrunner (https://github.com/alviano/python).
Table 1 summarizes the number of solved instances and the average running time
in seconds for each solver. In particular, the first column reports the considered bench-
marks; the remaining columns report the number of solved instances within the time-out
(solved), and the running time averaged over solved instances (time). The first obser-
vation is that JWASP outperforms the rewriting-based LP 2 SAT 4 J. In fact, JWASP solved
17 more instances than LP 2 SAT 4 J and it is in general faster. The advantage of JWASP
is obtained in 3 different benchmarks, namely KnightTour, MazeGeneration, and Num-
berlink, where JWASP solves 5, 7, and 3 more instances than LP 2 SAT 4 J. Once the SAT
solver backhand is replaced by GLUCOSE, a clear improvement of performance is mea-
sured. LP 2 GLUCOSE is clearly faster (it solves 20 instances more) than LP 2 SAT 4 J. In
Table 1. Solved instances and average running time.
LP 2 SAT 4 J JWASP LP 2 GLUCOSE WASP CLASP
Track # sol. avg t sol. avg t sol. avg t sol. avg t sol. avg t
GraphColouring 30 8 47.45 7 31.07 14 124.02 8 66.15 13 129.98
HanoiTower 30 27 120.80 26 166.57 30 10.41 30 33.83 28 53.18
KnightTour 10 2 67.66 7 52.03 3 24.37 8 4.39 10 57.95
Labyrinth 30 14 222.34 17 158.44 18 151.70 26 72.64 26 48.05
MazeGeneration 10 3 332.46 10 5.06 4 164.15 10 3.10 10 1.04
Numberlink 10 4 98.05 7 7.67 5 164.67 8 12.71 8 7.91
SokobanDecision 10 6 46.57 7 61.42 10 59.34 9 92.15 10 42.91
Total 130 64 133.72 81 100.50 84 82.45 99 44.75 105 52.48
21
M.Alviano et al. JWASP: A New Java-Based ASP Solver
this case, since the rewriting technique is the same, the difference of performance is due
to the fact that GLUCOSE outperforms LP 2 SAT 4 J. The performance gap between C++
and Java implementations can be observed also by comparing WASP and JWASP. In
particular, WASP solves 18 more instances than JWASP. The differences are noticeable
in Labyrinth where WASP solves 9 more instances than JWASP. Similar considerations
hold by comparing CLASP and JWASP. In fact, the former is in general faster solving
24 more instances than the latter. Finally, it is important to note that JWASP is basically
comparable in performance with LP 2 GLUCOSE (the latter solves only 3 instances more
than the former). An in-depth analysis shows that JWASP is faster in KnightTour and
MazeGeneration solving 4 and 6 instances more than LP 2 GLUCOSE, respectively. On
the contrary, LP 2 GLUCOSE is faster than JWASP in GraphColouring, HanoiTower, and
SokobanDecision. We observe that the main advantage of JWASP over LP 2 GLUCOSE
is registered (as expected) in the benchmarks in which the well founded propagation
(implemented natively by JWASP) is applied, such as KnightTour and MazeGeneration.
5 Discussion
During recent years, ASP has obtained growing interest since efficient implementations
were available. For reason of efficiency, most of the modern ASP solver are imple-
mented in C++. To the best of our knowledge, the only previous Java-based ASP solver
was JSMODELS [14], which is not developed anymore. JSMODELS was based on SMOD -
ELS featuring the DPLL algorithm and lookahead heuristics. From an abstract point of
view, JWASP is more similar to modern ASP solvers, like WASP [2, 3] and CLASP [11].
In fact, all the three solvers are based on CDCL algorithm and source pointers for the
computation of unfounded sets. However, JWASP is implemented in Java and thus it is a
cross-platform and more portable implementation. An alternative to the development of
a native solver is to rewrite the input program into a CNF formula, as done by the family
of solvers LP 2 SAT [13]. This alternative approach can be applied to obtain a Java-based
solver by endowing LP 2 SAT with a Java-based SAT solver such as SAT 4 J. This ap-
proach is less efficient than JWASP in the experimental analysis reported in this paper. It
is worth noting that, both JWASP and LP 2 SAT apply the Clark’s completion [17]. Thus,
the main difference between JWASP and LP 2 SAT 4 J consists of the native computation
of unfounded set of JWASP, which is obtained by using an algorithm based on source
pointers introduced by SMODELS [23].
In this paper we reported on the new Java-based ASP solver JWASP built on the
top of the SAT solver SAT 4 J. The new solver was compared with both C++ and Java-
based approaches. In our experiment, JWASP outperforms the Java-based alternative
LP 2 SAT 4 J , and it is competitive with LP 2 GLUCOSE . However, as expected, JWASP is in
general slower than the native solvers. This confirms that C++ implementations are usu-
ally much faster than Java-based approaches as also noted in [15]. Future work concerns
the extension of JWASP for handling optimization constructs and cautious reasoning.
References
1. M. Alviano, F. Calimeri, G. Charwat, M. Dao-Tran, C. Dodaro, G. Ianni, T. Krennwallner,
M. Kronegger, J. Oetsch, A. Pfandler, J. Pührer, C. Redl, F. Ricca, P. Schneider, M. Schwen-
22
M.Alviano et al. JWASP: A New Java-Based ASP Solver
gerer, L. K. Spendier, J. P. Wallner, and G. Xiao. The fourth answer set programming com-
petition: Preliminary report. In P. Cabalar and T. C. Son, editors, LPNMR, LNCS, pages
42–53, 2013.
2. M. Alviano, C. Dodaro, W. Faber, N. Leone, and F. Ricca. WASP: A native ASP solver based
on constraint learning. In P. Cabalar and T. C. Son, editors, LPNMR, volume 8148 of LNCS,
pages 54–66. Springer, 2013.
3. M. Alviano, C. Dodaro, N. Leone, and F. Ricca. Advances in WASP. In F. Calimeri, G. Ianni,
and M. Truszczynski, editors, LPNMR, volume 9345 of LNAI, page (to appear), 2015.
4. G. Audemard and L. Simon. Predicting learnt clauses quality in modern SAT solvers. In
C. Boutilier, editor, IJCAI, pages 399–404, 2009.
5. G. Brewka, T. Eiter, and M. Truszczynski. Answer set programming at a glance. Commun.
ACM, 54(12):92–103, 2011.
6. F. Calimeri, G. Ianni, and F. Ricca. The third open answer set programming competition.
TPLP, 14(1):117–135, 2014.
7. C. Dodaro, B. Nardi, N. Leone, and F. Ricca. Allotment problem in travel industry: A so-
lution based on ASP. In B. ten Cate and A. Mileo, editors, RR, volume 9209 of LNCS.
Springer, 2015.
8. N. Eén and A. Biere. Effective preprocessing in SAT through variable and clause elimination.
In SAT, volume 3569 of LNCS, pages 61–75. Springer, 2005.
9. O. Febbraro, K. Reale, and F. Ricca. ASPIDE: integrated development environment for
answer set programming. In J. P. Delgrande and W. Faber, editors, LPNMR, volume 6645 of
LNCS, pages 317–330. Springer, 2011.
10. M. Gebser, R. Kaminski, A. König, and T. Schaub. Advances in gringo series 3. In J. P.
Delgrande and W. Faber, editors, LPNMR, volume 6645 of LNCS, pages 345–351. Springer,
2011.
11. M. Gebser, B. Kaufmann, and T. Schaub. Conflict-driven answer set solving: From theory to
practice. Artif. Intell., 187:52–89, 2012.
12. M. Gelfond and V. Lifschitz. Classical negation in logic programs and disjunctive databases.
New Generation Comput., 9(3/4):365–386, 1991.
13. T. Janhunen. Some (in)translatability results for normal logic programs and propositional
theories. Journal of Applied Non-Classical Logics, 16(1-2):35–86, 2006.
14. H. V. Le and E. Pontelli. A Java Based Solver for Answer Set Programming.
15. D. Le Berre and A. Parrain. The sat4j library, release 2.2. JSAT, 7(2-3):59–6, 2010.
16. N. Leone, G. Pfeifer, W. Faber, T. Eiter, G. Gottlob, S. Perri, and F. Scarcello. The DLV
system for knowledge representation and reasoning. ACM TOCL, 7(3):499–562, 2006.
17. F. Lin and Y. Zhao. ASSAT: computing answer sets of a logic program by SAT solvers. Artif.
Intell., 157(1-2):115–137, 2004.
18. M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, and S. Malik. Chaff: Engineering an
efficient SAT solver. In DAC, pages 530–535. ACM, 2001.
19. F. Ricca. The DLV java wrapper. In F. Buccafurri, editor, AGP, pages 263–274, 2003.
20. F. Ricca, A. Dimasi, G. Grasso, S. M. Ielpa, S. Iiritano, M. Manna, and N. Leone. A logic-
based system for e-tourism. Fundam. Inform., 105(1-2):35–55, 2010.
21. F. Ricca, G. Grasso, M. Alviano, M. Manna, V. Lio, S. Iiritano, and N. Leone. Team-building
with answer set programming in the gioia-tauro seaport. TPLP, 12(3):361–381, 2012.
22. J. P. M. Silva and K. A. Sakallah. GRASP: A search algorithm for propositional satisfiability.
IEEE Trans. Computers, 48(5):506–521, 1999.
23. P. Simons, I. Niemelä, and T. Soininen. Extending and implementing the stable model se-
mantics. Artif. Intell., 138(1-2):181–234, 2002.
23