# grASP: A Graph Based ASP-Solver and Justification System

Fang Li1111Contact Author Huaduo Wang1 Gopal Gupta1
1University of Texas at Dallas
{fang.li, huaduo.wang<EMAIL_ADDRESS>
###### Abstract

Answer set programming (ASP) is a popular nonmonotonic-logic based paradigm
for knowledge representation and solving combinatorial problems. Computing the
answer set of an ASP program is NP-hard in general, and researchers have been
investing significant effort to speed it up. The majority of current ASP
solvers employ SAT solver-like technology to find these answer sets. As a
result, justification for why a literal is in the answer set is hard to
produce. There are dependency graph based approaches to find answer sets, but
due to the representational limitations of dependency graphs, such approaches
are limited. We propose a novel dependency graph-based approach for finding
answer sets in which conjunction of goals is explicitly represented as a node
which allows arbitrary answer set programs to be uniformly represented. Our
representation preserves causal relationships allowing for justification for
each literal in the answer set to be elegantly found. Performance results from
an implementation are also reported. Our work paves the way for computing
answer sets without grounding a program.

##  1 Introduction

Answer set programming (ASP) Gelfond and Lifschitz (1988); Marek and
Truszczyński (1999); Eiter et al. (2000); Simons et al. (2002) is a popular
nonmonotonic-logic based paradigm for knowledge representation and solving
combinatorial problems. Computing the answer set of an ASP program is NP-hard
in general, and researchers have been investing significant effort to speed it
up. Most ASP solvers employ SAT solver-like technology to find these answer
sets. As a result, justification for why a literal is in the answer set is
hard to produce. There are dependency graph (DG) based approaches to find
answer sets, but due to the representational limitations of dependency graphs,
such approaches are limited. In this paper we propose a novel dependency
graph-based approach for finding answer sets in which conjunctions of goals is
explicitly represented as a node which allows arbitrary answer set programs to
be uniformly represented. Our representation preserves causal relationships
allowing for justification for each literal in the answer set to be elegantly
found. Performance results from an implementation are also reported. Our work
paves the way for computing answer sets without grounding a program.

Compared to SAT solver based implementations, graph-based implementations of
ASP have not been well studied. Very few researchers have investigated graph-
based techniques. NoMoRe system Anger et al. (2001) represents ASP programs
with a block graph (a labeled graph) with meta-information, then computes the
A-coloring (non-standard graph coloring with two colors) of that graph to
obtain answer sets. Another approach Konczak et al. (2005) uses rule
dependency graph (nodes for rules, edges for rule dependencies) to represent
ASP programs, then performs graph coloring algorithm to determine which rule
should be chosen to generate answer sets. Another group Linke and Sarsakov
(2005) proposed an hybrid approach which combines different kinds of graph
representations that are suitable for ASP. The hybrid graph uses both rules
and literals as nodes, while edges represent dependencies. It also uses the
A-coloring technique to find answer sets.

All of the above approaches were well designed, but their graph
representations are complex as they all rely on extra information to map the
ASP elements to nodes and edges of a graph. In contrast, our approach uses a
much simpler graph representation, where nodes represent literals and an edge
represent the relationship between the nodes it connects. Since this
representation faithfully reflects the casual relationships, it is capable of
producing causal justification for goals entailed by the program.

##  2 Background

###  2.1 Answer Set Programming

Answer Set Programming (ASP) is a declarative paradigm that extends logic
programming with negation-as-failure. ASP is a highly expressive paradigm that
can elegantly express complex reasoning methods, including those used by
humans, such as default reasoning, deductive and abductive reasoning,
counterfactual reasoning, constraint satisfaction Baral (2003); Gelfond and
Kahl (2014).

ASP supports better semantics for negation (negation as failure) than does
standard logic programming and Prolog. An ASP program consists of rules that
look like Prolog rules. The semantics of an ASP program $\Pi$ is given in
terms of the answer sets of the program ground($\Pi$), where ground($\Pi$) is
the program obtained from the substitution of elements of the Herbrand
universe for variables in $\Pi$ Baral (2003). Rules in an ASP program are of
the form:

p :- q1, ..., qm, not r1, ..., not rn.

(1)

where $m\geq 0$ and $n\geq 0$. Each of p and qi ($\forall i\leq m$) is a
literal, and each not rj ($\forall j\leq n$) is a naf-literal (not is a
logical connective called negation-as-failure or default negation). The
literal not rj is true if proof of rj fails. Negation as failure allows us to
take actions that are predicated on failure of a proof. Thus, the rule r :-
not s. states that r can be inferred if we fail to prove s. Note that in Rule
1, p is optional. Such a headless rule is called a constraint, which states
that conjunction of qi’s and not rj’s should yield false. Thus, the constraint
:- u, v. states that u and v cannot be both true simultaneously in any model
of the program (called an answer set).

The declarative semantics of an Answer Set Program P is given via the Gelfond-
Lifschitz transform Baral (2003); Gelfond and Kahl (2014) in terms of the
answer sets of the program ground($\Pi$). More details on ASP can be found
elsewhere Baral (2003); Gelfond and Kahl (2014).

###  2.2 Dependency Graph

A dependency graph Linke and Sarsakov (2005) uses nodes and directed edges to
represent dependency relationships of an ASP rule.

######  Definition 1.

The dependency graph of a program is defined on its literals s.t. there is a
positive (resp. negative) edge from $p$ to $q$ if $p$ appears positively
(resp. negatively) in the body of a rule with head $q$.

Conventional dependency graphs are not able to represent ASP programs
uniquely. This is due to the inability of dependency graphs to distinguish
between non-determinism (multiple rules defining a proposition) and
conjunctions (multiple conjunctive sub-goals in the body of a rule) in logic
programs. For example, the following two programs have identical dependency
graphs (Figure 1).

⬇

%% program 1

p :- q, not r, not p.

%% program 2

p :- q, not p. p :- not r.

Figure 1: Dependency Graph for Programs 1 & 2

To make conjunctive relationships representable by dependency graphs, we first
transform it slightly to come up with a novel representation method. This new
representation method, called conjunction node representation (CNR) graph,
uses an artificial node to represent conjunction of sub-goals in the body of a
rule. This conjunctive node has a directed edge that points to the rule head
(Figure 2).

(a) CNR for Program 1

(b) CNR for Program 2

Figure 2: CNRs for program 1 & 2

The conjunction node, which is colored black, refers to the conjunctive
relation between the in-coming edges from nodes representing subogals in the
body of a rule. Note that a CNR graph is not a conventional dependency graph.

####  2.2.1 Converting CNR Graph to Dependency Graph

Since CNR graph does not follow the dependency graph convention, we need to
convert it to a proper dependency graph in order to perform dependency graph-
based reasoning. We use a simple technique to convert a CNR graph to an
equivalent conventional dependency graph. We negate all in-edges and out-edges
of the conjunction node. This process essentially converts a conjunction into
a disjunction. Once we do that we can treat the conjunction node as a normal
node in a dependency graph. As an example, Figure 3 shows the CNR graph to
dependency graph transformation for Program 3:

Figure 3: CNR-DG Transformation

⬇

%% program 3

p :- q, not r.

This transformation is a simple application of De Morgan’s law. The rule in
program 3 represents:

⬇

p :- C. C :- q, not r.

The transformation produces the equivalent rules:

⬇

p :- not C. C :- not q. C :- r.

Since conjunction nodes are just helper nodes which allow us to perform
dependency graph reasoning, we don’t report them in the final answer set.

####  2.2.2 Constraint Representation

ASP also allows for special types of rules called constraints. There are two
ways to encode constraints: (i) headed constraint where negated head is called
directly or indirectly in the body (e.g., Program 4), and (ii) headless
constraints (e.g., Program 5).

⬇

%% program 4

p :- not q, not r, not p.

%% program 5

:- not q, not r.

Our algorithm models these constraint types separately. For the former one, we
just need to apply the CNR-DG transformation directly. Note that the head node
connects to the conjunction node both with an in-coming edge and an out-going
edge (Figure 4(a)). For the headless constraint, we create a head node with
truth value as False.

(a) Program 4

(b) Program 5

Figure 4: Constraint DG

The reason why we don’t treat a headless constraint the same way as a headed
constraint is because in the latter case, if head node (p in Program 4) is
provable through another rule, then the headed constraint is inapplicable.
Therefore, we cannot simply assign a false value to its head.

###  2.3 Cycles in Program

Answer set programs have a notion of odd and even loops over negation as well
as positive loops. We refer to loops as cycles here. Note that a positive
(resp. negative) edge is an edge labeled with ‘+’ (resp. ‘-’).

######  Definition 2.

A cycle $C$ in a dependency graph is a Positive Cycle iff all edges in $C$ are
positive.

######  Definition 3.

A cycle $C$ in a dependency graph is a Negative Even Cycle (NEC) iff $C$ has
even number of negative edges.

######  Definition 4.

A cycle $C$ is a Negative Odd Cycle (NOC) iff $C$ has odd number of negative
edges.

Based on above definitions and the stable model semantics, three results
trivially follow:

######  Theorem 1.

If $C$ is a positive cycle, then all nodes in $C$ will have the same truth
value.

######  Theorem 2.

If $C$ is a NEC, then it will admit multiple answer sets obtained by breaking
arbitrary negative edges.

By breaking a cycle, we mean assigning appropriate truth values to the nodes
in the cycles obeying edge dependencies, and then deleting the edges. For
example, if we have the graph corresponding to:

⬇

p :- not q. q :- not p.

then breaking this negative even cycle will produce two answer sets:
$\\{$p$\\}$ and $\\{$q$\\}$: one in which node p is assigned true and q false,
and the other the opposite.

######  Theorem 3.

If $C$ is a negative odd cycle, then the program $\pi$ is satisfiable iff
there is at least one node assigned true in $C$.

If we have the graph corresponding to:

⬇

p :- not q. q :- not r. r :- not p.

then there will be no models unless one or more of p, q, or r are true through
other rules and are assigned the value True.

##  3 A Graph Algorithm for Answer Sets

We have developed the grASP graph-based algorithm for finding answer sets. The
philosophy of grASP is to translate an ASP program into a dependency graph,
then propagate truth values from nodes whose values are known to other
connected nodes, obeying the sign on the edge, until the values of all the
nodes are fixed. However, due to possible existence of a large number of
cycles, the propagation process is not straightforward. In grASP, we define a
collection of rules for propagating values among nodes involved in cycles.
These assignment rules take non-monotonicity of answer set program and the
causal relationship among nodes in the dependency graph into account.

Unlike other SAT-solver based approaches, our graph based approach enables
stratification of ASP programs based on dependence. The Splitting Theorem
Lifschitz and Turner (1994) can thus be used to link the various levels,
permitting values to be propagated among nodes more efficiently. Also, the
existence of sub-structures (sub-graphs) makes an efficient recursive
implementation algorithm possible.

###  3.1 Input

At present, the grASP algorithm takes only pure grounded propositional ASP
programs as input. A valid rule should be in the form of $head$ :- $body.$, :-
$body.$, or $head.$ For example, if we want to represent 3 balls, the form
$ball(1..3)$ is invalid. Instead, we have to declare them separately as
$ball(1).$ $ball(2).$ $ball(3).$ The input ASP program will be converted and
saved into a directed-graph data structure. The conversion process is based on
the concepts that were introduced in Section 2.2.

###  3.2 The grASP Algorithm

The grASP algorithm is designed in a recursive nature. Since a dependency
graph represents the causal relationships among nodes, the reasoning should
follow a topological order. We don’t need to do topological sorting to obtain
the order, instead, for each iteration, we just pick those nodes which have no
in-coming edges. We call this kind of node a root node. After picking the root
nodes, the algorithm checks their values. If a root node’s value has not been
fixed (no value yet), we assign False to it. Otherwise, the root node will
keep its value as is. Once all root nodes’ values are fixed, we will propagate
the values along their out-going edges in accordance with the sign on each
edge (the propagation rules will be discussed in Section 3.2.1). At the end of
this iteration, we remove all root nodes from the graph, then pass the rest of
the graph to the recursive call for the next iteration.

The input graph may contain cycles, and, of course, there will be no root
nodes in a cycle. Therefore, this recursive process will leave a cycle
unchanged. To cope with this issue, we proposed a novel solution, which wraps
all nodes in the same cycles together, and treat the wrapped nodes as a single
virtual node. All the in-coming and out-going edges connecting the wrapped
nodes to other nodes will be incident on or emanate from the virtual node.
Thus, the graph is rendered acyclic and ready for the root-finding procedure.

For each iteration of the recursive procedure, we have to treat regular root
nodes and virtual root nodes differently. If the node is a regular node, we do
the value assignment, but if it is a virtual node, we will have to break the
cycles. Cycle breaking means that we will remove the appropriate cycle edges
by assigning truth values to the nodes involved (cycle breaking will be
discussed in this section later). After cycle breaking, we will pass the nodes
and edges in this virtual node to another recursive call, because the virtual
node can be seen as a substructure of the program. The returned value of the
recursive call will be the answer set of the program constituting the virtual
node. When all regular and virtual root nodes are processed, we will have to
merge the values for propagation.

The value propagation in each iteration makes use of the splitting theorem
Lifschitz and Turner (1994) (details omitted due to lack of space). After
removing root nodes, rest of the graph acts as the top strata and all of the
predecessors constitute the bottom strata, using the terminology of Lifschitz
and Turner (1994). Thus, when we reach the last node in the topological order,
we will get the whole answer set.

The cycle breaking procedure may return multiple results, because a negative
even cycle generates two worlds (as discussed in Section 2.3). Therefore, the
merging of solution for the root nodes may possibly result in exponential
number of solutions. For example, if the root nodes consists of one regular
node and two virtual nodes, each virtual node generates two worlds & the
merging process will return four worlds. Of course, this exponential behavior
is inherent to ASP.

Algorithm 1 grASP core algorithm

1: reasoningRec(Graph g)

2: if $g$ is $empty$ then

3: return $g.nodes.values$

4: end if

5: $roots\leftarrow findRoot(g)$

6: $regular\leftarrow new$ $List()$

7: $virtual\leftarrow new$ $List()$

8: for $node$ in $roots$ do

9: if $node.type==regular$ then

10: if $node.value==None$ then

11: $node.value\leftarrow False$

12: end if

13: $regular.append(node.value)$

14: else

15: $worlds\leftarrow breakCycle(node)$

16: $current\leftarrow new$ $List()$

17: for $w$ in $worlds$ do

18: $current.append($reasoningRec$(w))$

19: end for

20: $virtual.append(values)$

21: end if

22: end for

23: $root\\_values\leftarrow merge\\_roots(regular,virtual)$

24: $results\leftarrow new$ $List()$

25: for $sub\\_world$ in $root\\_values$ do

26: $sub\\_g\leftarrow g.copy()$

27: $propagate(sub\\_g,sub\\_world)$

28: $sub\\_g.remove(roots)$

29: for $ans$ in reasoningRec$(sub\\_g)$ do

30: $results.append(sub\\_world.extend(ans))$

31: end for

32: end for

33: return $results$

Algorithm 1 is the pseudocode of grASP’s core algorithm. Line 9-13 assigns
values to regular root nodes, while line 14-20 deals with value assignments
for virtual nodes. Cycle breaking happens at line 15. Line 23 merges all
worlds generated by the root nodes, and prepares these values as the bottom
strata (Splitting Theorem Lifschitz and Turner (1994)) for the next layer.
Lines 24-32 deals with the recursive calls on the rest of the graph.

Note that we can optimize the system by adding consistency checking into the
regular root node processing (line 11). Since the constraint node is always
False (see Section 2.2.2), the algorithm can narrow the search by tracing back
along its in-coming edges. For example, if a negative edge is incident into
the constraint node, we will know that the node on the other end cannot be
False. Then if that node happens to be assigned a False value, we stop the
search along that path.

####  3.2.1 Propagation Rules

In an ASP rule, the head term only can be assigned as True if all its body
term(s) are true. For example, in rule p :- not q., only when q is unknown or
known as False, p will be True. For another example p :- q., p will be True,
only when q is known as True. In both examples, p will not be assigned as
False, until the reasoning of the whole program fails to make it True.
Therefore, mapping this to our graph representation, we obtain two propagation
rules: (i) when a node $N$ has a True value, assign True to all the nodes
connected to $N$ via positive out-going edges of $N$; (ii) when a $N$ node has
a False value, assign True to all the nodes connected to $N$ via negative out-
going edges of $N$.

####  3.2.2 Cycle Wrapping

As previously mentioned (Section 3.2), those nodes which are involved in the
same cycles need to be wrapped into a virtual node. The reason being that we
want the tangled nodes to act like a single node, in order to be found as a
root. This requires the dependency of the wrapped nodes to be properly
handled. The virtual node should inherit the dependencies of all the node it
contains. These dependency relations include both incoming and outgoing edges.

Since cycles may be overlapped or nested with each other, we can make use of
the strongly connected component concept in graph theory. Thus, each strongly
connected component will be a virtual node.

####  3.2.3 Cycle Breaking

We can state the following corollary:

######  Corollary 1.

In the dependency graph of an answer set program, if a node’s value is True,
all of its in-coming edges and negative out-going edges can be removed. If a
node’s value is False, then all its positive out-edges can be removed.

###### Proof.

According to the propagation rules (discussed in Section 3.2.1), a node can
only be assigned True through in-coming edges. When a node has already been
known as True, it no longer needs any assignment, then all in-coming edges
become meaningless. Also, a negative edge won’t be able to propagate the True
value to the other side. If a node has been known as False, we still have to
keep its in-coming edges to detect inconsistency (if some of its predecessors
attempt to assign it as True, the program is inconsistent). Note that a node
labeled False cannot make any node True through an outgoing positive edge. ∎

We will use Corollary 1 to remove edges while breaking cycles. According to
the algorithm design, cycles will only exit in virtual nodes, and a virtual
node will only be visited as a root. Therefore, when we start looking at a
cycle that needs to be broken, it means that there is no in-coming edge from
outside connected to any node inside the cycle. As we know that there are only
three types of cycles: positive cycles (PC), negative even cycles (NEC),
negative odd cycles (NOC) (see Section 2.3), the tangled cycles in a virtual
node can be divided into four cases. We will illustrate these scenarios by
using the pseudocode shown in Algorithm 2.

Algorithm 2 Cycle breaking algorithm

1: $result\leftarrow new$ $List()$

2: if NEC exists then

3: if NOC exists then

4: if overlap of NEC and NOC exists then

5: for $node$ in $overlapped\\_nodes$ do

6: pick arbitrary NEC that contains $node$

7: break the NEC into two worlds (by Theorem 2)

8: choose the world in which $node==True$

9: remove edges (by Corollary 1)

10: add the chosen world to $result$

11: end for

12: else

13: return Unsatisfiable

14: end if

15: else

16: pick arbitrary NEC

17: break the NEC into two worlds (by Theorem 2)

18: remove edges (by Corollary 1)

19: add both worlds to $result$

20: end if

21: else if NOC exists then

22: return Unsatisfiable

23: else

24: assign False value to every node

25: remove edges (by Corollary 1)

26: add the world to $result$

27: end if

28: return $result$

The most important thing for cycle breaking is that we need to follow a
specific order with respect to types of cycles. As we discussed in Theorem 2,
NECs create worlds, NOCs kill worlds. Which means that a negative even cycle
can divide a world into two, while a negative odd cycle will make one or more
worlds unsatisfiable and thus disappear (this happens if no node in the NOC
has the value True). Therefore, when breaking a virtual node that has hybrid
cycles, we need to first check those NOCs to make sure that these cycles are
satisfiable. According to Theorem 3, a NOC will make the world satisfiable if
and only if it has True nodes. In a virtual node, the only way for a NOC to
have True node would be by overlapping with a NEC. The overlapping node is
assigned True which means that the NEC admits only possible world, that is the
one with the overlapped node as True (see Example 1). Refer to Algorithm 2,
line 4-11 deals with this situation.

Figure 5: A Cycle Breaking Example

######  Example 1 (Breaking of Overlapped Cycles).

In Figure 5, {$A$, $B$, $C$} is an negative odd cycle, and {$B$, $D$} is a
negative even cycle. We first need to make sure the negative odd cycle can be
broken (i.e., a satisfying assignment made to the nodes in the NOC). In
traversal, we found that node $B$ can be assigned as true by breaking the
negative even cycle {$B$, $D$}. Therefore, we can get a model {A, B} by
keeping $B$ as true.

When there is a NOC which does not overlaps with any NEC, no assignment is
possible (line 13 and 22 in the Algorithm 1). If there is neither NEC, nor
NOC, the only possible situation is that all nodes that are connected by
positive edges. Since we are in the virtual node which has no predecessors,
per Theorem 1, there is no way to make these nodes True; so we assign False to
every node, and delete all edges.

###  3.3 Implementation and Performance

The grASP system has been written in python. A C++ version under the same
system architecture design (Figure 6) is under development. We adopted
Johnson’s algorithm which was proposed for finding all the elementary circuits
of a directed graph Johnson (1975). Our Python implementation uses the
$DiGraph$ data structure and simple_cycles function from NetworkX Hagberg et
al. (2008).

The performance testing for grASP was done on two types of programs: (i)
established benchmarks such as N-queens; (ii) randomly generated answer set
programs. Clingo Gebser et al. (2014) was chosen as the system to compare
with. For the first phase, we chose four classic NP problems (map coloring
problem, Hamiltonian cycle problem, etc.). The results are shown in Table 1.
For the second phase, we used a novel propositional ASP program generator that
we have developed for this purpose to generate random programs. The testing
performed five rounds with 100 programs each (Table 2). The performance
comparison shows that for programs with simpler cycle conditions, grASP
achieved similar speed to Clingo, but when solving programs with large number
of cycles, grASP is slowed down by the cycle breaking process.

Problem | Clingo | grASP
---|---|---
Coloring-10 nodes | 0.004 | 0.693
Coloring-4 nodes | 0.001 | 0.068
Ham Cycle-4 nodes(no cross edges) | 0.001 | 0.052
Ham Cycle-4 nodes(fully connected) | 0.002 | 0.089
Birds | 0.001 | 0.001
Stream Reasoning | 0.001 | 0.001
Table 1: Performance Comparison on Classic Problems Round | #Rules | #NEC | #NOC | Clingo | grASP
---|---|---|---|---|---
1 | 3231 | 61813 | 61781 | 0.032 | 0.351
2 | 3078 | 28593 | 29040 | 0.027 | 0.276
3 | 3307 | 39346 | 39433 | 0.028 | 0.087
4 | 3069 | 14581 | 14868 | 0.022 | 0.405
5 | 3074 | 23017 | 22984 | 0.024 | 0.801
Table 2: Performance on Random Problems (time in seconds) Figure 6: grASP
System Architecture

##  4 Causal Justification

A major advantage of grASP is that it provides justification as to why a
literal is in an answer set for free. Providing justification is a major
problem for implementations of ASP that are based on SAT solvers. In contrast
to SAT-based ASP solvers, grASP maintains the information about structure of
an ASP program while computing stable models. Indeed, the resulting graph
itself is a justification tree. Since the truth values of all vertices are
propagated along edges, we are able to find a justification by looking at the
effective out-going edges and their ending nodes. Here the effective out-going
edge refer to an edge that actually propagated True value to its ending node.
According to propagation rules that are discussed in Section 3.2.1, there are
only two type of effective out-going edges: (i) positive edge coming from a
True node; (ii) negative edge coming from a False node. Every effective out-
going edge should point to a True node.

######  Example 2 (Graph Coloring Problem).

Given a planar graph, color each node (red/green/blue), so that no two
connected nodes have the same color.

Let’s take graph coloring as an example. The problem is defined in Example 2.
For simplicity, we use a configuration with 4 nodes and 4 edges. We got 18
different answer sets. Now we want to justify one of them, which is: blue(1),
red(2), blue(3), green(4). The justification first picks effective out-going
edges, then check each edge’s ending node. If all those ending nodes are True,
the answer set is justified. Figure 7 shows a part of the justification graph.
The red-circled nodes are True nodes, while the black ones are False. The path
justifying a literal can be traced on this graph.

Figure 7: Part of the Justification Graph

##  5 Conclusion and Future Work

We proposed a dependency graph based approach to compute the answer sets of an
answer set program. We use a novel transformation to ensure that each program
has a unique dependency graph, as otherwise multiple programs can have the
same dependency graph. A major advantage of our algorithm is that it can
produce a justification for any proposition that is entailed by a program.
Currently, grASP only works for propositional answer set programs. Our goal is
to extend it so that answer sets of datalog programs (i.e., answer set
programs with predicates whose arguments are limited to variables and
constants) can also be computed without having to ground them first. This will
be achieved by dynamically propagating bindings along the edges connecting the
nodes in our algorithm’s propagation phase.

The grASP system is being developed with three main applications in mind (i)
justification: being able to justify each literal in the answer set, (ii)
program debugging: if a program has no answer sets, then find (small) changes
to the program (with some guidance from the user) that will make the program
succeed, (iii) commonsense reasoning: given a query, we want to not only find
out a justification for it, but also the related associative knowledge. E.g.,
if we infer that Tweety flies because Tweety is a bird due to the rule
flies(X) :- bird(X)., then we also want to know the associative concept that
Tweety has wings from the rule haswings(X) :- bird(X). Additionally, grASP
paves the way for implementing ASP without grounding, a major challenge even
today notwithstanding work done by Arias et al. (2018); Marple et al. (2017).

Even though the speed of execution on grASP is slower compared to CLINGO, it
still finds solutions to NP-hard problems in a reasonable time. We plan to
investigate optimizing techniques such as conflict driven clause learning
Silva and Sakallah (2003); Gebser et al. (2007) to speed up execution. grASP
is more than just an ASP solver: its visualization feature makes it suitable
for educational purpose and for debugging. Moreover, a graph-based approach
brings new possibilities for applying optimization. All source code & test
data of this project will be made open to the public.

## References

  * Anger et al. [2001] Christian Anger, Kathrin Konczak, and Thomas Linke.  Nomore: A system for non-monotonie reasoning under answer set semantics.  PSC 802 BOX 14 FPO 09499-0014, page 406, 2001.
  * Arias et al. [2018] Joaquín Arias, Manuel Carro, Elmer Salazar, Kyle Marple, and Gopal Gupta.  Constraint answer set programming without grounding.  Theory and Practice of Logic Programming, 18(3-4):337–354, 2018\.
  * Baral [2003] C. Baral.  Knowledge representation, reasoning and declarative problem solving.  Cambridge University Press, 2003.
  * Eiter et al. [2000] Thomas Eiter, Wolfgang Faber, Nicola Leone, and Gerald Pfeifer.  Declarative problem-solving using the dlv system.  In Logic-based artificial intelligence, pages 79–103. Springer, 2000.
  * Gebser et al. [2007] Martin Gebser, Benjamin Kaufmann, André Neumann, and Torsten Schaub.  Conflict-driven answer set solving.  In IJCAI, volume 7, pages 386–392, 2007.
  * Gebser et al. [2014] Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub.  Clingo = ASP + control: Preliminary report.  CoRR, abs/1405.3694, 2014.
  * Gelfond and Kahl [2014] Michael Gelfond and Yulia Kahl.  Knowledge representation, reasoning, and the design of intelligent agents: The answer-set programming approach.  Cambridge University Press, 2014.
  * Gelfond and Lifschitz [1988] Michael Gelfond and Vladimir Lifschitz.  The stable model semantics for logic programming.  In ICLP/SLP, volume 88, pages 1070–1080, 1988.
  * Hagberg et al. [2008] Aric A. Hagberg, Daniel A. Schult, and Pieter J. Swart.  Exploring network structure, dynamics, and function using networkx.  In Gaël Varoquaux, Travis Vaught, and Jarrod Millman, editors, Proceedings of the 7th Python in Science Conference, pages 11 – 15, Pasadena, CA USA, 2008.
  * Johnson [1975] Donald B Johnson.  Finding all the elementary circuits of a directed graph.  SIAM Journal on Computing, 4(1):77–84, 1975.
  * Konczak et al. [2005] Kathrin Konczak, Thomas Linke, and Torsten Schaub.  Graphs and colorings for answer set programming.  arXiv preprint cs/0502082, 2005.
  * Lifschitz and Turner [1994] Vladimir Lifschitz and Hudson Turner.  Splitting a logic program.  In ICLP, volume 94, pages 23–37, 1994.
  * Linke and Sarsakov [2005] Thomas Linke and Vladimir Sarsakov.  Suitable graphs for answer set programming.  In International Conference on Logic for Programming Artificial Intelligence and Reasoning, pages 154–168. Springer, 2005.
  * Marek and Truszczyński [1999] Victor W Marek and Miroslaw Truszczyński.  Stable models and an alternative logic programming paradigm.  In The Logic Programming Paradigm, pages 375–398. Springer, 1999\.
  * Marple et al. [2017] Kyle Marple, Elmer Salazar, and Gopal Gupta.  Computing stable models of normal logic programs without grounding.  arXiv preprint arXiv:1709.00501, 2017.
  * Silva and Sakallah [2003] João P Marques Silva and Karem A Sakallah.  Grasp—a new search algorithm for satisfiability.  In The Best of ICCAD, pages 73–89. Springer, 2003.
  * Simons et al. [2002] Patrik Simons, Ilkka Niemelä, and Timo Soininen.  Extending and implementing the stable model semantics.  Artificial Intelligence, 138(1-2):181–234, 2002.