#  Technical Report
Modeling Variations of First-Order Horn Abduction
in Answer Set Programming

Peter Schüller,
Computer Engineering Department, Faculty of Engineering
Marmara University, Turkey
<EMAIL_ADDRESS>This work is a significant extension of [47];
major additions are preference relations $\textsc{C}oh$ and $\textsc{W}a$,
revised encodings, increase performance, on-demand constraints, and flexible
value invention. This work has been supported by Scientific and Technological
Research Council of Turkey (TUBITAK) Grant 114E777.

###### Abstract

We study abduction in First Order Horn logic theories where all atoms can be
abduced and we are looking for preferred solutions with respect to three
objective functions: cardinality minimality, coherence, and weighted
abduction. We represent this reasoning problem in Answer Set Programming
(ASP), in order to obtain a flexible framework for experimenting with global
constraints and objective functions, and to test the boundaries of what is
possible with ASP. Realizing this problem in ASP is challenging as it requires
value invention and equivalence between certain constants, because the Unique
Names Assumption does not hold in general. To permit reasoning in cyclic
theories, we formally describe fine-grained variations of limiting
Skolemization. We identify term equivalence as a main instantiation
bottleneck, and improve the efficiency of our approach with on-demand
constraints that were used to eliminate the same bottleneck in state-of-the-
art solvers. We evaluate our approach experimentally on the ACCEL benchmark
for plan recognition in Natural Language Understanding. Our encodings are
publicly available, modular, and our approach is more efficient than state-of-
the-art solvers on the ACCEL benchmark.

##  1 Introduction

Abduction [44] is reasoning to the best explanation, which is an important
topic in diverse areas such as diagnosis, planning, and natural language
understanding (NLU).

We here focus on a variant of abduction, used in NLU, where the primary
concern is to find an explanation of a given input (sentence) with respect to
an objective function. Knowledge is expressed in First Order (FO) Horn logic
axioms. For example ‘a father of somebody is male’ can be expressed as
follows, where capital letters are variables which are universally quantified
unless explicitly indicated otherwise.

$\displaystyle\mathit{inst}(X,\mathit{male})\,{\Leftarrow}\,\mathit{fatherof}(X,Y).$

Abduction aims to find a set of explanatory atoms that make a set of goal
atoms true with respect to a background theory (i.e., a set of axioms). If
$\mathit{inst}(\mathit{tom},\mathit{male})$ is part of a goal then abduction
can explain this goal atom with the atom
$\mathit{fatherof}(\mathit{tom},\mathit{mary})$ where $\mathit{mary}$ is
another person of interest. Using abduction, we can interpret whole natural
language texts, for example ‘Mary lost her father. She is depressed.’ can be
interpreted using knowledge about losing a person, death of a person, and
being depressed, such that we obtain an abductive explanation that represents
‘Mary’s father died, and this is the reason for her depression’.

Abductive reasoning in FO Horn logic yields an infinite space of potential
inferences, because backward reasoning over axioms can produce existentially
quantified variables, which can introduce new terms (value invention). For
example the above axiom is transformed as follows.

$\displaystyle\mathit{inst}(X,\mathit{male})\Rightarrow\exists
Y:\mathit{fatherof}(X,Y).$

To achieve decidability, we need to limit value invention, which leads to a
challenging trade-off: the more we limit value invention, the more
(potentially optimal) solutions we lose.

A second challenge in FO logic is, that terms (input and invented) can be
equivalent to other terms. Equivalent terms make distinct atoms equivalent,
which is used in an inference called _factoring_. In the above example, we can
say that $\mathit{is}(\mathit{mary},\mathit{depressed})$ is factored with
$\mathit{is}(\mathit{she},\mathit{depressed})$ under the assumption that the
equivalence $\mathit{mary}\,{=}\,\mathit{she}$ holds.

A crucial issue when using abduction for NLU is the choice of an appropriate
_preference_ among possible abductive explanations. _Cardinality minimality_
of the set of abduced atoms is a frequently used preference, however in NLU
two other preferences have turned out to be more effective: _coherence_ [42,
41], and _weighted abduction_ [49, 28, 48], which are based on a proof graph
induced by back-chaining and unification operations.

Several tools for realizing abduction with such preferences exist: Phillip,
based on Integer Linear Programming (ILP) [52] and its precursor Henry-n700
[29] as well as an approach based on Markov Logic [5]. The problem of
termination is solved in [5] by instantiating existential terms only with
terms from the input (no value invention), while [29, 52] solves the issue by
inventing a new term only if no previously invented term is present in the
head of the axiom.

Unfortunately, using only input terms eliminates many valid solutions in NLU
applications, for example when processing a text about a son and a
grandfather, we would be unable to perform reasoning about the father (because
it does not exist as a constant). The alternative approach of blocking value
invention if an invented value is involved in the rule improves the situation,
however it is an ad hoc solution and its implications on solution quality have
not been formally or experimentally analyzed.

In addition to decidability issues, global consistency constraints are
necessary to yield practically meaningful abductive explanations, however
existing solvers Henry-n700 and Phillip realize each possible form of a global
constraint (e.g., unique slot values) in a separate checking procedure and
make it difficult to experiment with additional constraints.

Towards overcoming some of these problems, we realize abduction in the
declarative formalism of Answer Set Programming (ASP) [36] which allows
modular modeling of combinatorial problems based on clearly defined formal
semantics. Primary motivation for this work is to obtain a more flexible
framework where variations of Skolemization, objective functions and global
constraints on abduction can be studied easily and where novel preferences can
be studied, such as [46] that can comfortably be represented in ASP but not in
other solvers. Our secondary motivation is, to use ASP for realizing a task
that it is not typically used for, and to study how far we can go in this
task.

Realizing FO Horn abduction in ASP poses further challenges for the following
reasons:  (i) ASP semantics is based on the Unique Names Assumption (UNA),
which means that distinct terms cannot be equivalent (e.g.,
$\mathit{mary}=\mathit{she}$ is not expressible in a built-in feature of ASP);
moreover  (ii) ASP rules have no built-in support for existential variables in
rule heads, which is necessary for value invention during back-chaining as
shown above. In particular, Skolemization using function symbols, i.e.,
replacing $\exists Y:\mathit{fatherof}(X,Y)$ by $\mathit{fatherof}(X,sk(X))$
where $sk$ is a new function symbol, does not guarantee a finite
instantiation.

We tackle the above challenges and present an ASP framework for solving FO
Horn abduction problems for objective functions weighted abduction, coherence,
and cardinality minimality. We describe insights on the structure of the
problem as well as insights on the efficiency of straightforward versus more
involved ASP formulations. Our formulation allows a fine-grained configuration
of Skolemization for tackling cyclic background theories, moreover it permits
the usage of global constraints of any form that is expressible in ASP.
Experiments show, that our framework is faster than the state-of-the-art
solver Phillip [52] on the Accel benchmark [43] for plan recognition in NLU.

In detail, we make the following contributions.

  * •

We provide a novel uniform formalization of abduction with preference
relations weighted abduction, coherence, and cardinality minimality (Section
2).

  * •

We present an ASP encoding that realizes back-chaining in ASP by
deterministically representing an abductive proof graph and guessing which
parts of that graph to use. For value invention we use uninterpreted function
terms, and we explicitly represent an equivalence relation between terms to
model unification (Section 3.2).

  * •

We describe canonicalization operations on proof graphs, show that they do not
eliminate optimal solutions, and use these transformations for encoding
factoring efficiently (Section 3.3).

  * •

We present an alternative ASP encoding which does not represent a proof graph,
instead it generates abduced atoms, defines truth using axioms, and tests if
goals are reproduced (Section 3.4).

  * •

We give ASP encodings for realizing the objective functions weighted
abduction, coherence, and cardinality minimality (Section 3.5).

  * •

We study an alternative method for value invention by replacing uninterpreted
function terms with external computations. This provides us with a fine-
grained control over Skolemization, which is more flexible than state-of-the-
art solutions for achieving decidability. We formalize this extension using
the HEX formalism, and show termination guarantees for arbitrary (i.e.,
including cyclic) knowledge bases (Section 4.1).

  * •

We apply a technique used to increase performance of the Henry-n700 solver
[29] for weighted abduction to our encodings by introducing on-demand
constraints for transitivity of the equivalence relation and for ensuring
acyclicity of the proof graph. We formalize this using HEX and describe an
algorithm for computing optimal models in the presence of on-demand
constraints using the Python API of Clingo [25] (Section 4.2).

  * •

We perform computational experiments on the Accel benchmark [43] where we
measure and discuss resource consumption in terms of space, time, and solver-
internal statistics, as well as solution quality in terms of the objective
function (Section 5). For experimental evaluation we use the Python API of
Clingo, Gringo [23] with either Clasp [22] or Wasp [2], and the Phillip [52]
solver for weighted abduction which is based on C++ and Integer Linear
Programming (ILP).

We discuss related work in Section 6 and conclude in Section 7.

Appendices provide additional information: all ASP encodings in their complete
version; verbose listing of rewriting and answer set of the running example;
proofs for correctness of encodings; and algorithms for realizing on-demand
constraints.

Our framework, including experimental instances and algorithms, is available
online.111https://bitbucket.org/knowlp/asp-fo-abduction

##  2 Preliminaries

We give a brief introduction of abduction in general and variations of First
Order Horn abduction as used in Natural Language Processing, describe the
Accel benchmark which contains instances of such reasoning problems, and give
preliminaries of ASP and HEX.

In the following, in logical expressions and ASP rules we write variables
starting with capital letters and constants starting with small letters.

###  2.1 Abduction and Preferences on Abductive Explanations

Abduction, originally described in [44], can be defined logically as follows:
given a set $B$ of background knowledge axioms and an observation $O$, find a
set $H$ of hypothesis atoms such that $B$ and $H$ are consistent and reproduce
the observation, i.e., $B\,{\cup}\,H\not\models\bot$ and $B\,{\cup}\,H\models
O$. In this work we formalize axioms and observations in First Order logic:
the observation $O$ (also called ‘goal’) is an existentially quantified
conjunction of atoms

$\exists
V_{1},\ldots,V_{k}:o_{1}(V_{1},\ldots,V_{k})\,{\land}\,\cdots\,{\land}\,o_{m}(V_{1},\ldots,V_{k})$
(1)

and an axiom in $B$ is a Horn clause of form

$q(Y_{1},\ldots,Y_{m})\,\,{\Leftarrow}\,\,p_{1}(X^{1}_{1},\ldots,X^{1}_{k_{1}})\,{\land}\,\cdots\,{\land}\,p_{r}(X^{r}_{1},\ldots,X^{r}_{k_{r}}).$
(2)

where
$\mathcal{X}=\bigcup_{1\,{\leq}\,i\,{\leq}\,r}\bigcup_{1\,{\leq}\,j\,{\leq}\,k_{r}}X^{i}_{j}$
is the set of variables in the body,
$\mathcal{Y}=\bigcup_{1\,{\leq}\,i\,{\leq}\,m}Y_{i}$ is the set of variables
in the head, $\mathcal{Y}\,{\subseteq}\,\mathcal{X}$ and we implicitly
quantify universally over $\mathcal{X}$. In the variant of abduction we
consider here, the set $H$ of hypotheses can contain any predicate from the
theory $B$ and the goal $O$, hence existence of a solution is trivial. A
subset $S$ of constants from $B$ is declared as ‘sort names’ that cannot be
equivalent with other constants. Given $B$, $O$, and $S$, we call the tuple
$(B,O,S)$ an _abduction instance_. Unless otherwise indicated, we assume that
$B$ is acyclic.

######  Example 1 (Running Example).

Consider the following text

‘ _Mary lost her father. She is depressed._ ’

which can be encoded as the following observation, to be explained by
abduction.

$\displaystyle\mathit{name}(m,\mathit{mary}){\wedge}\mathit{lost}(m,f){\wedge}\mathit{fatherof}(f,m){\wedge}\mathit{inst}(s,\mathit{female}){\wedge}\mathit{is}(s,\mathit{depressed})$
(3)

Given the set of axioms

$\displaystyle\mathit{inst}(X,\mathit{male})$ $\displaystyle\,{\Leftarrow}\,$
$\displaystyle\mathit{fatherof}(X,Y)$ (4)
$\displaystyle\mathit{inst}(X,\mathit{female})$
$\displaystyle\,{\Leftarrow}\,$ $\displaystyle\mathit{name}(X,\mathit{mary})$
(5) $\displaystyle\\!\\!\\!\\!\mathit{importantfor}(Y,X)$
$\displaystyle\,{\Leftarrow}\,$ $\displaystyle\mathit{fatherof}(Y,X)$ (6)
$\displaystyle\mathit{inst}(X,\mathit{person})$
$\displaystyle\,{\Leftarrow}\,$ $\displaystyle\mathit{inst}(X,\mathit{male})$
(7) $\displaystyle\mathit{is}(X,\mathit{depressed})$
$\displaystyle\,{\Leftarrow}\,$
$\displaystyle\mathit{inst}(X,\mathit{pessimist})$ (8)
$\displaystyle\mathit{is}(X,\mathit{depressed})$
$\displaystyle\,{\Leftarrow}\,$
$\displaystyle\mathit{is}(Y,\mathit{dead})\,{\land}\,\mathit{importantfor}(Y,X)$
(9) $\displaystyle\mathit{lost}(X,Y)$ $\displaystyle\,{\Leftarrow}\,$
$\displaystyle\mathit{is}(Y,\mathit{dead})\,{\land}\,\mathit{importantfor}(Y,X)\,{\land}\,\mathit{inst}(Y,\mathit{person})$
(10)

and sort names

$\displaystyle\mathit{person}\quad\mathit{male}\quad\mathit{female}\quad\mathit{dead}\quad\mathit{depressed}$
(11)

we can use abduction to conclude the following: (a) loss of a person here
should be interpreted as death, (b) ‘she’ refers to Mary, and (c) her
depression is because of her father’s death because her father was important
for her.

We obtain these because we can explain (3) by the following abductive
explanation which contains atoms and equivalences.

$\displaystyle\mathit{name}(m,\mathit{mary})\quad\mathit{fatherof}(f,m)\quad\mathit{is}(f,\mathit{dead})\quad
m=s$ (12)

The first two atoms directly explain goal atoms. We can explain the remaining
goal atoms using inference from rules and factoring (which represents
unification in a certain reasoning direction).

$\displaystyle\mathit{inst}(f,\mathit{male})$ [infered via (4) using (12)]
(13) $\displaystyle\mathit{inst}(m,\mathit{female})$ [infered via (5) using
(12)] (14) $\displaystyle\mathit{inst}(s,\mathit{female})$ [goal, factored
from (14) using (12)] $\displaystyle\mathit{importantfor}(f,m)$ [infered via
(6) using (12)] (15) $\displaystyle\mathit{inst}(f,\mathit{person})$ [infered
via (7) using (13)] (16) $\displaystyle\mathit{is}(m,\mathit{depressed})$
[infered via (9) using (12) and (15)] (17)
$\displaystyle\mathit{is}(s,\mathit{depressed})$ [goal, factored from (17)
using (12)] $\displaystyle\mathit{lost}(m,f)$ [goal, infered via (10) using
(12), (15), and (16)] (18)

Note that there are additional possible inferences but they are not necessary
to explain the goal atoms. Moreover, there are several other abductive
explanations, for example to abduce all goal atoms, or to abduce
$\mathit{inst}(m,\mathit{pessimist})$ and $\mathit{lost}(m,f)$ instead of
abducing $\mathit{is}(f,\mathit{dead})$. $\square$

Preferred explanations. In the presence of multiple possible explanations, we
are naturally interested in obtaining a set of _preferred_ explanations. In
this work we consider three preference formulations:  ($\textsc{C}ard$)
cardinality-minimality of abduced atoms,  ($\textsc{C}oh$) ‘coherence’ as
described in [43] and in slight variation in more detail in [42], and
($\textsc{W}a$) ‘weighted abduction’ as initially formulated in [28].

$\textsc{C}oh$ is based on connectedness between observations and
explanations, while $\textsc{W}a$ finds a trade-off between least-specific and
most-specific abduction, depending on the explanatory power of more specific
atoms. Both objective functions are based on an inference procedure that
induces a proof graph by means of backchaining and unification.

Towards formalizing these preference functions, we next formalize such an
inference procedure. The following definitions are based on [49, 30] but
additionally define an explicit proof graph corresponding to the inferences
leading to a hypothesis. Here we consider only single-head axioms.

######  Definition 1.

A _hypothesis_ is a conjunction of atoms or equivalences between terms. Given
an abduction instance $A\,{=}\,(B,O,S)$ the set $\hat{\mathcal{H}}(A)$ of all
hypotheses of $A$ is the largest set containing hypotheses obtained by
extending $\mathcal{H}\,{=}\,\\{O\\}$ using back-chaining and unification.

_Back-chaining_ : given an atom $P$ which is part of a hypothesis
($P\,{\in}\,H$, $H\,{\in}\,\mathcal{H}$), such that $P$ unifies with the head
$Q\,{=}\,q(Y_{1},\ldots,Y_{m})$ of an axiom $\eqref{eqAx}$ with substitution
$\theta$, back-chaining adds to $\mathcal{H}$ a new hypothesis
$H\,{\land}\,P_{1}^{\prime}\,{\land}\,\cdots\,{\land}\,P_{r}^{\prime}$, where
$P_{i}^{\prime}$ is the substituted version
$\theta(p_{i}(X^{i}_{1},\ldots,X^{i}_{k_{i}})$ of the $i$-th body atom of
axiom (2).

_Unification_ : given hypothesis $H\,{\in}\,\mathcal{H}$ with distinct atoms
$P,Q\,{\in}\,H$ that unify under substitution $\theta$ such that all
$X\,{\mapsto}\,Y\,{\in}\,\theta$ obey $X,Y\,{\notin}\,S$, unification adds
hypothesis
$H{\wedge}\bigwedge\\{X\,{=}\,Y\,{\mid}\,X\,{\mapsto}\,Y\,{\in}\,\theta\\}$ to
$\mathcal{H}$.

Note that $\hat{\mathcal{H}}(A)$ is potentially infinite. We sometimes leave
$A$ implicit.

######  Example 2 (continued).

Three hypotheses for the abduction instance in Example 1 are  (a) the original
goal $G$ as shown in (3), which intuitively means that we do not justify any
atom in the goal by inference, instead we abduce all atoms in the goal;  (b)
the hypothesis $G\wedge\mathit{is}(f,\mathit{dead})\wedge
m\,{=}\,s\wedge\mathit{inst}(f,\mathit{male})\wedge\mathit{inst}(m,\mathit{female})\wedge\mathit{importantfor}(f,m)\wedge\mathit{inst}(f,\mathit{person})\wedge\mathit{is}(m,\mathit{depressed})$
which corresponds to (13)–(18) and includes the abductive explanation (12);
and  (c) the hypothesis $G\wedge\mathit{name}(s,\mathit{mary})\wedge
m\,{=}\,s\wedge\mathit{inst}(f,\mathit{person})\wedge\mathit{inst}(f,\mathit{male})\wedge\mathit{fatherof}(f,n_{2})\wedge
m\,{=}\,n_{2}\wedge\mathit{is}(n_{1},\mathit{dead})\wedge
f\,{=}\,n_{1}\wedge\mathit{is}(f,\mathit{dead})\wedge\mathit{importantfor}(f,m)\wedge\mathit{importantfor}(n_{1},m)$
which applies Skolemization during back-chaining and represents a variation of
explanation (12). Details about this hypothesis can be found in Example 3 and
in Figure 1.  $\square$

A hypothesis $H\,{\in}\,\hat{\mathcal{H}}$ does not contain any information
about how it was generated. For the purpose of describing the cost function
formally, we define proof graphs $G$ wrt. hypotheses $H$.

######  Definition 2.

Given an abduction instance $A\,{=}\,(B,O,S)$, a _proof graph_ $G$ wrt. a
hypothesis $H\\!\,{\in}\,\hat{\mathcal{H}}(A)$ is an acyclic directed graph
consisting of nodes $N(G)\,{=}\,\\{P\,{\in}\,H\,{\mid}\,P\text{ is not an
equality}\\}$ and edges $E(G)$ are recursively defined by the inference
operations used to generate atoms $P\,{\in}\,H$:  (a) back-chaining of $P$
induces an edge from all body atoms $P_{i}^{\prime}$ to $P$, and  (b)
unification of $P$ with $Q$ induces either an edge from $P$ to $Q$ or an edge
from $Q$ to $P$.

We denote by $A(G)\,{=}\,\\{a\,{\in}\,N(G)\,{\mid}\,\nexists
b:(b,a)\,{\in}\,E(G)\\}$ the set of nodes that are neither back-chained nor
unified. Note that the term ‘factoring’ is used to denote unification with
direction, this is discussed in detail in [49]. There can be multiple proof
graphs with respect to a single hypothesis, and these graphs differ only by
factoring directions. Figure 1 depicts a proof graph which is discussed in
Example 3.

Intuitively, an edge in the proof graph shows how an atom is justified: by
inference over an axiom (backchaining) or by equivalence with another atom
(factoring).

Equipped with these definitions, we next formalize the objective functions of
interest.

######  Definition 3.

Given a proof graph $G$ wrt. a hypothesis $H$ of an abduction instance
$(B,O,S)$,

  * •

$\textsc{C}ard\,{=}\,|A(G)|$,

  * •

$\textsc{C}oh\,{=}\,|\\{(a,b)\,{\mid}\,a,b\,{\in}\,O,a\,{<}\,b$, and $\nexists
n\,{\in}\,N(G)$ such that from $n$ we can reach both $a$ and $b$ in $G\\}|$
where the relation $\,{<}\,$ is an arbitrary fixed total order over $O$ (e.g.,
lexicographic order),

  * •

$\textsc{W}a\,{=}\,\sum_{a\,{\in}\,A(G)}\min\mathit{cost}(a)$, where
$\mathit{cost}\ {:}\ N(G)\to 2^{\mathbb{R}}$ labels each atom in the graph
with a set of cost values.

For the definition of $\mathit{cost}$ in $\textsc{W}a$ we require that each
axioms of form (2) has weights $w_{1},\ldots,w_{r}$ corresponding to its body
atoms, and initial costs $ic(o)$ for each observation $o\,{\in}\,O$.

Then $\mathit{cost}$ is initialized with $\emptyset$ for each node and
recursively defined as follows:

  * •

goal nodes $o\,{\in}\,O$ obtain cost
$\mathit{cost}(o)\,{=}\,\mathit{cost}(o)\,{\cup}\,\\{ic(o)\\}$;

  * •

if $P$ was back-chained with an axiom with body atoms
$P_{1}^{\prime},\ldots,P_{r}^{\prime}$ and $c\,{=}\,\min\,\mathit{cost}(P)$,
then $c$ is added to each body atom $P_{i}^{\prime}$ after adjusting it using
the respective cost multiplier $w_{i}$, formally
$\mathit{cost}(P_{i}^{\prime})\,{=}\,\mathit{cost}(P_{i}^{\prime})\,{\cup}\,\\{c\,{\cdot}\,w_{i}\\}$
for $1\,{\leq}\,i\,{\leq}\,r$;

  * •

if $P$ was unified with $Q$ such that there is a factoring edge
$(Q,P)\,{\in}\,G$ from $Q$ to $P$, then we add the smallest cost at $P$ to
$Q$:
$\mathit{cost}(Q)\,{=}\,\mathit{cost}(Q)\,{\cup}\,\\{\min\mathit{cost}(P)\\}$.

Note that the formalization in [30, above (1)] assigns unification cost to the
equality, but does not use that cost in case of multiple unifications, hence
we do not use such a formalization. Moreover, deleting cost values from the
hypothesis with higher cost in a unification (as shown in [30, Fig. 1,
‘Output’ vs ‘Backward-chaining’]) contradicts the formalization as a cost
‘function’ that maps hypotheses to costs. Therefore our formalization defines
$\mathit{cost}$ to map from atoms in a hypothesis to multiple ‘potential’
costs of that hypothesis. Note that due to acyclicity of the graph, no cost in
$\mathit{cost}$ recursively depends on itself, and that back-chaining can
create hypothesis atoms containing a part of the goal, therefore goal nodes
can have a cost lower than that goal’s initial cost (e.g.,
$\mathit{fatherof}(f,m)$ in Figure 1).

$\mathit{inst}(s,\mathit{female})^{\underline{100\$}}$$\mathit{name}(s,\mathit{mary})^{\textbf{120\$}}$$\mathit{name}(m,\mathit{mary})^{\underline{100\$},\,\textit{120\$}}$$\mathit{inst}(f,\mathit{person})^{\textbf{40\$}}$$\mathit{inst}(f,\mathit{male})^{\textbf{48\$}}$$\mathit{fatherof}(f,n_{2})^{\textbf{57\$}}$$\mathit{lost}(m,f)^{\underline{100\$}}$$\mathit{is}(s,\mathit{depressed})^{\underline{100\$}}$$\mathit{is}(n_{1},\mathit{dead})^{\textbf{60\$}}$$\mathit{is}(f,\mathit{dead})^{\textbf{40\$},\,\textit{60\$}}$$\mathit{importantfor}(n_{1},m)^{\textbf{60\$}}$$\mathit{importantfor}(f,m)^{\textbf{40\$},\,\textit{60\$}}$$\mathit{fatherof}(f,m)^{\textbf{48\$},\,\textit{57\$},\,\underline{100\$}}$(10)factor
$f\,{=}\,n_{1}$(7)(4)factor $f\,{=}\,n_{1}$factor $m\,{=}\,n_{2}$ (6)factor
$m\,{=}\,s$(5)(9)abducedcostsgoalcostsothercosts

Figure 1: Abductive proof graph of Example 1 including costs of nodes for
$\textsc{W}a$. Edges annotated with (X) are inference edges induced by back-
chaining over axiom (X). We underline initial goal costs, use italic font for
factoring costs, and bold font for back-chaining costs.

The formalization in this section was done to provide a basis for showing
correctness of canonicalization operations on proof graphs and for showing
correctness of ASP encodings. To the best of our knowledge, no precise formal
description of proof graphs and associated costs of $\textsc{C}oh$ and
$\textsc{W}a$ exists in the literature, therefore we here attempt to formally
capture the existing descriptions [43, 28, 29].

######  Example 3 (continued).

The proof graph of Example 1 is depicted in Figure 1 where we also show the
set of costs of each node using objective $\textsc{W}a$. The total cost of
this graph is $100\$\,{+}\,48\$\,{+}\,40\$\,{=}\,188\$$. Objective
$\textsc{C}ard$ has cost $3$ because we abduce 3 atoms, and objective
$\textsc{C}oh$ has cost $6$: let goal node set
$A\,{=}\,\\{\mathit{inst}(s,\mathit{female})$,
$\mathit{name}(m,\mathit{mary})\\}$ and $B\,{=}\,\\{\mathit{fatherof}(f,m)$,
$\mathit{lost}(m,f)$, $\mathit{is}(s,\mathit{depressed})\\}$, then nodes
within $A$ and within $B$ are reachable from some node, however pairs
$\\{(a,b)\,{\mid}\,a\,{\in}\,A,b\,{\in}\,B\\}$ of nodes are not reachable from
any node, and each of these $|A|\cdot|B|\,{=}\,6$ pairs incurs cost 1.
$\square$

Note that in this work we consider only hypotheses and proof graphs where an
atom is either justified by a single inference, or by a single factoring, or
not at all (then it is abduced).

##### Computational Complexity.

Existence of an abductive explanation is trivial, because we can abduce any
atom and the goal is the trivial explanation. However, finding the optimal
abductive explanation with respect to an objective function is not trivial.
With unlimited value invention and cyclic theories the problem of finding the
optimal explanation is undecidable, as we cannot bound the size of the proof
graph or the number of additionally required constants for finding the optimal
solution.

To the best of our knowledge, the computational complexity of deciding whether
an abductive explanation is optimal wrt. one of the objective functions
$\textsc{C}ard$, $\textsc{C}oh$, and $\textsc{W}a$, has not been formally
studied so far, although for $\textsc{C}ard$ related results exist. Section 6
discusses related complexity results.

###  2.2 Accel Benchmark

The Accel benchmark222Available at ftp://ftp.cs.utexas.edu/pub/mooney/accel .
[43, 41] contains a knowledge base with 190 axioms of form (2), defines a set
of sort names that observe the UNA, and contains 50 instances (i.e., goals)
with between 5 and 26 atoms in a goal (12.6 atoms on average). Axioms contain
a single head and bodies vary between 1 and 11 atoms (2.2 on average). Accel
axioms contain no weights and goal atoms contain no initial costs. For
experiments with $\textsc{W}a$ we follow existing practice (cf. [29]) and set
initial costs to $ic(o)\,{=}\,100\$$ for all $o\,{\in}\,O$ and for each axiom
we set weights to sum up to $1.2$, i.e., we set $w_{i}\,{=}\,1.2/r$,
$1\,{\leq}\,i\,{\leq}\,r$.

In addition to axioms, goals, and sort names, Accel contains constraints that
forbid certain combinations of atoms to become abduced at the same time
(assumption nogoods) and constraints that enforce functionality for certain
predicate symbols (unique slot axioms). We next give two examples.

######  Example 4.

An example for an assumption nogood is, that we are not allowed to abduce an
event $G$ to be part of a ‘go’ event $S$, and at the same time abduce that a
person $P$ is the ‘goer’ of $G$.

$\displaystyle\not\exists
S,G,P:\\{\mathit{go\\_step}(S,G),\mathit{goer}(G,P)\\}\,{\in}\,H\text{ for all
$H\,{\in}\,\hat{\mathcal{H}}$}$ (19)

An example for a unique slot axiom is, that the ‘goer’ of an event must be
unique.

$\displaystyle\not\exists G,P_{1},P_{2}:P_{1}\neq
P_{2}\,{\land}\,\\{\mathit{goer}(G,P_{1}),\mathit{goer}(G,P_{2})\\}\,{\in}\,H\text{
for all $H\,{\in}\,\hat{\mathcal{H}}$}$ (20)

$\square$

###  2.3 Answer Set Programming

We assume familiarity with ASP [26, 36, 18, 24] and give only brief
preliminaries of HEX programs [14] which extend the ASP-Core-2 standard [7].
We will use programs with (uninterpreted) function symbols, aggregates,
choices, and weak constraints.

Syntax. Let $\mathcal{C}$, $\mathcal{X}$, and $\mathcal{G}$ be mutually
disjoint sets of _constants_ , _variables_ , and _external predicate_ names,
which we denote with first letter in lower case, upper case, and starting with
‘ & ’, respectively. Constant names serve as constant terms, predicate names,
and names for uninterpreted functions. The set of _terms_ $\mathcal{T}$ is
recursively defined, it is the smallest set containing
$\mathbb{N}\,{\cup}\,\mathcal{C}\,{\cup}\,\mathcal{X}$ as well as
uninterpreted function terms of form $f(t_{1},\ldots,t_{n})$ where
$f\,{\in}\,\mathcal{C}$ and $t_{1},\ldots,t_{n}\,{\in}\,\mathcal{T}$. An
ordinary atom is of the form $p(t_{1},\dots,t_{n})$, where
$p\,{\in}\,\mathcal{C}$, $t_{1},\dots,t_{n}\,{\in}\,\mathcal{T}$, and $n\geq
0$ is the _arity_ of the atom. An aggregate atom is of the form
$X\,{=}\,\\#\mathit{agg}\\{\ e_{1};\ldots;e_{k}\ \\}$ with variable
$X\,{\in}\,\mathcal{X}$, aggregation function
$\\#\mathit{agg}\,{\in}\,\\{\\#\mathit{min},\\#\mathit{max}\\}$,
$k\,{\geq}\,1$ and each aggregate element $e_{i}$, $1\,{\leq}\,i\,{\leq}\,k$,
is of the form $t\,{:}\,a$ or $t$ with $t\,{\in}\,\mathcal{T}$ and $a$ an
atom. An external atom is of the form
$\text{{{\&}}}\\!\mathit{f}[y_{1},\dots,y_{n}](x_{1},\dots,x_{m})$, where
$y_{1},\dots,y_{n},x_{1},\dots,x_{m}\,{\in}\,\mathcal{T}$ are two lists of
terms (called input and output lists, resp.), and
$\text{{{\&}}}\\!\mathit{f}\in\mathcal{G}$ is an external predicate name. An
external atom provides a way for deciding the truth value of an output tuple
depending on the input tuple and a given interpretation. A term or atom is
ground if it contains no sub-terms that are variables.

A rule $r$ is of the form
$\alpha_{1}\lor\cdots\lor\alpha_{k}\leftarrow\beta_{1},\dots,\beta_{n},\mathbf{not}\,\beta_{n+1},\dots,\mathbf{not}\,\beta_{m}$
where $m,k\geq 0$, $\alpha_{i}$, $0\,{\leq}\,i\,{\leq}\,k$ is an ordinary atom
and $\beta_{j}$, $0\,{\leq}\,j\,{\leq}\,m$ is an atom, and we let
$H(r)=\\{\alpha_{1},\ldots,\alpha_{k}\\}$ and
$B(r)=\\{\beta_{1},\dots,\beta_{n},\mathbf{not}\,\beta_{n\,{+}\,1},\dots,\mathbf{not}\,\beta_{m}\\}$.
A program is a finite set $P$ of rules. A rule $r$ is a constraint, if
$k\,{=}\,0$ and $m\,{\neq}\,0$, and a fact if $m\,{=}\,0$.

A weak constraint is of form
${\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}}\,\beta_{1},\dots,\beta_{n},\mathbf{not}\,\beta_{n+1},\dots,\mathbf{not}\,\beta_{m}.\
[w@1,t_{1},\ldots,t_{k}]$ where all $\beta_{j}$ are atoms, and all $t_{i}$ are
terms such that each variable in some $t_{i}$ is contained in some $\beta_{j}$
(note that $1$ in $w@1$ shows the ‘level’ which we do not use).

Semantics. Semantics of a HEX program $P$ are defined using its Herbrand Base
$\mathit{H\\!B}_{P}$ and its ground instantiation $\mathit{grnd}(P)$. An
aggregate literal in the body of a rule accumulates truth values from a set of
atoms, e.g., $C\,{=}\,\\#min\\{4;2:p(2)\\}$ is true wrt. an interpretation
$I\,{\subseteq}\,\mathit{H\\!B}_{P}$ iff $p(2)\,{\in}\,I$ and $C\,{=}\,2$ or
$p(2)\,{\notin}\,I$ and $C\,{=}\,4$. Using the usual notion of satisfying a
rule given an interpretation, the FLP-reduct [21] $fP^{I}$ reduces a program
$P$ using an answer set candidate $I$:
$fP^{I}\,{=}\,\\{r\,{\in}\,\mathit{grnd}(P)\,{\mid}\,I\,{\models}\,B(r)\\}$.
$I$ is an answer set of $P$ ($I\,{\in}\,\mathit{AS}(P)$) iff $I$ is a minimal
model of $fP^{I}$. Weak constraints define that an answer set $I$ has cost
equivalent to the term $w$ for each distinct tuple $t_{1},\ldots,t_{k}$ of
constraints that have a satisfied body wrt. $I$. Answer sets of the lowest
cost are preferred.

Safety and Splitting. Programs must obey _syntactic safety restrictions_ (see
[7]) to ensure a finite instantiation. In presence of loops over external
atoms, HEX programs additionally must obey restrictions to ensure finite
instantiation. A _splitting set_ [38] of a program $P$ is any set $U$ of
literals such that, for every rule $r\,{\in}\,P$, if
$H(r)\,{\cap}\,U\,{\neq}\,\emptyset$ then $B(r)\,{\subseteq}\,U$. The set of
rules $r\,{\in}\,P$ such that $B(r)\,{\subseteq}\,U$ is called the bottom
$b_{U}(P)$ of $P$ relative to $U$. Given splitting set $U$ of program $P$,
$I\,{\in}\,\mathit{AS}(P)$ iff $I\,{=}\,X\,{\cup}\,Y$ where
$X\,{\cap}\,Y\,{=}\,\emptyset$, $X\,{\in}\,\mathit{AS}(b_{U}(P))$, and
$Y\,{\in}\,\mathit{AS}(e_{U}(P\setminus b_{U}(P),X))$ where $e_{U}(Q,J)$
partially evaluates $Q$ wrt. $J$. Splitting sets were lifted to HEX in [19,
14].

Syntactic Sugar. Anonymous variables of form ‘$\\_$’ are replaced by new
variable symbols. Choice constructions can occur instead of rule heads, they
generate a set of candidate solutions if the rule body is satisfied; e.g.,
$1\,{\leq}\,\\{p(a);p(b);p(c)\\}\,{\leq}\,2$ in the rule head generates all
solution candidates where at least 1 and at most 2 atoms of the set are true.
The bounds can be omitted. In choices, the colon symbol ‘:’ can be used to
generate a list of elements (similar as in aggregates), for example
$\\{p(X):q(X),\mathbf{not}\ r(X)\\}$ encodes a guess over all $p(X)$ such that
$q(X)$ is true and $r(X)$ is not true.

##  3 ASP Encodings

We next describe ASP encodings for modeling abduction with partial UNA and
value invention. All encodings consist of a deterministic part that
instantiates all atoms that can potentially used to build a hypothesis, i.e.,
to justify the goal. Some encodings also explicitly represent inferences
leading to these atoms. All encodings guess an equivalence relation over all
terms in these ‘potentially interesting’ atoms, to handle term equivalence. In
Bwd encodings, the actually used proof graph is nondeterministically guessed,
while encoding Fwd-A performs a guess of abduced atoms and checks if the goals
become true given these atoms. Variations of Bwd encodings perform factoring
in different ways. We next give common aspects of all encodings, then give
each encoding in detail, and finally provide a summary of differences between
encodings (Table 1).

A detailed example containing a rewriting of our running example and an answer
set corresponding to Figure 1 is given in the appendix.

We represent an atom of the form $p(a,b)$ as a term $c(p,a,b)$, which allows
us to quantify over predicates using ASP variables (e.g., $c(P,X,Y)$). We
represent each atom in a goal (1) as a fact

$\displaystyle\mathit{goal}(c(o_{1},v_{1},\ldots,v_{k})).$ (21)

where $v_{i}\,{\notin}\,S$ are constants corresponding to existentially
quantified variables $V_{i}$.

We mark each sort name $s\,{\in}\,S$ using a fact

$\displaystyle\mathit{sortname}(s).$ (22)

######  Example 5 (continued).

Goal and sort names of our running example are represented as

$\displaystyle\mathit{goal}(c(\mathit{name},m,\mathit{mary})).\quad\mathit{goal}(c(\mathit{lost},m,f)).\quad\mathit{goal}(c(\mathit{fatherof},f,m)).$
$\displaystyle\mathit{goal}(c(\mathit{inst},s,\mathit{female})).\quad\mathit{goal}(c(\mathit{is},s,\mathit{depressed})).\quad\mathit{sortname}(\mathit{person}).$
$\displaystyle\mathit{sortname}(\mathit{male}).\quad\mathit{sortname}(\mathit{female}).\quad\mathit{sortname}(\mathit{dead}).\quad\mathit{sortname}(\mathit{depressed}).$

$\square$

###  3.1 Rules common to all encodings

Goals are potential interesting facts, i.e., potential nodes of the proof
graph:

$\displaystyle\mathit{pot}(X)\,{\leftarrow}\,\mathit{goal}(X).$ (23)

Potential interesting facts provide potentially relevant terms in the Herbrand
Universe (HU).

$\displaystyle hu(X)$
$\displaystyle\,{\leftarrow}\,\mathit{pot}(c(\\_,X,\\_)).$ (24) $\displaystyle
hu(X)$ $\displaystyle\,{\leftarrow}\,\mathit{pot}(c(\\_,\\_,X)).$ (25)

Note that (24) and (25) assume, that all atoms in $B$ and $O$ have arity 2.
This assumption is made only in these two rules, which can be generalized
easily to arbitrary arities.

We call terms in HU that are not sort names ‘User HU’, represent them in
predicate $\mathit{uhu}$, and guess a relation $\mathit{eq}$ among pairs of
these terms.

$\displaystyle\mathit{uhu}(X)$
$\displaystyle\,{\leftarrow}\,hu(X),\mathbf{not}\ \mathit{sortname}(X).$ (26)
$\displaystyle\\{\ eq(A,B):\mathit{uhu}(A),\ \mathit{uhu}(B),\ A\,{\neq}\,B\
\\}$ $\displaystyle\,{\leftarrow}\,.$ (27)

Relation $\mathit{eq}$ holds symmetric on HU, and it is a reflexive,
symmetric, and transitive (equivalence) relation.

$\displaystyle eq(A,A)$ $\displaystyle\,{\leftarrow}\,hu(A).$ (28)
$\displaystyle\,{\leftarrow}\,eq(A,B),\mathbf{not}\ eq(B,A).$ (29)
$\displaystyle\,{\leftarrow}\,eq(A,B),eq(B,C),A\,{\neq}\,B,B\,{\neq}\,C,A\,{\neq}\,C,\mathbf{not}\
eq(A,C).$ (30)

Note, that we will later create instantiations of constraint (30) in a lazy
manner (on-demand), therefore we use a constraint to ensure transitivity, and
not a rule.

###  3.2 Bwd: Defining Back-chaining Proof Graph, Guess Active Parts

We next encode the maximal back-chaining proof graph from Definition 2 in ASP
by:  (i) deterministically defining the maximum possible potential proof graph
by back-chaining from the goal and creating new constants when required;  (ii)
guessing which parts of the proof graph are used, i.e., which atoms are back-
chained over which axioms, and which bodies of axioms must therefore be
justified;  (iii) factor atoms with other atoms and mark the remaining atoms
as abduced.

##### Potential Proof Graph.

Building the potential proof graph is realized by rewriting each axiom of form
(2) into a deterministic definition of potential inferences from the axiom’s
head atom, and defining which body atoms become part of the hypothesis due to
such an inference.

We first give this rewriting as an example and then formally.

######  Example 6.

Axiom (9) from our running example is translated into the following rules.

$\displaystyle\mathit{mayInferVia}(r_{1},c(\mathit{is},X,\mathit{depressed}),l(Y))\,{\leftarrow}\,$
$\displaystyle\hskip
160.00024pt\mathit{pot}(c(\mathit{is},X,\mathit{depressed})),Y\,{=}\,s(r_{1},``Y",X).$
(31)
$\displaystyle\mathit{inferenceNeeds}(c(\mathit{is},X,\mathit{depressed}),r_{1},c(\mathit{importantfor},Y,X))\,{\leftarrow}\,$
$\displaystyle\hskip
160.00024pt\mathit{mayInferVia}(r_{1},c(\mathit{is},X,\mathit{depressed}),l(Y)).$
(32)
$\displaystyle\mathit{inferenceNeeds}(c(\mathit{is},X,\mathit{depressed}),r_{1},c(\mathit{is},Y,\mathit{dead}))\,{\leftarrow}\,$
$\displaystyle\hskip
160.00024pt\mathit{mayInferVia}(r_{1},c(\mathit{is},X,\mathit{depressed}),l(Y)).\quad$
(33)

Here $r_{1}$ is a unique identifier for axiom (9). Rule (31) defines all
possible substitutions of the axiom, including value invention via
Skolemization which is represented in the last argument of
$\mathit{mayInferVia}$ in the term $l(\cdots)$. Rules (32) and (33) define
which body atoms become part of the hypothesis because of back-chaining. Note
that Skolemization is here realized with an uninterpreted function term
$s(r_{1},``Y",X)$ that takes as arguments the unique axiom identifier $r_{1}$,
the name of the skolemized existential variable $``Y"$ (to skolemize several
variables in one axiom independently), and all variables (here only $X$) in
the body of the axiom. $\square$

For each body atom that can be added to the hypothesis by an inference,
$\mathit{inferenceNeeds}(\mathit{Head}$, $\mathit{Rule},\mathit{Body})$ is
defined. To allow back-chaining from $\mathit{Body}$, we define
$\mathit{Body}$ as potentially interesting.

$\displaystyle\mathit{pot}(P)\,{\leftarrow}\,\mathit{inferenceNeeds}(\\_,\\_,P)$
(34)

Axioms rewritten as in (31)–(33) together with (23) and (34) form a
deterministic ASP program, that, given a set of goal atoms $\mathit{goal}(A)$,
defines the union of all possible proof graphs.

This graph is finite under the assumption that the knowledge base is acyclic,
i.e., that no circular inferences are possible over all axioms in the
knowledge base. (For reasons of presentation we will maintain this assumption
while presenting the basic encodings and eliminate the assumption in Section
4.1.)

For readability we gave the rewriting in Example 6. Formally, an axiom of form
(2) is rewritten into

$\displaystyle\mathit{mayInferVia}(a,c(q,Y_{1},\ldots,Y_{m}),l(Z_{1},\ldots,Z_{v}))\,{\leftarrow}\,$
$\displaystyle\hskip 50.00008pt\mathit{pot}(c(q,Y_{1},\ldots,Y_{m})),\
Z_{1}\,{=}\,s(a,1,Y_{1},\ldots,Y_{m}),\
\ldots,Z_{v}\,{=}\,s(a,v,Y_{1},\ldots,Y_{m})\quad$
$\displaystyle\mathit{inferenceNeeds}(c(q,Y_{1},\ldots,Y_{m}),a,c(p_{i},X^{i}_{1},\ldots,X^{i}_{k_{i}}))\,{\leftarrow}\,$
(35) $\displaystyle\hskip
50.00008pt\mathit{mayInferVia}(a,c(q,Y_{1},\ldots,Y_{m}),l(Z_{1},\ldots,Z_{v}))\qquad\qquad\text{for
}i\,{\in}\,\\{1,\ldots,r\\}$

where $a$ is a unique identifier for that particular axiom,
$Z_{1},\ldots,Z_{v}\,{=}\,\mathcal{X}\,{\setminus}\,\mathcal{Y}$ is the set of
variables occurring in the body but not in the head, and the second argument
of the uninterpreted function $s(\cdot)$ is a unique identifier for each
skolemized variable in this axiom.

######  Lemma 1.

Given an abduction instance $A\,{=}\,(B,O,S)$, let
$P_{\mathit{bos}}(A)\,{=}\,P_{b}\cup P_{o}\cup P_{s}$ where $P_{b}$ is the
rewriting of each axiom in $B$ as (35), $P_{o}$ the rewriting of $O$ as (21),
and $P_{s}$ the rewriting of $S$ as (22). Let
$P_{\mathit{bpt}}(A)=P_{\mathit{bos}}(A)\,{\cup}\,\\{$(23), (34)$\\}$. Then
$P_{\mathit{bpt}}(A)$ has a single answer set $I$ that represents the union of
all proof graphs of all hypotheses of $A$ that are generated by back-chaining
according to Def. 2, with nodes $\\{P\,{\mid}\,\mathit{pot}(P)\,{\in}\,I\\}$
and edges
$\\{(Q,P)\,{\mid}\,\mathit{mayInferVia}(R,P,L)\,{\in}\,I,\mathit{inferenceNeeds}(P,R,Q)\,{\in}\,I\\}$.

##### Representing a Hypothesis.

Based on the potential proof graph defined above, we now formulate in ASP the
problem of guessing a hypothesis, i.e., selecting a connected part of the
potential proof graph as a solution to the abduction problem. Nodes of the
proof graph are represented as $\mathit{true}(\cdot)$.

If an atom $P$ is a goal, it is true.

$\displaystyle\mathit{true}(P)\,{\leftarrow}\,\mathit{goal}(P).$ (36)

If an atom $P$ is true, it is back-chained ($\mathit{infer}(\cdot)$),
factored, or abduced (the latter two represented as $\mathit{fai}$).

$\displaystyle 1\,{\leq}\,\\{\ \mathit{infer}(P)\ ;\ \mathit{fai}(P)\
\\}\,{\leq}\,1\,{\leftarrow}\,\mathit{true}(P).$ (37)

Each atom $P$ that is marked as inferred in the proof graph, has to be back-
chained via exactly one axiom $R$.

$\displaystyle 1\,{\leq}\,\\{\
\mathit{inferVia}(R,P):\mathit{mayInferVia}(R,P,\\_)\
\\}\,{\leq}\,1\,{\leftarrow}\,\mathit{infer}(P).$ (38)

If back-chaining an atom $P$ would add body atom $Q$ to the hypothesis, then
we define $Q$ as true.

$\displaystyle\mathit{true}(Q)\,{\leftarrow}\,\mathit{inferVia}(R,P),\mathit{inferenceNeeds}(P,R,Q).$
(39)

This encoding guesses the back-chaining part of a particular proof graph and
hypothesis.

######  Proposition 2.

Given an abduction instance $A=(B,O,S)$, let $P_{\mathit{gp}}$ consist of
rules (36)–(39). Then answer sets
$\mathit{AS}(P_{\mathit{bpt}}(A)\,{\cup}\,P_{\mathit{gp}})$ correspond 1-1
with proof graphs $G$ induced by hypotheses $H\,{\in}\,\hat{\mathcal{H}}(A)$
via back-chaining: edges $E(G)$ are represented as
$\mathit{inferVia}(\cdot,\cdot)$, nodes $N(G)$ as $\mathit{true}(\cdot)$,
back-chained atoms as $\mathit{infer}(\cdot)$, and other atoms in
$\mathit{fai}(\cdot)$.

###  3.3 Factoring

So far we merely encoded the back-chaining part of proof graphs. It remains to
deal with unification, which allows us to identify those atoms in a hypothesis
that incur a cost in $\textsc{C}ard$ and $\textsc{W}a$ because they must be
abduced. For that we use rules (24)–(30) which guess an equivalence relation
$\mathit{eq}(\cdot,\cdot)$ over the Herbrand Universe such that constants that
are not sort names can be equivalent with other constants.

######  Lemma 3.

Given an abduction instance $A=(B,O,S)$, let $P_{\mathit{eq}}$ consist of
rules (24)–(30). Then $\mathit{AS}(P_{bpt}(A)\,{\cup}\,P_{\mathit{eq}})$
contains one answer set for each equivalence relation on the HU of
$I\,{\in}\,\mathit{AS}(P_{bpt}(A))$ represented in predicate $\mathit{eq}$
such that sort names are singleton equivalence classes.

Atoms that are not back-chained are represented as $\mathit{fai}(P)$. These
must either be unified or abduced.

####  3.3.1 Bwd-G: Guess Factoring

This method guesses whether an atom is factored or abduced and represents for
factored atoms with which other atom they have been unified. As the
deterministically defined proof graph does not contain factoring between
inference steps, we require factoring with inferred atoms to obtain all
possible proof graphs. (We discuss and relax this restriction in Section
3.3.3.)

For an atom in $H$ that is not inferred, we guess if it is factored or
abduced.

$\displaystyle 1\,{\leq}\,\\{\ \mathit{factor}(P)\ ;\ \mathit{abduce}(P)\
\\}\,{\leq}\,1\,{\leftarrow}\,\mathit{fai}(P).$ (40)

If a factored atom $A_{1}\,{=}\,c(P,S_{1},O_{1})$ unifies with an inferred
atom $A_{2}\,{=}\,c(P,S_{2},O_{2})$ that is not below $A_{1}$ in the proof
graph, then represent that $A_{1}$ is factored via $A_{2}$.

$\displaystyle\mathit{factorVia}(c(P,S_{1},O_{1}),c(P,S_{2},O_{2}))\,{\leftarrow}\,\mathit{factor}(c(P,S_{1},O_{1})),\mathit{infer}(c(P,S_{2},O_{2})),$
$\displaystyle\hskip 50.00008pt\mathbf{not}\
\mathit{below}(c(P,S_{2},O_{2}),c(P,S_{1},O_{1})),eq(S_{1},S_{2}),eq(O_{1},O_{2}).$
(41)

We define $\mathit{below}(A_{1},A_{2})$ as a partial order over atoms such
that $A_{1}$ is below $A_{2}$ whenever inference of $A_{1}$ requires $A_{2}$,
and whenever $A_{1}$ is factored via $A_{2}$. Intuitively, ‘below’ can be read
as ‘closer to goal nodes’.

$\displaystyle\mathit{below}(P,Q)\,{\leftarrow}\,\mathit{inferVia}(R,P),\mathit{inferenceNeeds}(P,R,Q).$
(42)
$\displaystyle\mathit{below}(A,C)\,{\leftarrow}\,\mathit{below}(A,B),\mathit{below}(B,C).$
(43)
$\displaystyle\mathit{below}(P,Q)\,{\leftarrow}\,\mathit{factorVia}(P,Q).$
(44)

Note that without $\mathbf{not}\ \mathit{below}(\cdots)$ in (41), we would
obtain cyclic proof graphs where an atom justifies itself. This would affect
all objective functions we study, therefore we need to eliminate such cases.

If a factored atom unifies with an abduced atom, represent that this is the
case.

$\displaystyle\mathit{factorVia}(c(P,S_{1},O_{1}),c(P,S_{2},O_{2}))\,{\leftarrow}\,$
$\displaystyle\hskip
50.00008pt\mathit{factor}(c(P,S_{1},O_{1})),\mathit{abduce}(c(P,S_{2},O_{2})),eq(S_{1},S_{2}),eq(O_{1},O_{2}).$
(45)

Finally, we require that all factored atoms are unified with another atom.

$\displaystyle\mathit{factorOk}(P)\,{\leftarrow}\,\mathit{factorVia}(P,\\_).$
(46) $\displaystyle\leftarrow\,\mathit{factor}(P),\mathbf{not}\
\mathit{factorOk}(P).$ (47)

We do not prove correctness of Bwd-G, as encoding Bwd-A is similar and has
better performance.

####  3.3.2 Bwd-AI: Abduced/Inferred Cluster Factoring

As an alternative to guessing which atoms are factored and which are abduced,
we next define deterministically, that every atom that can be factored with an
inferred atom must be factored with that atom, and that all remaining sets $X$
of atoms that unified wrt. $\mathit{eq}$ are factored with the
(lexicographically) smallest atom in that equivalence class $X$ of atoms, in
the following called ‘cluster’.

To that end, instead of (41) we use the following rule.

$\displaystyle\mathit{factorViaI}(c(P,S_{1},O_{1}),c(P,S_{2},O_{2}))\,{\leftarrow}\,\mathit{fai}(c(P,S_{1},O_{1})),\mathit{infer}(c(P,S_{2},O_{2})),$
$\displaystyle\hskip 50.00008pt\mathbf{not}\
\mathit{below}(c(P,S_{2},O_{2}),c(P,S_{1},O_{1})),eq(S_{1},S_{2}),eq(O_{1},O_{2}).$
(48)

We represent atoms that are factored via inferred atoms using predicate
$\mathit{factorI}$ and we represent what remains to be factored or abduced in
$\mathit{fa}$. Moreover, we define that $\mathit{factorViaI}$ entails
$\mathit{factorVia}$.

$\displaystyle\mathit{factorI}(P)$
$\displaystyle\,{\leftarrow}\,\mathit{factorViaI}(P,\\_).$ (49)
$\displaystyle\mathit{fa}(P)$
$\displaystyle\,{\leftarrow}\,\mathit{fai}(P),\mathbf{not}\
\mathit{factorI}(P).$ (50) $\displaystyle\mathit{factorVia}(A,B)$
$\displaystyle\,{\leftarrow}\,\mathit{factorViaI}(A,B).$ (51)

Next we deal with these remaining atoms: we define a partial order over atoms
that unify under equivalence $\mathit{eq}$ and factor these clusters with the
(lexicographically) smallest element as follows.

$\displaystyle\mathit{factorCluster}(c(P,S_{2},O_{2}),c(P,S_{1},O_{1}))\,{\leftarrow}\,$
$\displaystyle\mathit{fa}(c(P,S_{1},O_{1})),\mathit{fa}(c(P,S_{2},O_{2})),eq(S_{1},S_{2}),$
$\displaystyle c(P,S_{1},O_{1})\,{<}\,c(P,S_{2},O_{2}),eq(O_{1},O_{2}).$ (52)
$\displaystyle\mathit{factorClusterAbove}(A)\,{\leftarrow}\,$
$\displaystyle\mathit{factorCluster}(A,\\_).$ (53)
$\displaystyle\mathit{factorVia}(A,B)\,{\leftarrow}\,$
$\displaystyle\mathit{factorCluster}(A,B),$ $\displaystyle\mathbf{not}\
\mathit{factorClusterAbove}(B).$ (54)

Note that (52) defines the partial order, (53) represents elements that are
not the smallest in the cluster, and (54) maps the partial order into
$\mathit{factorVia}$ using the smallest element as the atom that all others
are unified with. Finally, we define $\mathit{below}$ using rules (42)–(44),
and we define that every hypothesis atom that could not be factored is
abduced.

$\displaystyle\mathit{factor}(P)\,{\leftarrow}\,$
$\displaystyle\mathit{factorVia}(P,\\_).$ (55)
$\displaystyle\mathit{abduce}(P)\,{\leftarrow}\,$
$\displaystyle\mathit{fa}(P),\mathbf{not}\ \mathit{factor}(P).$ (56)

Note that this encoding represents a restricted set of solutions compared to
the previous one, however because of the symmetry of unification, by fixing
the direction of factoring we merely canonicalize solutions and cannot lose
optimal solutions.

######  Example 7 (continued).

To illustrate, that the factoring method of Bwd-AI does not eliminate optimal
solutions, consider the arc between the abduced atom $\mathit{fatherof}(f,m)$
and the factored atom $\mathit{fatherof}(f,n_{2})$ in Figure 1: if we reverse
this arc, then the former becomes factored and the latter abduced. The number
of abduced atoms stays the same, therefore $\textsc{C}ard$ is not affected;
reachability stays the same so $\textsc{C}oh$ is not affected; and costs
propagate the other direction:
$\mathit{fatherof}(f,m)^{\mathbf{48}\text{\$},\,\underline{100\text{\$}}}$
obtains cost via (6) and initial goal cost;
$\mathit{fatherof}(f,n_{2})^{\mathit{48}\textit{\$},\,\mathbf{57}\textbf{\$}}$
obtains cost from factoring and via (4), so $\textsc{W}a$ remains unchanged.

Similarly, the factoring edge between $\mathit{name}(m,\mathit{mary})$ and
$\mathit{name}(s,\mathit{mary})$ could be reversed: then
$\mathit{name}(m,\mathit{mary})^{\underline{100\$}}$ obtains only initial goal
cost and we would abduce
$\mathit{name}(s,\mathit{mary})^{\mathit{100}\textit{\$},\,\mathbf{120}\textbf{\$}}$
and minimum cost of $\textsc{W}a$ remains $100\$$ for these nodes, moreover
the number of abduced atoms ($\textsc{C}ard$) and reachability
($\textsc{C}oh$) stays the same.

For reversing factoring arcs between two non-abduced atoms, consider reversing
the arc between $\mathit{importantfor}(f,m)$ and
$\mathit{importantfor}(n_{1},m)$ in Figure 1: reversing that arc makes the
former atom factored (with costs $40\$$) and the latter abduced (with costs
$40\$$ and $60\$$), and back-chaining using (6) can be done from
$\mathit{importantfor}(n_{1},m)$ instead, which yields the abduced atom
$\mathit{fatherof}(n_{1},m)$${}^{\mathbf{48}\textbf{\$},\,\mathit{57}\textit{\$},\,\underline{100\$}}$
instead of $\mathit{fatherof}(f,m)$. Note that $\mathit{fatherof}(f,n_{2})$
can still be factored with that new abduced atom as $f\,{=}\,n_{1}$.
$\square$.

As we are solving an optimization problem, dealing with a subset of solutions
that has been canonicalized (by enforcing an arbitrary order on factoring) can
be an advantage for efficiency, as certain symmetric solutions are
automatically excluded.

We do not prove correctness of this factoring variant, as the following
variant has better performance.

####  3.3.3 Bwd-A: Abduced Cluster Factoring

Finally, we apply an even stronger canonicalization to the proof graph: we
assume factoring only happens with abduced atoms. We first show, that every
proof graph, that contains factoring with an inferred atom, can be transformed
into a proof graph where inferences between factored atom and abduced atoms is
duplicated and all factoring is done with abduced atoms.

######  Example 8 (continued).

The proof graph in Figure 1 can be transformed into a graph where factoring
happens only with abduced atoms: instead of factoring atom
$\mathit{importantfor}(n_{1},m)^{\textbf{60\$}}$ with atom
$\mathit{importantfor}(f,m)^{\textbf{40\$},\,\textit{60\$}}$, we can back-
chain from the former over axiom (6) which yields the atom
$\mathit{fatherof}(n_{1},m)^{\textbf{72\$}}$ in the graph. This atom can now
be factored with $\mathit{fatherof}(f,m)$ at the top, which obtains the set
$\\{48\$,\,72\$,\,100\$\\}$ of costs and therefore keeps the same minimum
cost. $\square$

Importantly, the metrics we consider do not change when we perform this
canonicalization.

######  Proposition 4.

Given a proof graph $G$ of a hypothesis $H\,{\in}\,\hat{\mathcal{H}}(A)$ of an
abduction instance $A$, there is a proof graph $G^{\prime}$ and hypothesis
$H^{\prime}$ of same cost wrt. $\textsc{C}ard$, $\textsc{C}oh$, $\textsc{W}a$
where factoring is only performed with atoms in $A(G^{\prime})$.

###### Proof.

We show how to push factoring edges closer to abduced atoms without changing
the objective function value. As the graph is acyclic, this operation can be
continued until we only unify with abduced atoms.

Given an atom $P\,{\in}\,H$ and an edge $(P,Q)\,{\in}\,E(G)$ of factoring $Q$
with $P$ using substitution $\theta$, and $P\,{\notin}\,A(G)$. Then either (i)
$P$ is factored with $Q^{\prime}$, i.e., $(Q^{\prime},P)\,{\in}\,E(G)$, or
(ii) $P$ is back-chained on axiom $r$ with $k$ body atoms, i.e.,
$(P_{i}^{\prime},P)\,{\in}\,E(G)$ for $1\,{\leq}\,i\,{\leq}\,k$. In case (i)
we can factor $Q$ with $Q^{\prime}$ instead of with $P$, which pushes
factoring one edge closer to abduced atoms. This does not affect
$\textsc{C}ard$ as $A(G)\,{=}\,A(G^{\prime})$, reachability stays the same so
$\textsc{C}oh$ is not affected, and the minimal cost of $P$ and $Q$ is
propagated to $Q^{\prime}$ as before the change, so $\textsc{W}a$ is not
affected. In case (ii) we can back-chain from $Q$ with axiom $r$, creating
edges $(\theta^{-1}(P_{i}^{\prime}),Q)$, adding nodes
$\theta^{-1}(P_{i}^{\prime})$ to $G^{\prime}$ if they do not exist (implicitly
they are already contained in $H$ due to equivalences) and adding factoring
edges from $(P_{i}^{\prime},\theta^{-1}(P_{i}^{\prime}))$ to $G^{\prime}$.
This reduces the number of inference edges between factored and abduced atoms
in the graph by 1. Similar as before, reachability and number of abduced atoms
stays constant. For $\textsc{W}a$, cost might increase for
$\theta^{-1}(P_{i}^{\prime})$ but stays the same for $Q^{\prime}$. Therefore,
we do not lose optimal solutions by restricting factoring to abduced atoms. ∎

By a similar argument, the order of factoring in such a proof graph does not
matter, so we can also canonicalize factoring direction.

######  Proposition 5.

Given a proof graph $G$ of a hypothesis $H$ where factoring is only performed
with atoms in $A(G)$, an abduced atom $P\,{\in}\,A(G)$, and atoms
$Q_{1},\ldots,Q_{k}$ that are factored with $P$. Then we can swap an arbitrary
$Q_{i}$, $1\,{\leq}\,i\,{\leq}\,k$, with $P$, factor all other $Q_{j}$,
$j\,{\neq}\,i$ with $Q_{i}$, factor $P$ with $Q_{i}$, and all objective
functions stay the same.

###### Proof.

As all $Q_{1},\ldots,Q_{k},P$ unify, we can arbitrarily choose one of them as
representative and factor all others with it. This does not increase the
number of abduced atoms in $\textsc{C}ard$, this does not affect reachability
in $\textsc{C}oh$, and costs of all atoms are propagated to the chosen
representative, and the minimum cost in $\textsc{W}a$ stays the same. ∎

To realize this canonicalization, we use rules (52)–(56) and add the following
rule, such that every atom that is not back-chained is factored with abduced
atoms if possible, otherwise abduced.

$\displaystyle\mathit{fa}(P)\,{\leftarrow}\,$ $\displaystyle\mathit{fai}(P).$
(57)

Note that this encoding does not require any guesses to determine what is
factored and what is abduced, moreover there is no need for the definition of
$\mathit{below}$.

######  Proposition 6.

Given an abduction instance $A=(B,O,S)$, let $P_{\text{\sc
Bwd-A}}(A)\,{=}\,P_{\mathit{bpt}}(A)\,{\cup}\,P_{\mathit{gp}}\,{\cup}\,P_{\mathit{eq}}\cup
P_{c}$ where $P_{c}=\\{$(52)–(56),(57)$\\}$, then answer sets
$\mathit{AS}(P_{\text{\sc Bwd-A}}(A))$ of $P_{\text{\sc Bwd-A}}(A)$ are in 1-1
correspondence with proof graphs $G$ and hypotheses
$H\,{\in}\,\hat{\mathcal{H}}(A)$ where factoring is performed only with $A(G)$
and only with lexicographically smaller atoms.

###  3.4 Fwd-A: Guess Abduced Atoms, Forward Inference, Check Goal

The previous encodings are based on explicitly representing proof graphs. We
next describe an encoding that is more in the spirit of the generate-define-
test paradigm of Answer Set Programming [35]: we again propagate potentially
interesting truth values, however we do not keep track of the inferences. We
guess which of these potentially interesting truth values is abduced or
factored, and use another rewriting of the axioms to reproduce their
semantics, i.e., we define that the head of an axiom is true if all its bodies
are true. Finally we check that all goals become true. For example axiom (9)
is translated into

$\displaystyle\mathit{infer}(c(\mathit{is},X,\mathit{depressed}))\,{\leftarrow}\,\mathit{true}(c(\mathit{importantfor},Y,X)),\mathit{true}(c(\mathit{is},Y,\mathit{dead})).$
(58)
$\displaystyle\mathit{pot}(c(\mathit{importantfor},Y,X))\,{\leftarrow}\,\mathit{pot}(c(\mathit{is},X,\mathit{depressed})),Y\,{=}\,s(r_{1},y,X).$
(59)
$\displaystyle\mathit{pot}(c(\mathit{is},Y,\mathit{dead}))\,{\leftarrow}\,\mathit{pot}(c(\mathit{is},X,\mathit{depressed})),Y\,{=}\,s(r_{1},y,X).$
(60)

where $r_{1}$ again is a unique identifier for axiom (9).

We guess potential atoms as factored or abduced, define truth from factoring,
abducing, and inference, and require that goals are true.

$\displaystyle\\{\ \mathit{fai}(X):\mathit{pot}(X)\ \\}\,{\leftarrow}\,$ .
(61) $\displaystyle\mathit{true}(X)\,{\leftarrow}\,$
$\displaystyle\mathit{fai}(X).$ (62)
$\displaystyle\mathit{true}(X)\,{\leftarrow}\,$
$\displaystyle\mathit{infer}(X).$ (63) $\displaystyle\,{\leftarrow}\,$
$\displaystyle\mathit{goal}(A),\mathbf{not}\ \mathit{true}(A).$ (64)

This realizes abduction in the classical generate-define-test way. The only
thing missing is factoring to determine which atoms actually need to be
abduced. For that we add the following rule to define which atoms are factored
or abduced.

$\displaystyle\mathit{fa}(X)\,{\leftarrow}\,\mathit{fai}(X),\mathbf{not}\
\mathit{infer}(X).$ (65)

We complete the encoding by cluster factoring rules (52)–(56) and common rules
(23)–(30).

Because we do not have an explicit representation of the proof tree, only the
$\textsc{C}ard$ metric is applicable. Moreover, we cannot factor with inferred
atoms as there is no way to rule out circular inference, hence we only study
the most restricted factoring variant.

For readability we gave the rewriting as an example. Formally, an axiom of
form (2) is rewritten into

$\displaystyle\mathit{infer}(c(q,Y_{1},\ldots,Y_{m}))$
$\displaystyle\,{\leftarrow}\,\mathit{true}(c(p_{1},X^{1}_{1},\ldots,X^{1}_{k_{1}})),\ldots,\mathit{true}(c(p_{r},X^{r}_{1},\ldots,X^{r}_{k_{r}})).$
$\displaystyle\mathit{pot}(c(p_{i},X^{i}_{1},\ldots,X^{i}_{k_{1}}))$
$\displaystyle\,{\leftarrow}\,Z_{1}\,{=}\,s(a,1,Y_{1},\ldots,Y_{m}),\ldots,Z_{v}\,{=}\,s(a,v,Y_{1},\ldots,Y_{m}),$
$\displaystyle\quad\mathit{pot}(c(q,Y_{1},\ldots,Y_{m})).\qquad\qquad\qquad\qquad\qquad\qquad\text{
for }i\,{\in}\,\\{1,\ldots,r\\}$

where $a$ is a unique identifier for that particular axiom and
$Z_{1},\ldots,Z_{v}\,{=}\,\mathcal{X}\,{\setminus}\,\mathcal{Y}$. Note that
this means that the resulting rules will all be safe.

We do not prove correctness of this encoding as it is only applicable to
$\textsc{C}ard$ and does not have good performance compared with other
encodings.

###  3.5 Encodings for Preferred Solutions

We next describe program modules that realize objective functions when we add
them to the previously given encodings.

##### Cardinality Minimality.

For realizing objective $\textsc{C}ard$ we use the following weak constraint.

$\displaystyle\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}\mathit{abduce}(P).\quad[1@1,P]$
(66)

##### Coherence Metric.

For $\textsc{C}oh$ we represent which nodes are reachable from which goal
node.

$\displaystyle\mathit{reach}(P,P)$
$\displaystyle\,{\leftarrow}\,\mathit{goal}(P).$ (67)
$\displaystyle\mathit{reach}(Q,\mathit{From})$
$\displaystyle\,{\leftarrow}\,\mathit{reach}(P,\mathit{From}),\mathit{inferVia}(R,P),\mathit{inferenceNeeds}(P,R,Q).$
(68) $\displaystyle\mathit{reach}(Q,\mathit{From})$
$\displaystyle\,{\leftarrow}\,\mathit{reach}(P,\mathit{From}),\mathit{factorVia}(P,Q).$
(69)

We represent pairs of distinct goal atoms that have a common reachable atom,
and we create a weak constraint that incurs a cost corresponding to pairs of
goal atoms without a common reachable atom.

$\displaystyle\mathit{reachFromBoth}(P,Q)$
$\displaystyle\,{\leftarrow}\,\mathit{goal}(P),\mathit{goal}(Q),P\,{<}\,Q,\mathit{reach}(N,P),\mathit{reach}(N,Q).$
(70)
$\displaystyle\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}\mathit{goal}(P),\mathit{goal}(Q),P\,{<}\,Q,\mathbf{not}\
\mathit{reachFromBoth}(P,Q).\quad[1@1,P,Q]$ (71)

##### Weighted Abduction.

For realizing $\textsc{W}a$ we represent potential costs as an integers. We
seed cost with $\$100$ for goal atom assumption cost.

$\displaystyle\mathit{pcost}(P,100)$
$\displaystyle\,{\leftarrow}\,\mathit{goal}(P).$ (72)

As common practice for applying $\textsc{W}a$ to Accel, we realize axiom costs
such that body cost factors sum up to $1.2$. For that we require for each
axiom $R$ a fact $\mathit{numberOfBodyAtoms}(R,N)$ to be defined such that $N$
is the number of body atoms of $R$. We also require a minimum cost of $1$
which prevents spurious very deep proof trees from being optimal due to cost
$0$ at abduced atoms.

$\displaystyle\mathit{pcost}(Q,Mc)\,{\leftarrow}\,$
$\displaystyle\mathit{inferVia}(R,P),\mathit{inferenceNeeds}(P,R,Q),$ (73)
$\displaystyle Mc\,{=}\,\mathit{\\#max}\ \\{\ (C*6/5)/N\ ;\ 1\
\\},\mathit{pcost}(P,C),\mathit{numberOfBodyAtoms}(R,N).$

These computations are handled during instantiation. They can be generalized
to assumption weights that are individually given for each axiom as facts,
without causing a change the rest of the encoding.

We propagate cost across factoring edges, define cost to be the minimum cost
found at all abduced atoms, and minimize that cost using a weak constraint.

$\displaystyle\mathit{pcost}(Q,C)$
$\displaystyle\,{\leftarrow}\,\mathit{factorVia}(P,Q),\mathit{pcost}(P,C).$
(74) $\displaystyle\mathit{cost}(P,C)$
$\displaystyle\,{\leftarrow}\,\mathit{abduce}(P),\ C\,{=}\,\mathit{\\#min}\
\\{\ Ic:\mathit{pcost}(P,Ic)\ \\}.$ (75)
$\displaystyle\mathrel{\mathchoice{\reflectbox{$\displaystyle\rightsquigarrow$}}{\reflectbox{$\textstyle\rightsquigarrow$}}{\reflectbox{$\scriptstyle\rightsquigarrow$}}{\reflectbox{$\scriptscriptstyle\rightsquigarrow$}}}\mathit{cost}(P,C).\quad[C@1,P]$
(76)

Table 1: Comparison of key aspects of ASP encodings Bwd-G, Bwd-AI, Bwd-A, and
Fwd-A.

Bwd-G Bwd-AI Bwd-A Fwd-A Objective functions supports $\textsc{C}ard$,
$\textsc{C}oh$, and $\textsc{W}a$ supports only $\textsc{C}ard$ Atom
justification backward inference from goals via forward inference from
(reasoning method) guessed inferences in proof graph abduced atoms Proof graph
represent potentially true atoms represent potentially (deterministic) and
inferences true atoms Nondeterministic guess infered vs. infered vs. false vs.
(atom justification) abduced vs. abduced or factored abduced or factored
factored Factoring none factor first with infered, deterministic factoring
canonicalization then with abduced atoms with abduced atoms Factoring
acyclicity check required (predicate $\mathit{below}$) check not required
(always acyclic)

######  Proposition 7.

Let $P_{\textsc{C}}ard=\\{$(66)$\\}$, $P_{\textsc{C}}oh=\\{$(67)–(71)$\\}$,
and $P_{\textsc{W}}a=\\{$(72)–(76)$\\}$. Then the cost of answer sets
$I\in\mathit{AS}(P_{\text{\sc Bwd-A}}(A)\cup P_{\textsc{C}}ard)$,
$I\in\mathit{AS}(P_{\text{\sc Bwd-A}}(A)\cup P_{\textsc{C}}oh)$, and
$I\in\mathit{AS}(P_{\text{\sc Bwd-A}}(A)\,{\cup}$ $P_{\textsc{W}}a)$ is the
objective function $\textsc{C}ard(G)$, $\textsc{C}oh(G)$, and
$\textsc{W}a(G)$, respectively, of the proof graph $G$ represented in $I$,
where for $\textsc{W}a$ costs are rounded to integers and at least $1$.

###  3.6 Summary

Table 1 gives an overview of our encodings. Encodings in the Bwd family
deterministically represent the maximal potential proof graph and all its
inferences, while Fwd-A represents only atoms in the hypothesis. Justification
of atoms in the proof graph is ensured from goals to abducibles (backward) in
the Bwd encodings, and from abduced atoms to goals (forward) in Fwd-A. The
type of justification of goals and atoms in the hypothesis is
nondeterministically guessed as one of three classes by Bwd-Gand one of two
classes by Bwd-AI and Bwd-A. Fwd-A guesses truth of abduced or factored atoms
(two classes). Factoring is canonicalized to various extent, and acyclicity of
factoring is implicitly ensured in Bwd-A and Fwd-A but is encoded explicitly
in other encodings.

##  4 Extensions

The ASP encodings given so far are realized in pure ASP-Core-2 syntax and do
not require additional features specific to particular solver tools. However,
these encodings have two drawbacks: they can represent only acyclic theories,
and they have performance issues related to the size of instantiation of the
transitivity constraint for $\mathit{eq}$. We next formalize two extensions of
these encodings and describe their computational realization.

In Section 4.1 we introduce Flexible Value Invention for fine-grained control
of Skolemization, which makes our encodings applicable to cyclic theories. In
Section 4.2 we show how to replace certain constraints in our encodings with
lazy variants to reduce grounding size and potentially improve evaluation
performance. Both extensions are described formally in the HEX formalism.
Section 4.3 discusses how we realized these extensions using the Python
library of Clingo.

###  4.1 Flexible Value Invention for Cyclic Knowledge Bases

The encodings in Section 3 assume that the knowledge base is acyclic, which
ensures finite proof trees and a finite instantiation of our ASP encodings in
the presence of Skolemization with Uninterpreted Function terms as done in our
axiom rewritings.

######  Example 9.

As an example of a cyclic knowledge base consider the following two axioms

$\displaystyle p(A,b)$ $\displaystyle\,\,{\Leftarrow}\,\,q(A,C),t(C,b).$
($r_{1}$) $\displaystyle t(D,b)$ $\displaystyle\,\,{\Leftarrow}\,\,p(D,b).$
($r_{2}$)

where a goal of $p(a,b)$ yields the following infinite backward chaining
instantiation of axioms in the proof tree

$\displaystyle p(a,b)$
$\displaystyle\,\,{\Leftarrow}\,\,q(a,s(r_{1},``C",a)),t(s(r_{1},``C",a),b).$
(via $r_{1}$) $\displaystyle t(s(r_{1},``C",a),b)$
$\displaystyle\,\,{\Leftarrow}\,\,p(s(r_{1},``C",a),b).$ (via $r_{2}$)
$\displaystyle p(s(r_{1},``C",a),b)$
$\displaystyle\,\,{\Leftarrow}\,\,q(s(r_{1},``C",a),s(r_{1},``C",s(r_{1},``C",a))),$
$\displaystyle\hphantom{\,\,{\Leftarrow}\,\,}t(s(r_{1},``C",s(r_{1},``C",a)),b).$
(via $r_{1}$) $\displaystyle t(s(r_{1},``C",s(r_{1},``C",a)),b)$
$\displaystyle\,\,{\Leftarrow}\,\,p(s(r_{1},``C",s(r_{1},``C",a)),b).$ (via
$r_{2}$) $\displaystyle\ \>\>\vdots$

where $C$ is first skolemized as $s(r_{1},``C",a)$ (see (31)) but then used
again to back-chain over the first axiom which leads to another Skolemization.
This leads to undecidability as we cannot know when we have generated ‘enough’
distinct variables to find the optimal solution. $\square$

The Accel benchmark is described as being acyclic [43] however it contains one
cyclic axiom and this contains a comment that suggests that the respective
axiom has been added after publication of [43]. To evaluate Accel, or any
cyclic theory with our encodings, we therefore need to exclude axioms to break
cycles, or infinite instantiations will occur. However, in knowledge
representation, knowledge is sometimes naturally expressed in cyclic axioms,
and we would like to handle such knowledge bases. In particular the cyclic
axioms in Accel are required to obtain correct solutions for some instances,
so we do not want to dismiss such axioms.

We next use external atoms instead of uninterpreted function symbols to
achieve a _Flexible Value Invention_ where we can control when to block value
invention. By blocking certain value inventions, we ensure a finite
instantiation of our encoding which thereby allows computation of optimal
solutions. If we do _not_ use cyclic axioms and limit value invention, we
obtain a subset of all acyclic proof graphs and a sound approximation of the
optimal solution. If we use cyclic axioms, they extend the proof graph in ways
that are impossible with acyclic axioms. The variations of Flexible Value
Invention (shown in the following) permit usage of cyclic axioms and allow for
controlling the trade-off between instantiation size and distance from the
optimal solution.

For Flexible Value Invention, we first outsource value invention into an
external atom $\text{{{\&}}}\\!\mathit{skolem}$. Formally, instead of
skolemizing variables $Z_{v}\,{\in}\,\mathcal{X}\setminus\mathcal{Y}$ in the
rewriting (35) as

$\displaystyle Z_{v}\,{=}\,s(a,v,Y_{1},\ldots,Y_{m})$ (77) where $a$ is the
axiom identifier, $v$ is the variable index, and $Y_{1},\ldots,Y_{m}$ are head
variables, we use
$\displaystyle\text{{{\&}}}\\!\mathit{skolem}[a,v,Y_{1},\ldots,Y_{m}](Z_{v}).$
(78)

######  Example 10.

Instead of (31) in the Bwd encodings (Example 6), we rewrite into the rule

$\displaystyle\mathit{mayInferVia}(r_{1},c(\mathit{is},X,\mathit{depressed}),l(Y))\,{\leftarrow}\,$
$\displaystyle\hskip
160.00024pt\mathit{pot}(c(\mathit{is},X,\mathit{depressed})),\text{{{\&}}}\\!\mathit{skolem}[r_{1},``Y",X](Y)$
(79) and instead of (59) and (60) in the Fwd-A encoding we rewrite the body
elements of the axiom into
$\displaystyle\mathit{pot}(c(\mathit{importantfor},Y,X))\,{\leftarrow}\,\mathit{pot}(c(\mathit{is},X,\mathit{depressed})),\text{{{\&}}}\\!\mathit{skolem}[r_{1},``Y",X](Y).$
$\displaystyle\mathit{pot}(c(\mathit{is},Y,\mathit{dead}))\,{\leftarrow}\,\mathit{pot}(c(\mathit{is},X,\mathit{depressed})),\text{{{\&}}}\\!\mathit{skolem}[r_{1},``Y",X](Y).$

$\square$

This way we outsource Skolemization, i.e., building a new unique constant term
$Z_{v}$ from terms $a,v,Y_{1},\ldots,Y_{m}$ — or the decision not to build
such a term — to an external computation. We next realize several
Skolemization methods that limit value invention in different ways.

The original Skolemization with uninterpreted functions can be emulated by
defining $f_{\text{\sl\&}skolem}$ as

$\displaystyle f_{\text{\sl\&}sk^{\infty}}(I,R,V,Y_{1},\ldots,Y_{m},Z)=1\text{
iff }Z=s(R,V,Y_{1},\ldots,Y_{m}).$

This shows that we can still express the original Skolemization (without
guaranteeing decidability).

######  Example 11 (continued).

The external atom $\text{{{\&}}}\\!\mathit{sk^{\infty}}[r_{1},``Y",X](Y)$ is
true iff $Y\,{=}\,s(r_{1},``Y",X)$. This means that instantiating (31), which
contains an uninterpreted function, and instantiating (79), which contains an
external computation, will create the same ground Skolem terms. $\square$

A simple way for ensuring termination is the following function.

$\displaystyle f_{\text{\sl\&}sk^{P^{1}}}(I,R,V,Y_{1},\ldots,Y_{m},Z)=1\text{
iff }\left\\{\begin{array}[]{@{~}l@{}}{}\lx@intercol
Z=s(R,V,Y_{1},\ldots,Y_{m})\\\ {}\lx@intercol\text{ and no $Y_{i}$,
$1\,{\leq}\,i\,{\leq}\,m$, is of the form
$s(\cdot,\cdot,\cdots)$.}\end{array}\right.$ (82)

This prevents value invention if any of the terms $Y_{1},\ldots,Y_{m}$ is an
invented value, which is a very restrictive criterion: it blocks all value
invention where at least one parent is an invented value.

######  Example 12 (continued).

The external atom $\text{{{\&}}}\\!\mathit{sk^{P^{1}}}[r_{1},``Y",X](Y)$ is
true if $Y\,{=}\,s(r_{1},``Y",X)$ and $X$ is not a term of form
$s(\cdots\\!)$. Instantiating rule (79) with $X\,{=}\,m$ then yields a single
external atom
$\text{{{\&}}}\\!\mathit{sk^{P^{1}}}[r_{1},``Y",m](s(r_{1},``Y",m))$ which
evaluates to true. Therefore, the rule head is instantiated as
$\mathit{mayInferVia}(r_{1},c(\mathit{is},m,\mathit{depressed})$,
$l(s(r_{1},``Y",m)))$. Assume that we have an additional axiom which contains
$\mathit{is}(X,\mathit{depressed})$ in the head and
$\mathit{is}(X,\mathit{dead})$ or $\mathit{importantfor}(X,Z)$ in the body.
Such an axiom allows cyclic back-chaining over
$\mathit{is}(X,\mathit{depressed})$, which yields another instantiation of
(79) with body literals $\mathit{pot}(c(\mathit{is},s(r_{1},``Y"$,
$m),\mathit{depressed}))$ and
$\text{{{\&}}}\\!\mathit{sk^{P^{1}}}[r_{1},``Y",s(r_{1},``Y",m)](Y)$. In this
case the external atom will not be true for any ground term $Y$: it blocks
Skolemization as the input term is already a Skolem term. Without this
blocking (e.g., with $\text{{{\&}}}\\!\mathit{sk^{\infty}}$) we would obtain
an infinite instantiation. $\square$

We can extend $f_{\text{\sl\&}sk^{P^{1}}}$ to block value invention only if
some grandparent is an invented value.

$\displaystyle f_{\text{\sl\&}sk^{P^{2}}}(I,R,V,Y_{1},\ldots,Y_{m},Z)=1\text{
iff }\left\\{\begin{array}[]{@{~}l@{}}{}\lx@intercol
Z=s(R,V,Y_{1},\ldots,Y_{m})\\\ {}\lx@intercol\text{ and no $Y_{i}$,
$1\,{\leq}\,i\,{\leq}\,m$, is of the form
$s(\cdot,\cdot,U_{1},\ldots,U_{k})$}\\\ {}\lx@intercol\text{ \quad with some
$U_{j}$, $1\,{\leq}\,j\,{\leq}\,k$, of the form
$s(\cdot,\cdot,\cdots)$.}\end{array}\right.$ (86)

This can be further generalized to $f_{\text{\sl\&}sk^{P^{i}}}$, where
$i\,{\in}\,\\{1,2,\ldots\\}$, indicates that in the $i{-}1$-th nesting level
of terms $Y_{i}$, $1\,{\leq}\,i\,{\leq}\,m$, terms must not be invented
values. $P^{1}$ corresponds to the method used in Henry-n700 for achieving
termination (Naoya Inoue 2015, personal communication).

External oracle functions $f_{\text{\sl\&}sk^{P^{i}}}$, $1\,{\leq}\,i$,
guarantee finite instantiation of cyclic abduction problems.

######  Proposition 8.

Given a cyclic or acyclic abduction instance $A\,{=}\,(B,O,S)$, let
${P_{\text{\sc Bwd-A}}}^{P^{i}}(A)$ be the program $P_{\text{\sc Bwd-A}}(A)$
after replacing all body atoms of form (77) by body atoms of form (78) where
$\text{{{\&}}}\\!\mathit{skolem}\,{=}\,\text{{{\&}}}\\!\mathit{sk^{P^{i}}}$,
then $\mathit{grnd}({P_{\text{\sc Bwd-A}}}^{P^{i}}(A))$ is finite for
$i\,{\in}\,\\{1,2,\ldots\\}$.

###### Proof.

${P_{\text{\sc Bwd-A}}}^{P^{i}}(A)$ is finite and contains only safe rules,
therefore the only source of infinite instantiation can be the instantiation
of terms of unlimited depth. Except for the first rule in the axiom rewriting
(35), all rules have heads with term nesting level equal or lower than in the
body, hence the only rule that can generate terms of unlimited depth is the
first in (35). In that rule, term $l(\cdots)$ is created, but it is only used
in the other rewritten rules in (35) where only the arguments of $l(\cdots)$
are used, and in (38), where this term is discarded, therefore $l(\cdots)$
cannot be infinitely nested. The only source of terms of infinite depth is the
external atom of form
$\text{{{\&}}}\\!\mathit{sk^{P^{i}}}[a,i,Y_{1},\ldots,Y_{m}](Z_{i})$ and it
causes infinite instantiation only if
$f_{\text{\sl\&}sk^{P^{i}}}(I,R,V,Y_{1},\ldots,Y_{m},Z)$ is true for
infinitely many distinct terms $Z$. $f_{\text{\sl\&}sk^{P^{i}}}$ is $1$ only
if no input $Y_{i}$, $1\,{\leq}\,i\,{\leq}\,m$, has a subterm at nesting level
$i-1$ that is of form $s(\cdots)$, and $R,V$ can be a finite number of
constants from $P_{\text{\sc Bwd-A}}^{P^{1}}(A)$. Moreover there is a finite
number of terms that can be built from constants in ${P_{\text{\sc
Bwd-A}}}^{P^{i}}(A)$ with function symbol $s$, and not having a subterm of
form $s(\cdots)$ below nesting level $i-1$. Hence there is a finite number of
tuples $R,V,Y_{1},\ldots,Y_{m}$ for which $f_{\text{\sl\&}sk^{P^{i}}}$
evaluates to true. As $Z$ depends on $R,V,Y_{1},\ldots,Y_{m}$,
$f_{\text{\sl\&}sk^{P^{i}}}$ evaluates to true for a finite number of tuples
$R,V,Y_{1},\ldots,Y_{m},Z$ and instantiation is finite with respect to a given
program ${P_{\text{\sc Bwd-A}}}^{P^{i}}(A)$. ∎

Limiting value invention this way is not the only way: nontermination of value
invention always involves a certain rule and a certain existential variable of
that rule being instantiated over and over again in a cycle. Therefore, we
next formulate an external Skolemization oracle that blocks Skolemization only
if a child term was generated for the same rule and variable.

$\displaystyle f_{\text{\sl\&}sk^{G^{1}}}(I,R,V,Y_{1},\ldots,Y_{m},Z)=1\text{
iff }\left\\{\begin{array}[]{@{~}l@{}}{}\lx@intercol
Z=s(R,V,Y_{1},\ldots,Y_{m})\text{ and}\\\ {}\lx@intercol\text{no $Y_{i}$,
$1\,{\leq}\,i\,{\leq}\,m$, has a sub-term of form
$s(R,V,\cdots)$.}\end{array}\right.$ (89)

This function also ensures finite instantiation.

######  Proposition 9.

Given a cyclic or acyclic abduction instance $A\,{=}\,(B,O,S)$, let
${P_{\text{\sc Bwd-A}}}^{G^{1}}(A)$ be the program $P_{\text{\sc Bwd-A}}(A)$
after replacing all body atoms of form (77) by body atoms of form (78) where
$\text{{{\&}}}\\!\mathit{skolem}\,{=}\,\text{{{\&}}}\\!\mathit{sk^{G^{1}}}$,
then $\mathit{grnd}({P_{\text{\sc Bwd-A}}}^{G^{1}}(A))$ is finite for
$i\,{\in}\,\\{1,2,\ldots\\}$.

###### Proof.

As in the proof of Proposition 8, the only reason for infinite instantiation
can be the external atom. Assume towards a contradiction, that the
instantiation is infinite. Then
$f_{\text{\sl\&}sk^{G^{1}}}(I,R,V,Y_{1},\ldots,Y_{m},Z)$ must be true for an
infinite number of terms $Z$. As we have a finite number of constants in
${P_{\text{\sc Bwd-A}}}^{G^{1}}(A)$ and $Z$ is instantiated using this set of
constants and function symbols of form $s(\cdots)$ with finite arity, for an
infinite number of terms we require infinite nesting depth of terms of form
$s(\cdots)$. As the set of possible tuples $(R,V)$ used as inputs of
$f_{\text{\sl\&}sk^{G^{1}}}$ is finite, we must repeat $(R,V)$ in some
subterms of $Z$ to reach an infinite amount of them. However
$f_{\text{\sl\&}sk^{G^{1}}}$ is false for such terms, contradiction. ∎

As before, we can further generalize to $f_{\text{\sl\&}sk^{G^{i}}}$ where
$i\,{\in}\,\\{1,2,\ldots\\}$ indicates that a Skolem term may contain at most
$i$ layers of sub-terms from the same rule and variable.

###  4.2 On-Demand Constraints

In the set of rules common to all encodings (Section 3.1), we represented
transitivity of the equivalence relation $\mathit{eq}$ as a constraint (30)
instead of using the more commonly used rule

$\displaystyle\mathit{eq}(A,C)\,{\leftarrow}\,\mathit{eq}(A,B),\mathit{eq}(B,C),A\,{\neq}\,B,B\,{\neq}\,C,A\,{\neq}\,C.$

The formulation as a constraint allows us to eliminate (30) from the encoding
and lazily create only those instances of (30) that are violated during the
search for the optimal solution. Such a lazy instantiation is easy for
constraints but not supported for rules in current solvers, as adding a new
rule changes the solver representation (usually the Clark completion) of all
rules with the same head in the program.

Formally we represent lazy constraints in HEX (cf. [14, 2.3.1]) by replacing
(30) with a constraint

$\displaystyle\,{\leftarrow}\,\mathbf{not}\
\text{{{\&}}}\\!\mathit{transitive}[\mathit{eq}]().$ (90) where the external
computation oracle is defined as follows: $\displaystyle
f_{\text{\sl\&}transitive}(I,p)=1\text{ iff }\text{the relation
$\\{(A,B)\,{\mid}\,p(A,B)\,{\in}\,I\\}$ is transitive.}$ (91)

Moreover, if we find a transitivity violation, i.e., a new triple $(A,B,C)$
such that $\\{p(A,B),p(B,C)\\}\,{\subseteq}\,I$ and $p(A,C)\,{\notin}\,I$, we
add a new nogood into the solver that prevents
$p(A,B)\,{\land}\,p(B,C)\,{\land}\,\neg p(A,C)$ for future answer set
candidates.

Similarly, we can ensure that $\mathit{below}$ is a partial order, by
replacing (43) with a guess of the relevant part of the extension of predicate
$\mathit{below}$333I.e., the part used in (41) and (48). as follows

$\displaystyle\\{\ \mathit{below}(Q,P)\
\\}\,{\leftarrow}\,\mathit{fai}(P),\mathit{infer}(Q).$

and require acyclicity of $\mathit{below}$ using a constraint of form (90)
with external atom $\text{{{\&}}}\\!\mathit{acyclic}[\mathit{below}]()$, an
oracle function that is true iff relation
$\\{(A,B)\,{\mid}\,p(A,B)\,{\in}\,I\\}$ is acyclic, and nogood generation for
all basic cycles in that relation.

###  4.3 Implementation

We formulated Flexible Value Invention and On-Demand Constraints using HEX as
a formal framework. In preliminary experiments we identified a performance
problem in the dlvhex solver that was not possible to fix easily, therefore we
decided to realize the extensions using the Python libraries of Gringo and
Clasp [25]. This posed additional challenges that we discuss next.

##### Flexible Skolemization.

Flexible Skolemization can be realized purely during instantiation by
replacing external atoms of the form
$\text{{{\&}}}\\!\mathit{skolem}[a,i,Y_{1},\ldots,Y_{m}](Z_{i})$ by the
expression $Z_{i}=@\mathit{skolem}(a,i$, $Y_{1},\ldots,Y_{m})$ and
implementing a Python function skolem that generates constants according to
the various semantic definitions for limited value invention that are
described in Section 4.1.

Note that we can only handle this kind of external atoms in grounding because
the value of the oracle function $f_{\text{\sl\&}skolem}$ does not depend on
the interpretation $I$.

##### On-demand Constraints.

Different from Flexible Skolemization, on-demand constraints are handled
during solving. For that, Clasp provides an interface for registering a
callback function which receives answer set candidates. In that callback we
can add nogoods to the solver. However, answer set enumeration modes of the
current Python API of Clasp do not work well together with this idea: either
we enumerate models of increasing quality, or we enumerate models without
using the objective function. In the former case an on-demand constraint can
invalidate the first model of optimal quality, which causes no further answer
set candidates to be found, (there are no better ones). The latter case is a
blind search for better solutions which is prohibitively slow.

To realize on-demand constraints with reasonable efficiency, we created
algorithm FindOptimalModel which first finds an optimistic bound for the
objective function and then backtracks to worse bounds using on-demand
constraints. This algorithm is of interest only until the Clasp API supports
changing enumeration mode or objective bound from within the callback, hence
we show details only in the appendix.

##### Global Constraints of Accel.

A final implementation aspect is the realization of global constraints of the
Accel benchmark.

Assumption nogoods and unique-slot constraints can be represented uniformly
for all encodings in ASP constraints. We here show the encoding strategy by
means of examples. Assumption nogoods as exemplified in (19) are encoded in
ASP as

$\displaystyle\,{\leftarrow}\,$
$\displaystyle\mathit{abduce}(c(\mathit{go\\_step},S,G_{1})),\mathit{abduce}(c(\mathit{goer},G_{2},P)),\mathit{eq}(G_{1},G_{2})$

where we take into account term equivalence.

Unique slot axioms as exemplified in (20) are encoded in ASP as

$\displaystyle\,{\leftarrow}\,$
$\displaystyle\mathit{true}(c(\mathit{goer},G_{1},P_{1})),\mathit{true}(c(\mathit{goer},G_{2},P_{2})),\mathit{eq}(G_{1},G_{2}),P_{1}\,{<}\,P_{2},\mathbf{not}\
\mathit{eq}(P_{1},P_{2})$

where we take into account term equivalence both for the entity that must be
the same to violate the constraint ($G_{1}$, $G_{2}$), and for the entity that
is enforced to be unique, i.e., must not be the same to violate the constraint
($P_{1}$, $P_{2}$). Note that condition $P_{1}\,{<}\,P_{2}$ achieves symmetry
breaking during instantiation.

##  5 Experimental Evaluation

We evaluated the above encodings, on-demand constraints, and flexible value
invention using the Accel benchmark described in Section 2.2. The encodings
and instances we used in experiments are available
online.444https://bitbucket.org/knowlp/asp-fo-abduction The benchmarks were
performed on a computer with 48 GB RAM and two Intel E5-2630 CPUs (total 16
cores) using Ubuntu 14.04. As solvers we used the Python API of
Clingo555http://potassco.sourceforge.net/ 4.5.4666Including a patch that will
be contained in future versions and eliminates a bug with aggregates. [25] to
implement on-demand constraints and flexible Skolemization as described in
Section 4.3, and we tested pure ASP encodings also with Gringo††footnotemark:
4.5.4††footnotemark:  [23] as grounder and both solvers Clasp††footnotemark:
3.1.4 [22] and Wasp777https://github.com/alviano/wasp/ version f9d436 [2]. We
also make experiments to compare with state-of-the-art approaches
Henry-n700888https://github.com/naoya-i/henry-n700 version 4b0d900 [29] and
its successor Phillip999https://github.com/kazeto/phillip version 5612b13
[52]. Each run was limited to 5 minutes and 5 GB RAM, HTCondor was used as a
job scheduling system, each run was repeated 5 times and no more than 8 jobs
were running simultaneously. For Clasp we used the setting
`--configuration=crafty` which turned out to be superior to all other preset
configurations of Clasp. For Wasp we used the default configuration (core-
based OLL algorithm) which performs equal or better compared with other
settings (note in particular, that configurations `basic`, `mgd`, and `opt`
for option `--weakconstraints-algorithm` perform clearly worse than the
default).

Table 2: Experiments with Clasp (C) and Wasp (W) on pure ASP encodings, and
the Phillip system (P).

Encoding Solver Opt To Mo $\mathit{T}$ $\mathit{M}$ $\mathit{Obj}$
$\mathit{T}_{\\!\mathit{grd}}$ $\mathit{T}_{\\!\mathit{slv}}$ $|\mathit{Chc}|$
$|\mathit{Conf}|$ # # # sec MB 1 sec sec # # $\textsc{C}ard$ Bwd-G C 15 28 7
223 1962 * * * * * Bwd-G W 36 0 14 68 2440 9.3 5.5 10.6 10K 758K Bwd-AI C 35 9
6 125 1870 9.3 5.3 25.9 74K 544 Bwd-AI W 36 0 14 64 2435 9.3 5.9 9.5 10K 143K
Bwd-A C 43 1 6 99 1778 9.3 5.0 22.5 14K 189 Bwd-A W 45 0 5 58 1689 9.3 5.2 6.0
11K 66 Fwd-A C 35 10 5 129 1765 9.3 5.2 22.1 128K 7K Fwd-A W 44 0 6 58 1697
9.3 5.6 6.0 14K 7K $\textsc{C}oh$ Bwd-G C 37 5 8 122 1980 26.8 5.7 29.7 121K
2K Bwd-G W 34 2 14 81 2613 26.8 6.0 13.0 20K 1M Bwd-AI C 39 5 6 113 1867 26.8
6.2 26.3 82K 1K Bwd-AI W 35 0 15 64 2492 26.8 5.4 9.2 19K 90K Bwd-A C 42 3 5
102 1760 26.8 5.1 22.5 76K 334 Bwd-A W 44 0 6 58 1696 26.8 5.3 5.9 8K 2K
$\textsc{W}a$ Bwd-G C 6 36 8 262 1977 * * * * * Bwd-G W 34 2 15 120 2761 482.6
5.3 53.0 953K 16M Bwd-AI C 31 13 6 156 1888 482.6 5.3 36.5 134K 8K Bwd-AI W 35
0 15 83 2530 482.6 5.4 18.5 393K 1M Bwd-A C 40 4 6 111 1774 482.6 5.1 24.1
138K 3K Bwd-A W 44 0 6 66 1703 482.6 5.1 8.1 159K 29K - P 0 50 0 300 230 * * *
* *

In the following tables, columns Opt, To, and Mo give the number of instances
for which an optimal solution was found, the timeout was reached, and the
memory limit was exceeded, respectively. These numbers are summed over
instances and averaged over runs. Columns $\mathit{T}$ and $\mathit{M}$ show
time (seconds) and memory (MB) requirement, averaged over instances and runs.

The remaining columns show detailed diagnostics of the solver and objective
function, where provided by the respective tool.
$\mathit{T}_{\\!\mathit{grd}}$ and $\mathit{T}_{\\!\mathit{slv}}$ give
grounding and solving time, respectively, as reported by running first Gringo
and then Clasp or Wasp. In experiments with the Python implementation,
$\mathit{T}_{\\!\mathit{grd}}$ includes solver preprocessing which cannot be
separated from grounding in Clasp API, and $\mathit{T}_{\\!\mathit{slv}}$
contains pure search time. Further metrics are only available if an optimal
solution could be found and proved as optimal: $\mathit{Obj}$ shows the
objective function, $|\mathit{Odc}|$ the number of on-demand constraints,
$|\mathit{Sk}|$ the number of created Skolem constants,
$|\mathit{Chc}|$/$|\mathit{Conf}|$ the number of choices and conflicts
encountered, and $|\mathit{Ru}|$ the number of rules in the program. To permit
a meaningful comparison of these values, we average them over the 17 easiest
instances. We only show averages if all runs found the optimum solution,
otherwise we write ‘*’. For large numbers, K and M abbreviate $10^{3}$ and
$10^{6}$.

Preliminary encodings in [47] were able to represent acyclic theories and
therefore only suitable for objective $\textsc{C}ard$. Equivalence was
represented by a relation between terms and representative terms in the
respective equivalence class (BackCh) or not at all (Simpl). We will not make
numerical comparisons as the performance of BackCh and Simpl is significantly
worse than the performance of encodings in this work in all cases (in
particular memory is exhausted in more than 50% of instances with Clasp).

##### Basic ASP Encodings.

Table 2 shows experimental results for encodings Bwd-G, Bwd-AI, Bwd-A, and
Fwd-A for objectives $\textsc{C}ard$, $\textsc{C}oh$, and $\textsc{W}a$ using
Gringo for grounding and Clasp (C) or Wasp (W) for solving. For $\textsc{W}a$
we also compare with Phillip (P). Bwd-G performs worst with respect to all
metrics, it performs significantly worse than Bwd-AI with Clasp, while it
performs just a bit below Bwd-AI with Wasp. Bwd-A performs best with respect
to all metrics, and for $\textsc{C}ard$, Wasp performs nearly the same with
the Fwd-A encoding.

Comparing Clasp and Wasp shows that Wasp is able to find the optimal solution
faster than Clasp except in cases where Wasp exceeds the 5GB memory limit,
which happens mainly for the encodings containing a higher amount of guesses
(Bwd-G, Bwd-AI). Another difference is the number of choices and conflicts:
Wasp generates fewer choices for $\textsc{C}ard$ and $\textsc{C}oh$, but more
choices for $\textsc{W}a$, moreover Wasp often generates more conflicts. These
differences on the same encoding can be explained by different ASP
optimization algorithms: for Clasp the used (default) configuration BB is
based on adding constraints to a relaxation of the instance, while for Wasp
the used (default) configuration OLL is based on unsatisfiable cores (for a
discussion of optimization approaches, see [3]).

Due to its unfavorable performance, we omit results for Bwd-G in the
following.

The Henry-n700 solver realizes $\textsc{W}a$ and on the Accel benchmark
results of around 10 sec per instance have been reported [29]. Phillip is the
successor of Henry-n700 and adds heuristics for a partial instantiation of the
most relevant portions of the proof graph [52]. We experimented with
Henry-n700 and Phillip on the original Accel knowledge base. Unfortunately we
were not able to reproduce the results reported for Henry-n700: as shown in
the table, all 50 instances timed out, moreover an ILP solution was found only
for 4 instances and the costs of these solutions where more than 25% above the
optimal result. As we had problems with the Gurobi license, we used the open-
source ‘lpsolve’ ILP backend in experiments, however Gurobi cannot improve the
situation much because most instances timed out during instantiation. From the
authors of Henry-n700 and Phillip we obtained a transformed version of Accel
that was used to produce their published results; unfortunately that rewriting
is incompatible with the current version of Henry-n700 as well as Phillip,
however we noticed that the rewriting makes some simplifying assumptions on
Accel: it interprets constants in goals as sort names, i.e., distinct entities
in the goal can never denote the same entity (which makes, e.g., coreference
resolution impossible); moreover sort names are compiled into predicates which
creates many distinct predicates of lower arity and makes instantiation
easier. Also assumption constraints are not realized. For reasoning with the
complete set of rules in Accel, our approach is significantly faster than the
state-of-the-art solver Phillip.

Table 3: Experimental Comparison of using uninterpreted function symbols
versus Python for Skolemization.

Uninterpreted Function Skolemization Python Skolemization Encoding Opt To Mo
$\mathit{T}$ $\mathit{M}$ $\mathit{T}_{\\!\mathit{grd}}$
$\mathit{T}_{\\!\mathit{slv}}$ Opt To Mo $\mathit{T}$ $\mathit{M}$
$\mathit{T}_{\\!\mathit{grd}}$ $\mathit{T}_{\\!\mathit{slv}}$ # # # sec MB sec
sec # # # sec MB sec sec $\textsc{C}ard$ Bwd-AI 36 5 9 114 1987 29.2 1.1 37 5
8 109 1989 29.4 1.1 Bwd-A 43 0 7 89 1890 28.3 0.1 43 0 7 88 1891 28.3 0.1
Fwd-A 34 9 7 120 1892 26.0 1.0 39 4 7 100 1893 25.9 0.8 $\textsc{C}oh$ Bwd-AI
38 3 9 111 1998 31.3 3.7 39 2 9 102 1997 31.1 2.0 Bwd-A 42 1 7 94 1895 26.8
0.4 41 2 7 93 1896 27.4 0.6 $\textsc{W}a$ Bwd-AI 29 12 9 151 2006 30.5 12.6 33
8 9 136 2004 28.9 8.6 Bwd-A 42 1 7 96 1899 26.2 1.2 42 1 7 95 1901 26.2 1.1

##### Skolemization.

Table 3 compares the encodings and objectives from Table 2 with their
counterparts using Python Skolemization. For a fair comparison, we here do not
compare with pure Gringo+Clasp, but we use our algorithm in Python in both
cases (even for ASP encodings that do not use Python Skolemization): this
explains differences to Table 2 and why we do not experiment with Wasp here.
For these and previous experiments we use only acyclic axioms and do not limit
Skolemization, so the only difference between the program is the shape of
constant symbols: nested uninterpreted function terms of form
$s(\cdot,\cdot,\cdot)$ versus constants of form $p_{i}$,
$i\,{\in}\,\mathbf{N}$, generated with Python. Although Python Skolemization
provides higher flexibility than uninterpreted function terms, there is no
noticeable effect on efficiency of the 17 easiest instances, and across all 50
instances, Python Skolemization has a positive effect on efficiency of the
Bwd-AI and Fwd-A encodings, while performance of the most efficient encoding
Bwd-A is unchanged.

It is not apparent why some encodings improve performance with Python
Skolemization. Structurally, the instantiated program entering the solver is
exactly the same in both Skolemization methods, except for Skolem constants
instead of uninterpreted function terms in the symbol table. However, we
additionally observed, that the order of rules created by Gringo changes
between both Skolemization methods. From this we conclude that the order of
rules matters, and that there is potential for optimization in solvers,
moreover this suggests that Clasp is sensitive to the order of rules it
consumes before solving. (We conjecture, that efficiency is not affected by
the form of strings in the symbol table.)

We conclude that in addition to the flexibility of Python Skolemization we can
gain efficiency.

Table 4: Managing acyclicity of $\mathit{below}$ and transitivity of
$\mathit{eq}$ using rules (R) versus on-demand constraints (O).

Encoding Method Opt To Mo $\mathit{T}$ $\mathit{M}$ $|\mathit{Odc}|$
$\mathit{T}_{\\!\mathit{grd}}$ $\mathit{T}_{\\!\mathit{slv}}$ $|\mathit{Chc}|$
$|\mathit{Conf}|$ $|\mathit{Ru}|$ # # # sec MB # sec sec # # # $\textsc{C}ard$
Bwd-AI R 36 5 9 114 1987 0 29.2 1.1 72K 553 3M Bwd-AI O 49 1 0 28 196 19 1.0
0.2 42K 5K 129K Bwd-A R 43 0 7 89 1890 0 28.3 0.1 14K 185 3M Bwd-A O 50 0 0 3
79 19 0.4 0.0 18K 3K 34K Fwd-A R 34 9 7 120 1892 0 26.0 1.0 131K 7K 3M Fwd-A O
39 11 0 88 87 213 0.6 0.6 165K 14K 39K $\textsc{C}oh$ Bwd-AI R 38 3 9 111 1998
0 31.3 3.7 99K 2K 3M Bwd-AI O 48 2 0 21 244 1185 1.2 1.1 226K 47K 252K Bwd-A R
42 1 7 94 1895 0 26.8 0.4 80K 287 3M Bwd-A O 47 3 0 27 134 1863 0.5 0.2 147K
30K 66K $\textsc{W}a$ Bwd-AI R 29 12 9 151 2006 0 30.5 12.6 113K 8K 3M Bwd-AI
O 37 13 0 102 286 2663 1.4 2.4 211K 37K 257K Bwd-A R 42 1 7 96 1899 0 26.2 1.2
127K 3K 3M Bwd-A O 49 1 0 42 146 5256 0.5 0.8 253K 23K 66K

##### On-Demand Constraints.

Table 4 shows experimental results for comparing two methods for ensuring
acyclicity of the relation $\mathit{below}$ and transitivity of the relation
$\mathit{eq}$. The rows with (R) use encodings as given in Section 3 while
those with (O) use on-demand constraints as described in Section 4.2. For a
fair comparison, all runs were performed with algorithms based on the Clasp
Python API (Section 4.3).

We observe that on-demand constraints significantly reduce instantiation time
and memory usage in all encodings and all objective functions. We can see the
difference between instantiating the full encodings or encodings without rules
(30) and (43) in column $\mathit{T}_{\\!\mathit{grd}}$. We observe that
instantiating transitivity and acyclicity dominates the instantiation time,
and that back-chaining in ASP is fast. Therefore we did not perform
experiments for creating the proof graph outside ASP (this would correspond to
the architecture of Phillip, where the proof graph is created in C++ and
solved in ILP).

Interestingly, for the $\textsc{C}oh$ objective, encoding Bwd-AI outperforms
Bwd-A with on-demand constraints (although by a small amount, and although the
instantiation time of the easiest 17 instances of Bwd-A is smaller than the
one of Bwd-AI).

As reported in the ILP-based solvers Henry-n700 and Phillip, on-demand
constraints turn out to be important for managing bigger instances in this
reasoning problem: we observe increased performance and a significant
reduction in memory usage.

Table 5: Comparison of Skolemization limits with Bwd-A encoding and objective
functions $\textsc{C}oh$ and $\textsc{W}a$.

Obj. Limit Opt To Mo $\mathit{T}$ $\mathit{M}$ $\mathit{Obj}$ $|\mathit{Sk}|$
$\mathit{T}_{\\!\mathit{grd}}$ $\mathit{T}_{\\!\mathit{slv}}$ $|\mathit{Chc}|$
$|\mathit{Conf}|$ $|\mathit{Ru}|$ # # # sec MB 1 # sec sec # # #
$\textsc{C}oh$ $P^{1}$ 50 0 0 2 37 33.9 23 0.4 0.0 4K 48 42K $P^{2}$ 45 2 3 68
1313 26.8 121 23.3 0.5 83K 630 3M $\infty$ 41 2 7 93 1896 26.8 128 27.4 0.6
90K 948 3M $G^{1}$ 33 1 16 127 2845 26.8 163 41.4 1.2 169K 917 6M $G^{2}$ 25 0
25 157 3635 26.8 199 76.8 2.2 286K 2K 12M $\textsc{W}a$ $P^{1}$ 50 0 0 2 38
595.3 23 0.4 0.0 5K 111 44K $P^{2}$ 43 4 3 79 1318 488.2 121 21.5 1.5 156K 2K
3M $\infty$ 42 1 7 95 1901 482.6 128 26.2 1.1 129K 2K 3M $G^{1}$ 33 1 16 130
2853 448.5 163 41.7 2.5 243K 2K 6M $G^{2}$ 24 1 25 159 3642 419.6 199 77.4 5.0
479K 3K 12M

##### Cyclic Theories and Limited Skolemization.

Table 5 shows the results of experiments with cyclic theories and limited
value invention as defined in Section 4.1. For encoding Bwd-A and all
objective functions, we evaluate the acyclic theory with unlimited
$f_{\text{\sl\&}sk^{\infty}}$ Skolemization, and the theory including the
cyclic axiom with parent- and rule-based Skolemization limits
$f_{\text{\sl\&}sk^{\alpha}}$ with
$\alpha\,{\in}\,\\{P^{1},P^{2},G^{1},G^{2}\\}$.

We show only $\textsc{C}oh$ and $\textsc{W}a$ with Bwd-A, because
$\textsc{C}ard$ and other encodings show the same trends.

We observe that time ($\mathit{T}$) and memory ($\mathit{M}$) usage, number of
generated Skolem constants ($|\mathit{Sk}|$), grounding time
($\mathit{T}_{\\!\mathit{grd}}$), and size of the instantiation
($|\mathit{Ru}|$), are ordered
$P^{1}\,{<}\,P^{2}\,{<}\,\infty\,{<}\,G^{1}\,{<}\,G^{2}$ for both objective
functions. Solving time ($\mathit{T}_{\\!\mathit{slv}}$), choices
($|\mathit{Chc}|$), and conflicts ($|\mathit{Conf}|$), are also nearly always
ordered like that.

Regarding the objective function, the $\infty$ method does not use the
(single) cyclic axiom in Accel, while the other methods use that axiom.
$P^{1}$ and $P^{2}$ permit a limited amount of value invention based on
invented values, and allow fewer inferences than $\infty$ on the acyclic
axioms, which results in a higher cost of the optimal solution. $G_{1}$ and
$G_{2}$ block value invention only when it reaches the same rule (not other
rules), therefore they allow a superset of the inferences of $\infty$. This
explains, why $\mathit{Obj}$ of $\infty$ is above the one of $P_{2}$ and below
the one of $G_{1}$ (recall that we display $\mathit{Obj}$ only for the 17
instances where all runs found the optimum).

Regarding efficiency, one or two generations of invented values across rules
($G^{1}$, $G^{2}$) drastically increase memory exhaustion, while strictly
limiting value invention ($P^{1}$) makes the problem easy to solve and impairs
solution quality.

Table 6: Experiments with Clasp (C) and Wasp (W) about realizing global
constraints versus omitting them.

Global Constraints in ASP Global Constraints Omitted Encoding Solver Opt To Mo
$\mathit{T}$ $\mathit{M}$ $\mathit{Obj}$ $|\mathit{Conf}|$ Opt To Mo
$\mathit{T}$ $\mathit{M}$ $\mathit{Obj}$ $|\mathit{Conf}|$ # # # sec MB 1 # #
# # sec MB 1 # $\textsc{C}ard$ Bwd-AI C 35 9 6 125 1870 9.8 815 35 9 6 130
1870 9.8 1K Bwd-AI W 36 0 14 64 2435 9.8 194K 36 0 14 64 2442 9.8 188K Bwd-A C
43 1 6 99 1778 9.8 248 42 3 5 104 1755 9.8 560 Bwd-A W 45 0 5 58 1689 9.8 73
45 0 5 59 1688 9.8 52 Fwd-A C 35 10 5 129 1765 9.8 11K 34 11 5 133 1765 9.8
26K Fwd-A W 44 0 6 58 1697 9.8 2K 44 0 6 57 1695 9.8 2K $\textsc{C}oh$ Bwd-AI
C 39 5 6 113 1867 29.4 666 40 4 6 111 1870 29.4 614 Bwd-AI W 35 0 15 64 2492
29.4 77K 35 0 15 64 2489 29.4 124K Bwd-A C 42 3 5 102 1760 29.4 461 42 2 6 103
1783 29.4 369 Bwd-A W 44 0 6 58 1696 29.4 1K 44 0 6 59 1699 29.4 563
$\textsc{W}a$ Bwd-AI C 31 13 6 156 1888 487.0 14K 29 14 7 162 1903 487.0 15K
Bwd-AI W 35 0 15 83 2530 487.0 2M 35 1 14 82 2524 487.0 1M Bwd-A C 40 4 6 111
1774 487.0 4K 39 6 5 117 1757 487.0 6K Bwd-A W 44 0 6 66 1703 487.0 25K 44 0 6
68 1701 487.0 22K

##### Global Constraints.

Table 6 shows a comparison between realizing unique-slot constraints and
assumption constraints in ASP constraints versus not considering these
constraints.

Global constraints have no significant effect on efficiency.

We see no effect on the objective function when removing global constraints.
This seems counterintuitive: more constraints should intuitively increase cost
of the optimal solution. It turns out that these cases are rare: we can
observe an increased cost of optimal solutions if we limit Skolemization using
method $P^{1}$. We conclude that global constraints in the Accel benchmark
have a small impact on solution quality.

##### Other Experiments.

For combining on-demand constraints with optimization, we also investigated
alternatives to algorithm FindOptimalModel (see Section 4.3 and the appendix)
where we used Clasp assumptions and Clasp externals for deactivating certain
optimization criteria during some parts of the search. These alternatives
perform significantly worse, moreover they are involved and require rewriting
weak constraints into normal rules, therefore we decided to omit further
details about these experiments.

Realizing global constraints of Accel also in an on-demand manner did not
yield significantly different results from using the pure ASP versions,
therefore we omit these results from the presentation.

We experimented with projecting answer sets to the atoms that are relevant for
the objective function, which yielded a significant reduction in log file size
(because we print the solution) but no significant reduction in time or
memory.

##  6 Related Work

The idea of abduction goes back to Peirce [44] and was later formalized in
logic.

Abductive Logic Programming (ALP) is an extension of logic programs with
abduction and integrity constraints. Kakas et al. [31] discuss ALP and
applications, in particular they relate Answer Set Programming and abduction.
Fung et al. describe the IFF proof procedure [20] which is a FOL rewriting
that is sound and complete for performing abduction in a fragment of ALP with
only classical negation and specific safety constraints. Denecker et al. [9]
describe SLDNFA-resolution which is an extension of SLDNF resolution for
performing abduction in ALP in the presence of negation as failure. They
describe a way to ‘avoid Skolemization by variable renaming’ which is exactly
what we found to increase performance in flexible Skolemization (recall that
we create numbered constants $p_{i}$ instead of structured terms $s(\cdots)$
in Python). Kakas et al. describe the $\mathcal{A}$-System for evaluating ALP
using an algorithm that interleaves instantiation of variables and constraint
solving [33]. The CIFF framework [40] is conceptually similar to the
$\mathcal{A}$-System but it allows a more relaxed use of negation. The
$\mathcal{S}\text{CIFF}$ framework [1] relaxes some restrictions of CIFF and
provides facilities for modeling agent interactions. In [27],
$\mathcal{S}\text{CIFF}$ was used to realize semantics of Datalog± [8] which
natively supports existentials in rule heads (i.e., value invention) as
opposed to ASP. The focus of $\mathcal{S}\text{CIFF}$ is on finding abductive
explanations, while our focus is to find preferred abductive explanations
according to objective functions. Realizing objective functions requires
modifying the $\mathcal{S}\text{CIFF}$ engine (Evelina Lamma 2015, personal
communication) therefore we did not perform experiments comparing
$\mathcal{S}\text{CIFF}$ with our encodings.

Implementations of ALP, have in common that they are based on evaluation
strategies similar to Prolog [40]. In [40], CIFF is compared with ASP on the
example of n-queens and the authors emphasize that CIFF has more power due to
its partial non-ground evaluation. However, they use a non-optimized n-queens
encoding for that comparison, and optimized n-queens encodings for Clingo[24]
are known to yield orders of magnitude better performance than naive
encodings, hence partial non-ground evaluation is not necessarily a guarantee
for better performance. Different from CIFF and earlier ALP implementations,
our approach instantiates one Boolean variable for each node in the potential
proof graph and then searches for the best solution, while methods that create
nodes on demand (such as CIFF) can completely eliminate certain nodes from
instantiation, while instantiating other nodes multiple times.

The AAA (ATMS-based Abduction Algorithm) reasoner [41, 43] combines Prolog
resolution with ATMS-based caching for realizing abduction. For Accel, AAA
realizes $\textsc{C}ard$ and $\textsc{C}oh$ metrics and enforces assumption-
nogoods and unique-slot constraints in dedicated (imperative) procedures.

The Henry-n700 reasoner [29] realizes $\textsc{W}a$ by creating an ILP
instance with C++ using back-chaining and then finding optimal solutions for
the ILP instance. The newest version of Henry-n700 is called Phillip [52];
this solver adds heuristics that partially instantiate the proof tree
according to relatedness between predicates (although without formal proof of
the correctness or worst-case approximation error). This two-step approach is
similar to our approach in ASP: our encodings cause the ASP grounder to
perform back-chaining in the knowledge base, and after instantiation the
solver searches for optimal solutions satisfying all rules and constraints. A
big performance improvement for Henry-n700 was the usage of Cutting Plane
Inference [29]. We mimic the approach with on-demand constraints in ASP, and
we can observe similar improvements in instantiation size and time, however
solve time increases by a larger amount for many instances, hence this
approach is not sufficient for achieving a corresponding performance boost in
ASP. Within the ASP community, on-demand constraints are related to methods of
lazy instantiation of ASP programs, as done in the solvers ASPeRiX [34], OMiGA
[13], Galliwasp [39], and recently also in the IDP system [10]. These systems
apply lazy instantiation to all rules and constraints in the program, whereas
we make only certain problematic constraints lazy.

_Probabilistic_ abduction was realized in Markov Logic [45] in the Alchemy
system [32] although without value invention [5, 48], i.e., existential
variables in rule heads are naively instantiated with all ground terms in the
program. A corresponding ASP encoding for the non-probabilistic case for
$\textsc{C}ard$ exists [47, Simpl], however it shows prohibitively bad
performance.

The termination proofs we do are related to the notion of _Liberal Safety_ in
HEX programs [15], however Liberal Safety requires either specific acyclicity
conditions (which are absent in our encodings), or conditions on finiteness of
the domain of certain attributes of the external atom (that our Skolemization
atoms do not fulfill). Hence we had to prove termination without using Liberal
Safety.

In the area of Automated Theorem Proving, algorithms search for finite models
(or theorems, unsatisfiability proofs) in full first order logic without
enforcing UNA and including native support for Skolemization (cf. [50]). These
algorithms focus on finding a feasible solution and do not contain support for
preferences (optimization criteria). However, the main emphasis of our
abduction problems is to find solutions with optimal cost (recall that our
problems always have the trivial solution to abduce all input atoms). To
tackle our abduction problem with such theorem provers, it would be necessary
to transform the optimization problem into a decision problem and perform a
search over the optimization criterion, calling the prover several times.
Related to theorem proving, a hypertableaux algorithm for coreference
resolution is described in [6]. This algorithm is inspired by weighted
abduction, however it does not use preferences and relies solely on
inconsistency for eliminating undesired solutions.

##### Computational Complexity.

The complexity of abduction in _propositional_ theories in the presence of the
$\textsc{C}ard$ objective has been analyzed in [4, 16], and in [17], the
propositional case of abduction in logic programs is studied and extended to
function-free logic programming abduction (Sec. 6), under the restriction that
only constants from observations and knowledge base (there called
‘manifestations’ and ‘program’) are used and that the UNA holds for all terms.
However, in our variant of abduction the optimal solution may use a set (of
unspecified size) of constants that are not present in the input and there is
potential equality among certain input constants and constants originating in
value invention. Hence, existing results can be seen as lower bounds for
hardness but do not directly carry over to our scenario.

In an acyclic theory, our reasoning problem is related to non-recursive
negation-free Datalog theories and non-recursive logic programming with
equality, which has been studied (although not with respect to abductive
reasoning) in [11].

Creating the largest possible proof graph for a given goal and knowledge base
can be done by reversing axioms and evaluating them with the goal; the
complexity of this problem (definite not range-restricted logic program
without function symbols) was shown to be PSPACE-complete [51, Thm. 4.1].

##  7 Conclusion

We have created a flexible and publicly available framework for realizing
variations of cost-based FO Horn abduction represented in the declarative
reasoning framework of Answer Set Programming [36] that allows us (i) to
modularly encode additional objective functions based on the abductive proof
graph, and (ii) to add global constraints of arbitrary complexity and size.
Our encodings use a modular translation of axioms into ASP rules, i.e., each
axiom can be translated independent from other axioms. As preference relations
we realized cardinality-minimality, coherence [43], and weighted abduction
[28, 49]. We evaluated our framework on the Accel benchmark [43] and found
that we have significantly higher performance than state-of-the-art solver
Phillip [52] which is the successor system of Henry-n700[29]. In our
experiments, Wasp [2] solves instances faster than Clasp [22], however Wasp
uses more memory for programs with a high degree of nondeterminism.

For realizing value invention we experimented with uninterpreted functions and
with external computations providing new values to the program. Performing
Skolemization with external computations provides fine-grained control for
deciding when to instantiate a term and when to refuse further instantiation.
This allows us to ensure and formally prove decidability when performing
abduction in cyclic FO Horn knowledge bases. Fortunately, this flexibility
does not impair computational efficiency.

An important topic in this research is encoding the proof graph. Usually, in
ASP we are not interested in the order of inferences made in the program or in
the dependencies or equivalences between atoms — those are handled
transparently in the solver. However, for modeling preference functions
$\textsc{C}oh$ and $\textsc{W}a$, which are defined on proof graphs, we must
explicitly represent a proof graph, including back-chaining and unification,
in our ASP encoding. We also experiment with an alternative encoding (Fwd-A)
for representing objective $\textsc{C}ard$: this encoding performs abduction
without representing a proof graph, it is based on forward inference, has good
performance with the Wasp solver.

The Bwd-A encoding performs best, intuitively because it makes the most strict
canonicalization operations on the graph by requiring factoring to happen only
with abduced atoms. Proof cost is not affected by this canonicalization,
however proof graphs will contain duplicate inferences for atoms that are
equivalent due to term equivalence: these atoms could be first factored and
inferred later. Yet this seemingly wasteful proof graph does not diminish
performance in ASP, because we anyway need to instantiate the whole potential
proof graph, so all inferences trees are available even if we do permit
factoring anywhere in the tree. Postponing factoring to abduced atoms has the
effect that we need to handle term equivalence only for these atoms, which is
an advantage for efficiency.

As ASP provides no native support for term equivalence, we encode equivalence
and unification explicitly. We guess an equivalence relation and check its
reflexivity, symmetry, transitivity with constraints. Explicit representation
of transitivity of equivalence has been shown to be a major performance issue
in Henry-n700, as it causes instantiation of a cubic amount of rules [29].
This performance issue also becomes apparent in our ASP representation, and we
apply the solution from Henry-n700 to our encodings by using on-demand
constraints, which we describe formally in the HEX formalism [14]. Realizing
on-demand constraints in presence of optimization is nontrivial in current
solvers, and we describe an algorithm based on the Python API of Clingo[25].
On-demand constraints significantly reduce memory usage by partially
instantiating transitivity constraints of the term equivalence relation (note
that the potential proof graph is still fully instantiated). This is
consistent with results reported for Henry-n700 and Phillip for weighted
abduction [29] with ILP as a solver backend and not surprising as ASP and ILP
are related methods for solving combinatorial problems [37].

##### Future work.

The major motivation for this work was to obtain a more flexible framework
where variations of objective functions and constraints on abduction can be
studied. In the future we intend to perform research in this direction.
Moreover we want to apply our encodings to other datasets like the one derived
from the Recognizing Textual Entailment (RTE) [12] challenge.

Among the encodings we experiment with, the most obvious and straightforward
encoding (Bwd-G) has the worst performance, and small encoding changes as well
as bigger changes, that realize symmetry breaking based on a theoretical
analysis of the problem, are required for achieve acceptable performance
(Bwd-A). Interestingly, the Wasp solver is able to compensate for the more
nondeterministic representation: it performs similar on Bwd-G and Bwd-AI
encodings, opposed to Clasp which performs significantly worse on Bwd-G. We
conclude that automatic program optimization and supporting tools for
diagnosing performance issues are open problems in ASP and fruitful topics for
future work.

## Acknowledgements

We thank Naoya Inoue, Evelina Lamma, Christoph Redl, and the anonymous
reviewers and RCRA workshop participants for constructive feedback about this
work. We thank Mario Alviano, Carmine Dodaro, Roland Kaminski, and Benjamin
Kaufmann for support regarding Clasp, Gringo, and Wasp.

## References

  * ACG+ [08] Marco Alberti, Federico Chesani, Marco Gavanelli, Evelina Lamma, Paola Mello, and Paolo Torroni.  Verifiable agent interaction in abductive logic programming: The SCIFF framework.  ACM Transactions on Computational Logic, 9(4):Article No. 29, 2008\.
  * ADLR [15] Mario Alviano, Carmine Dodaro, Nicola Leone, and Francesco Ricca.  Advances in WASP.  In International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR), pages 40–54, 2015.
  * ADMSR [15] Mario Alviano, Carmine Dodaro, Joao Marques-Silva, and Francesco Ricca.  Optimum stable model search: algorithms and implementation.  Journal of Logic and Computation, 2015.
  * BATJ [91] Tom Bylander, Dean Allemang, Michael C Tanner, and John R Josephson.  The computational complexity of abduction.  Artificial Intelligence, 49(1-3):25–60, 1991.
  * BHD+ [11] James Blythe, Jerry R Hobbs, Pedro Domingos, Rohit J Kate, and Raymond J Mooney.  Implementing Weighted Abduction in Markov Logic.  In International Conference on Computational Semantics (IWCS), pages 55–64, 2011.
  * BK [00] Peter Baumgartner and Michael Kühn.  Abducing Coreference by Model Construction.  Journal of Language and Computation, 1(2):175–190, 2000.
  * CFG+ [12] Francesco Calimeri, Wolfgang Faber, Martin Gebser, Giovambattista Ianni, Roland Kaminski, Thomas Krennwallner, Nicola Leone, Francesco Ricca, and Torsten Schaub.  ASP-Core-2 Input language format.  Technical report, ASP Standardization Working Group, 2012.
  * CGL [09] Andrea Calì, Georg Gottlob, and Thomas Lukasiewicz.  Datalog+/-: A Unified Approach to Ontologies and Integrity Constraints.  In International Conference on Database Theory, pages 14–30, 2009\.
  * DdS [98] Marc Denecker and Danny de Schreye.  SLDNFA: An abductive procedure for abductive logic programs.  The Journal of Logic Programming, 34(2):111–167, 1998.
  * DDSB [15] Broes De Cat, Marc Denecker, Peter Stuckey, and Maurice Bruynooghe.  Lazy Model Expansion: Interleaving Grounding with Search.  Journal of Artificial Intelligence Research, 52:235–286, 2015.
  * DEGV [01] Evgeny Dantsin, Thomas Eiter, Georg Gottlob, and Andrei Voronkov.  Complexity and expressive power of logic programming.  ACM Computing Surveys, 33(3):374–425, 2001.
  * DGM [06] Ido Dagan, Oren Glickman, and Bernardo Magnini.  The PASCAL Recognising Textual Entailment Challenge.  In Machine Learning Challenges, pages 177–190. Springer, 2006.
  * DtEF+ [12] Minh Dao-tran, Thomas Eiter, Michael Fink, Gerald Weidinger, and Antonius Weinzierl.  OMiGA: An Open Minded Grounding On-The-Fly Answer Set Solver.  In Logics in Artificial Intelligence (JELIA), pages 480–483, 2012\.
  * EFI+ [16] Thomas Eiter, Michael Fink, Giovambattista Ianni, Thomas Krennwallner, Christoph Redl, and Peter Schüller.  A model building framework for Answer Set Programming with external computations.  Theory and Practice of Logic Programming, 16(04):418–464, 2016\.
  * EFKR [13] Thomas Eiter, Michael Fink, Thomas Krennwallner, and Christoph Redl.  Liberal Safety for Answer Set Programs with External Sources.  In AAAI Conference on Artificial Intelligence, pages 267–275, 2013\.
  * EG [95] Thomas Eiter and Georg Gottlob.  The Complexity of Logic-Based Abduction.  Journal of the ACM, 42(1):3–42, 1995.
  * EGL [97] Thomas Eiter, Georg Gottlob, and Nicola Leone.  Abduction from logic programs: Semantics and complexity.  Theoretical Computer Science, 189(1-2):129–177, 1997.
  * EIK [09] Thomas Eiter, Giovambattista Ianni, and Thomas Krennwallner.  Answer Set Programming: A Primer.  In Reasoning Web Summer School, Lecture Notes in Computer Science, pages 40–110. Springer, 2009.
  * EIST [06] Thomas Eiter, Giovambattista Ianni, Roman Schindlauer, and Hans Tompits.  Effective Integration of Declarative Rules with External Evaluations for Semantic-Web Reasoning.  In European Semantic Web Conference (ESWC), pages 273–287, 2006\.
  * FK [97] Tze Ho Fung and Robert Kowalski.  The IFF proof procedure for abductive logic programming.  The Journal of Logic Programming, 33(2):151–165, 1997.
  * FPL [11] Wolfgang Faber, Gerald Pfeifer, and Nicola Leone.  Semantics and complexity of recursive aggregates in answer set programming.  Artificial Intelligence, 175(1):278–298, 2011.
  * GKK+ [15] Martin Gebser, Roland Kaminski, Benjamin Kaufmann, Javier Romero, and Torsten Schaub.  Progress in clasp Series 3.  In International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR), pages 368–383, 2015.
  * GKKS [11] Martin Gebser, Roland Kaminski, Arne König, and Torsten Schaub.  Advances in gringo series 3.  In International Conference on Logic Programming and Non-monotonic Reasoning (LPNMR), pages 345–351, 2011.
  * GKKS [12] Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub.  Answer Set Solving in Practice.  Morgan Claypool, 2012.
  * GKKS [14] Martin Gebser, Roland Kaminski, Benjamin Kaufmann, and Torsten Schaub.  Clingo = ASP + Control: Extended Report.  Technical report, University of Potsdam, 2014.
  * GL [88] Michael Gelfond and Vladimir Lifschitz.  The Stable Model Semantics for Logic Programming.  In International Conference and Symposium on Logic Programming (ICLP/SLP), pages 1070–1080, 1988.
  * GLR+ [15] Marco Gavanelli, Evelina Lamma, Fabrizio Riguzzi, Elena Bellodi, Riccardo Zese, and Giuseppe Cota.  An abductive Framework for Datalog+/- Ontologies.  In International Conference on Logic Programming (ICLP), Technical Communications, number 1433. CEUR-WS.org, 2015.
  * HSME [93] Jerry R Hobbs, Mark Stickel, Paul Martin, and Douglas Edwards.  Interpretation as abduction.  Artificial Intelligence, 63(1-2):69–142, 1993.
  * II [13] Naoya Inoue and Kentaro Inui.  ILP-based Inference for Cost-based Abduction on First-order Predicate Logic.  Journal of Natural Language Processing, 20(5):629–656, 2013.
  * IOIH [14] Naoya Inoue, Ekaterina Ovchinnikova, Kentaro Inui, and Jerry Hobbs.  Weighted Abduction for Discourse Processing Based on Integer Linear Programming.  In Plan, Activity, and Intent Recognition, pages 33–55. Elsevier, 2014.
  * KKT [92] A C Kakas, R A Kowalski, and F Toni.  Abductive Logic Programming.  Journal of Logic and Computation, 2(6):719–770, 1992.
  * KSR+ [10] S Kok, M Sumner, M Richardson, P Singla, H Poon, Lowd D, J Wang, A Nath, and P Domingos.  The Alchemy system for statistical relational AI.  Technical report, Department of Computer Science and Engineering, University of Washington, 2010.
  * KVD [01] Antonis C. Kakas, Bert Van Nuffelen, and Marc Denecker.  A-System: Problem solving through abduction.  In International Joint Conference on Artificial Intelligence (IJCAI), pages 591–596, 2001.
  * LBSG [15] Claire Lefèvre, Christopher Béatrix, Igor Stéphan, and Laurent Garcia.  Asperix, a first order forward chaining approach for answer set computing.  Theory and Practice of Logic Programming, 2015.  To appear, arXiv:1503.07717.
  * Lif [02] Vladimir Lifschitz.  Answer set programming and plan generation.  Artificial Intelligence, 138(1-2):39–54, 2002.
  * Lif [08] Vladimir Lifschitz.  What Is Answer Set Programming?  In AAAI Conference on Artificial Intelligence, pages 1594–1597, 2008.
  * LJN [12] Guohua Liu, Tomi Janhunen, and I Niemelä.  Answer set programming via mixed integer programming.  In Principles of Knowledge Representation and Reasoning (KR), pages 32–42, 2012.
  * LT [94] Vladimir Lifschitz and Hudson Turner.  Splitting a Logic Program.  International Conference on Logic Programming (ICLP), 19(1):23–37, 1994.
  * MG [13] Kyle Marple and Gopal Gupta.  Galliwasp: A goal-directed answer set solver.  In Logic-Based Program Synthesis and Transformation (LoPSTR), pages 122–136, 2013.
  * MTS+ [09] Paolo Mancarella, Giacomo Terreni, Fariba Sadri, Francesca Toni, and Ulle Endriss.  The CIFF Proof Procedure for Abductive Logic Programming with Constraints: Theory, Implementation and Experiments.  Theory and Practice of Logic Programming, 9(6):691–750, 2009.
  * Ng [92] Hwee Tou Ng.  A General Abductive System with Applications to Plan Recognition and Diagnosis.  Phd thesis, University of Texas at Austin, 1992.
  * NM [90] Hwee Tou Ng and Raymond J Mooney.  On the Role of Coherence in Abductive Explanation.  In National Conference on Artificial Intelligence, pages 337–342, 1990.
  * NM [92] Hwee Tou Ng and Raymond J Mooney.  Abductive Plan Recognition and Diagnosis: A Comprehensive Empirical Evaluation.  In Knowledge Representation and Reasoning (KR), pages 499–508, 1992\.
  * Pei [55] C S Peirce.  Abduction and Induction.  In Philosophical Writings of Peirce, chapter 11, pages 150–156. Dover Publications, 1955.
  * RD [06] Matthew Richardson and Pedro Domingos.  Markov logic networks.  Machine Learning, 62(1-2):107–136, jan 2006.
  * Sch [14] Peter Schüller.  Tackling Winograd Schemas by Formalizing Relevance Theory in Knowledge Graphs.  In International Conference on Principles of Knowledge Representation and Reasoning (KR), pages 358–367. AAAI Press, 2014.