As a programming paradigm, answer set programming (ASP) brings about the usual issue of the human error. Hence, it is desirable to provide automated techniques that could help the programmer to find the error. This paper studies the question of computing a subset-minimal correction of a contradictory ASP program. A contradictory ASP program is often undesirable and we wish to provide an automated way of fixing it. We consider a minimal correction set of a contradictory program to be an irreducible set of rules whose removal makes the program consistent. In contrast to propositional logic, corrections of ASP programs behave non-monotonically. Nevertheless, we show that a variety of algorithms for correction set computation in propositional logic can be ported to ASP. An experimental evaluation was carried showing that having a portfolio of such algorithms is indeed of benefit.
Answer set programming (ASP) is a powerful paradigm for modeling and solving combinatorial and optimization problems in artificial intelligence. An inconsistent program is such a program that does not have a solution. This might be due to a bug in the program and for such cases it is desirable to provide the programmer with tools that would help him identify the issue.
The primary motivation for this paper is to focus on program’s input. In theory, an input to an ASP program is really just another ASP program that is joined to the original one. In practice, however, the conceptual division between a program and its input plays an important role in the program’s development. Indeed, a program, as a set of rules, expresses the semantics of the problem being solved. The input is a set of facts describing a particular instance of the problem. Such input is typically large.
This paper asks the question, how to resolve situations when there is an error in the given input? In particular, we consider scenarios when the input leads to a contradiction in the program. Consider the following simple program.
← not move(a). (1) (2) (3) By rule (1) the program requires move(a) be true. To achieve that, however, stone(b) must be true and stone(c) must be false (by rule (2)). The input is specified as the fact (3). Altogether, the program is inconsistent since rule (2) is not applicable. If we wish to modify the input so it becomes consistent, the fact stone(c) must be removed and the fact stone(b) must be added. It is the aim of this paper to compute such corrections to inconsistent inputs. Further, we aim at corrections that are irreducible, i.e. that do not perform unnecessary changes. Note that this program could also be made consistent by modifying the rules (1) and (2). Similarly, one could add the fact move(a). This might be undesirable as these represent the rules of the modeled move (in a game, for instance). In the end, however, it is the programmer that must decide what to correct. The objective of the proposed tool-support is to pin-point the source of the inconsistency.
We show that the problem of inconsistency corrections is closely related to a problem of maximal consistency, which we define as identifying a subset-maximal set of atoms that can be added to the program as facts while preserving consistency. Maximal consistency lets us provide a solution to inconsistency correction but it is also an interesting problem to study on its own.
Maximal consistency is closely related to the concept of maximally satisfiable
sets (MSS) in propositional logic. For a formula in conjunctive normal form, an
MSS is a subset of the formula’s clauses that is satisfiable and adding any clause
to it makes it unsatisfiable. There is also a dual, minimal correction subset
(MCS), which is a complement of an MSS [
An important difference between propositional logic and ASP is that ASP
is not monotone. This means that an algorithm for calculating MSSes cannot
be immediately used for ASP. We show, however, that it is possible to port
existing MSS algorithms to ASP. This represents a great potential for calculating
maximally consistent sets in ASP as a bevy of algorithms for MSS exist [
The main contributions of this paper are the following. (1) It devises a technique for adapting algorithms from MSS computation to maximal consistency in ASP. (2) Using the technique a handful of MSS algorithms is adapted to ASP. (3) It is shown how maximal consistency can be used to calculate minimal corrections to ASP inputs. (4) The proposed algorithms were implemented and evaluated on a number of benchmarks. 2
We assume the reader’s familiarity with standard ASP syntax and semantics,
e.g. [
a ← b1, . . . , bm, not cm+1, . . . , not cn,
where a, bi, cj are atoms. A literal is an atom or its default negation not a. A rule
is called a fact if it has an empty body; in such case we don’t write the symbol ←.
For a rule r, we write body(r) to denote the literals b1, . . . , bm, not cm+1, . . . , not cn
and we write head(r) to denote the literal a. We write B+(r) for b1 . . . , bm
and B−(r) for cm+1, . . . , cn. Further, we allow choice rules of the form n ≤
{a1, . . . , ak}. (this is a special case of weight constraint rules [
A program is called ground if it does not contain any variables. A ground instance of a program P , denoted as grd(P ), is a ground program obtained by substituting variables of P by all constants from its Herbrand universe.
The semantics of ASP programs can be defined via a reduct [
P I =
head(r) ← B+(r) | r ∈ grd(P ), I ∩ B−(r) = ∅
The set I is an answer set of P if I is a minimal model of P I . Intuitively,
this definition guarantees that an answer set contains only atoms that are
justified by the rules of the program (cf. [
This section studies the problem of computing a maximal subset of given atoms whose addition to the program, as facts, yields a consistent program. Definition 1 (maximal consistent subset). Let P be a consistent ASP program and S be a set of atoms. A set L ⊆ S is a maximal consistent subset of S w.r.t. P if the program P ∪ {s. | s ∈ L} is consistent and for any L , such that L L ⊆ S, the program P ∪ s. | s ∈ L is inconsistent. If P is clear from the context, we simply say that L is an (in)consistent set of atoms.
The definition of maximal consistent subset is syntactically similar to maximal models or MSSes in propositional logic. Semantically, however, there is an important difference due to nonmonotonicity of ASP. While in propositional logic the satisfiability of φ∧x∧y guarantees satisfiability of φ∧x, in ASP it is not necessarily the case. Hence, algorithms for MSSes in propositional logic cannot be readily used for our maximal consistent subset. We will show, however, that it is possible to port these algorithms to ASP.
The following presentation uses the following auxiliary functions. The function choice(S) yields the choice rule 0 ≤ {s1, . . . , sk} over the set S = {s1, . . . , sk}. The function atleast1({s1, . . . , sk}) yields the choice rule 1 ≤ {s1, . . . , sk}. The function solve(P ) represents an ASP solver, which returns a pair (res, µ) where res is true and µ is an answer set of P if some exists. If P is inconsistent, res is false and µ is undefined.
A brute force approach to calculating a maximal consistent subset would be to enumerate all subsets of S and for each test whether it is still consistent. As there are 2| S | subsets of S, this approach is clearly unfeasible.
Algorithm 1: Atleast-1 algorithm for maximal consistency. 1 L ← ∅ 2 while true do 3 P ← P ∪ {s. | s ∈ L} 4 P ← P ∪ {atleast1(S 5 (res, µ) ← solve(P ) 6 if ¬res then return L 7 L ← µ ∩ S
L).}
A better approach is to maximize the number of s ∈ S that are set to true.
Such ensures finding a maximal consistent subset with maximum cardinality.
This can be done by iteratively calling an ASP solver while imposing increasing
cardinality on the set S. However, modern ASP solvers directly support
minimization constraints through which maximization can be specified by minimizing
negation of the atoms in S. This approach was taken elsewhere [
Finding a maximal correction subset with maximum cardinality might be computationally harder than finding some maximal correction subset. This is the purpose of the rest of the section.
We begin by an important observation that it is possible to check whether a set of atoms L can be extended into a consistent set of atoms by a single call to an ASP solver.
Observation 1 Let P be an ASP program, L ⊆ S be sets of atoms, and P be defined as P = P ∪ {s. | s ∈ L} ∪{choice(S L).}. There exists a consistent set L s.t. L ⊆ L ⊆ S iff P has an answer set µ such that L = S ∩µ.
Observation 1 enables us to check whether a set of atoms can be extended into a consistent set. This is done by letting the solver choose the additional atoms. Similar reasoning enables us to devise a test for checking that a consistent set L is already maximal. This is done by enforcing that L is extended by at least one element.
Observation 2 Let P be an ASP program and S be a set of atoms, and P be defined as P = P ∪ {s. | s ∈ L} ∪{atleast1(S L)}. A set L ⊆ S is a maximal consistent subset of S iff P ∪ {s. | s ∈ L} is consistent and P is inconsistent.
Combining Observation 1 and Observation 2 gives us Algorithm 1. The algorithm maintains a lower bound L, which is initialized to the empty set. The set L grows incrementally until a maximal set is found. In each iteration it is tested whether L is already maximal in accord with Observation 2. The invariant of the loop is that the program P ∪ {s. | s ∈ L} is consistent. The set L grows monotonically with the iterations because whenever a new answer set µ is obtained, it must contain all the atoms from the previous L. Hence, the algorithm terminates in at most |S| calls to an ASP solver. Note that the algorithm does not necessarily need all of the |S| iterations since more than one element might be
Algorithm 2: Iterative algorithm for maximal consistency.
1 L ← ∅
2 while S = ∅ do
3 sf ← pick an arbitrary element from S
4 S ← S {sf }
5 L ← L ∪{sf }
6 P ← P ∪{choice(S).}
7 P ← P ∪ {s. | s ∈ L}
8 (res, µ) ← solve(P )
9 if ¬res then L ← L {sf }
10 else L ← L ∪(µ ∩ S)
11 return L
added to L in one iteration. Similar algorithms have been proposed in different
contexts, including computing the backbone of a propositional formula [48] and
computing a minimal correction set (MCS) of a propositional formula [
The second algorithm we propose also maintains a lower bound on a maximal consistent set and tests, one by one, the elements to be added. The pseudo-code can be found in Algorithm 2. In each iteration it tests whether an element sf can be added to the current lower bound L. If it is possible, the algorithm continues with a larger L. If it is not, then sf is removed from L and never inspected again.
In contrast to Algorithm 1, here it is not immediately clear that the returned
set is indeed maximal. Indeed, how do we know that if it was impossible to add
some element sf to an earlier L1, that is it still impossible for the final Lf ?
This follows from Observation 1 and from the fact that L grows monotonically
throughout the algorithm. More precisely, it holds that L1 ⊆ Lf and our test
checks that sf cannot be added to any superset of L1, i.e. if it was not possible to
extend L1 with sf , then it is also impossible to extend Lf with it. As Algorithm 1,
Algorithm 2 also performs at most | S | calls to an ASP solver. Similar algorithms
have been proposed in a number of contexts, including computing an MCS [
The third algorithm we consider is inspired by the progression algorithm [
Algorithm 3: Progression-based algorithm for maximal consistency. In this section we see how maximal consistency is useful for calculating corrections to an inconsistent program. Hence, the objective is to calculate an irreducible correction to a given inconsistent program so it becomes consistent.
The concept of (minimal) correction sets commonly appears in propositional
logic [
Enabling corrections by addition brings about a substantial difficulty as the universe of rules that can be potentially added to the program can be easily unwieldy or even infinite. Hence, we assume that the user (the programmer) provides us with a set of rules R that can be removed from the program and a set of rules A that can be added to the program.
Definition 2 ((A, R)-correction). Let A and R be sets of rules and P be an inconsistent logic program. An (A, R)-correction of P is a pair (Mr, Ma) such that Mr ⊆ R and Ma ⊆ A and the program (P \ Mr) ∪ Ma is consistent.
An (A, R)-correction (Mr, Ma) is minimal if for any (A, R)-correction (Mr, Ma) such that Mr ⊆ Mr and Ma ⊆ Ma, it holds that Ma = Ma and Mr = Mr.
We refer to the problem of calculating a minimal correction as MinCorrect; it accepts as input sets A, R, and a program P and outputs a pair (Mr, Ma) in accord with Definition 2.
We show how to translate MinCorrect to maximal consistent subset calculation. Construct a program P from P as follows3. 1. Introduce fresh atoms srr for each r ∈ R and sra for each r ∈ A. 2. Replace each rule r ∈ R with head(r) ← srr, body(r) a 3. Replace each rule r ∈ A with head(r) ← not sr, body(r).
Let S = {srr | r ∈ R} ∪ {sra | r ∈ A}. Then any maximal consistent subset L of S w.r.t. P gives us a solution to MinCorrect by setting Mr = {r | srr ∈/ L} and Ma = {r | sra ∈/ L}. It is easy to see why that is the case. From the definition of maximal consistent subset, there must be an answer set µ of the program P ∪ {s. | s ∈ L}. If srr ∈ µ for r ∈ R, then µ also satisfies the original rule r, hence it is not necessary to remove r to achieve consistency. Similarly, if sra ∈ µ, then the body of head(r) ← not sra, body(r) is false, i.e. the rule is ineffective, and therefore it is not necessary to add the rule r to the original program to achieve consistency. Conversely, adding any further srr or sra to µ leads to inconsistency due to the definition of maximal consistent subset. Hence, Mr and Ma defined as above are irreducible. 4.1
Minimal Corrections for Program Inputs Here we come back to the problem that we used to motivate the paper in the introduction, which is to calculate corrections of program’s data so that the program becomes consistent. Hence, we assume that there is a program Pe— representing the encoding of the problem and a program Pd—representing data to the encoding, consisting only of facts. Assuming that Pe ∪ Pd is inconsistent, we wish to identify correction to Pd that would make it consistent.
For such, we use the concept of minimal corrections as described above. What is needed is to specify the sets R and A. To specify the set R, the user just needs to identify facts in the given input that can be removed. This can for instance be done by giving predicate names. Specifying the set A is more challenging because it may comprise facts that do not appear in the program. Hence, we let the user give expressions E of the form p(A1) : t(A2) where p and t are predicate symbols and A1,A2 appropriate arguments. The set A is obtained by an additional call to an ASP solver. This call constructs a program r P just as above and adds the rule atleast1 ({sr | r ∈ R} ∪ {E1, . . . , Eu}). If this call is successful, the obtained answer set contains facts of the form p(A1) that constitute the set A. 5
The proposed algorithms were implemented using the state-of-the-art ASP solver
clingo [
ASP solver is invoked repeatedly from a python script. Computing a cardinalitymaximal consistent subset was done by a single call to clingo, using the minimization rule syntax (:∼). For readability we refer to the individual approaches by single letters, Algorithm 1–letter a (atleast-1 constraint); Algorithm 2–letter u (unit addition); Algorithm 3–letter p (progression); the maximization approach is denoted by x. The evaluation was carried out on machines with Intel Xeon 5160 3GHz and 4GB of memory. The time limit was set to 1000 seconds and the memory limit to 2GB. The experimental evaluation considers several problems from the 2013 ASP Competition4. The following classes were considered.
Solitaire. In the game a single player moves and removes stones from the board according to the rule that a stone can be moved by two squares if that move jumps over another stone; the stone being jumped over is removed (similarly to Checkers). The problem to be solved in the context of this game is to perform T steps given T and an initial configuration. For instance, the problem does not have a solution if the board contains only one stone and at least one move is required to be made.
The size of the board is 7x7 with 2x2-size corners removed, thus comprising 33 squares. The initial configuration of the board is given by the predicates empty(L) and full(L), where L is a square of the board. The set R was specified as containing all the input’s facts using empty and full. The set A was specified by the expressions empty(L) : location(L) and full(L) : location(L).
To generate unsatisfiable instances of the game, initial board configurations were generated randomly and the parameter T (number of steps) were fixed. We considered T = 12 and T = 16; 100 instances were generated for each T and only the inconsistent ones were considered. This process was repeated for other benchmarks.
Knight tour with holes. The input is a chessboard of size N ×N with H holes. Following the standard chess rules, a knight chess piece must visit all non-hole positions of the boards exactly once and return to the initial position (which may be chosen). The objective of correction was to remove as few holes as possible so that the tour is possible. Random hole positions were generated for fixed N and H. Instances with N = 8, H = 4 and N = 8, H = 10 were considered.
Graceful graphs. Given a graph (V, E) the task is to determine whether it is possible to label its vertices with distinct integers in the range 0..|E| so that each edge is labeled with the absolute difference between the labels of its vertices and so that all edge labels are distinct (such graph is called graceful ). The correction, for a given graph that is not graceful, tries to find its subgraph that maintains as many edges as possible (a single-edge graph is graceful). Considered instances were generated with |V | = 10 and |E| = 50 and |V | = 30 and |E| = 20.
Permutation Pattern Matching. The problem’s input are two permutations T and P . The task is to determine whether T contains a subsequence that is order-isomorphic to P . For the purpose of correcting we consider T and P so that P is not an order-isomorphic subsequence of T with the objective of adding and 4 https://www.mat.unical.it/aspcomp2013/FrontPage
Family a p u x VBS
knight [
Table 1 shows the number of solved instances by each of the approaches for
the different benchmark families. The last column shows the virtual best solver
(VBS), which is calculated by picking the best solver for each of the instances.
While the progression-based algorithm (p) is clearly in the lead, it is not a winner
for all the instances (or even classes of instances). Indeed, the virtual best solver
enables us to solve almost 20 more instances compared to the progression-based
approach. The strength of progression shows on benchmarks with larger target
sets. Such is the case for the class graceful graphs [
Out of the considered algorithms, cardinality maximization (x) performs the worst. The scatter plot in Fig 2 compares progression to cardinality maximization. There are some instances where maximization performs well but overall progression dominates maximization; by orders of magnitude in a number of cases.
VBS p u a x 300 350
400 instances 450 500
While Algorithms 1–3 give us an advantage over the cardinality maximization approach, the data so far does not show how the minimal corrections differ from the minimum-cardinality corrections in size. This is shown in Table 2. The table shows a distribution of how much the value |Ma| + |Mr| differs from the value obtained from the approach x. For instance, row p, column 3 shows that in 12 cases the value differs by 3 from the minimum one. Naturally, these data only come from instances where x and the given approach finished with success. The distributions have a characteristic “heavy tail”. In the majority of cases, the actual minimum is obtained (over 300 for all the approaches). Outliers exist but they are small in numbers. 6
The proposed approach is closely related to the work on debugging on answer set
programs, which has a long history [
Nevertheless, the existing work on ASP debugging (in particular [
Other approaches to maximality in ASP exist. In particular, Gebser et al. [
Some of the algorithms described in the paper are inspired by work on
computing MSS/MCSes of propositional formulas in conjunctive normal form, which
in term can be traced back to Reiter’s seminal work on model-based
diagnosis [
Although the paper considers a restricted sample of algorithms for
computing MCS algorithms, adapted from [
Our approach to effectively modifying the debugged program is conceptually
akin to belief revision and abduction reasoning in ASP [
Minimization in the context of ASP is addressed in asprin [
Motivated by debugging of data to ASP programs, the paper studies the problem of minimal (irreducible) corrections of inconsistent programs and the problem of maximal consistency. The two problems are closely related. Indeed, a minimal correction to an inconsistent program can be calculated by computing a maximal consistency with respect to only slightly modified program.
We show that algorithms for calculating maximally satisfiable sets (MSSes) in propositional logic can be adapted to ASP. This is an interesting result as unlike propositional logic, ASP is non-monotonic. For three MSS algorithms we show how they are ported to ASP (Algorithms 1–3). A similar approach, however, could be used for other MSS algorithms.
The algorithms for maximal consistency let us then calculate minimal
corrections. For these corrections we assume a general scheme where rules may be
added or removed in order to restore consistency. For evaluation we return to the
initial motivation of the paper and that is the calculation of corrections to data
that make a program inconsistent. A number of instances from various problem
classes were considered. The progression-based algorithm (Algorithm 3) turned
out to be the most effective overall. Nevertheless, it was not a winner for each
of the considered classes. In contrast, the maximum-cardinality approach clearly
performed the worst. Here, however, we should point out that we used the
default implementation of minimization in clingo and it is the subject of future
work to evaluate other algorithms. (A number of MaxSAT algorithms are being
adapted to Max-ASP [
The paper opens a number of avenues for future work. Irredundancy is needed
in other approaches to debugging, e.g. [
Acknowledgments. This work was supported by national funds through Funda¸c˜ao para a Ciˆencia e a Tecnologia (FCT) with reference UID/CEC/50021/2013 and by FCT funding of LASIGE Research Unit, reference UID/CEC/00408/2013. 42. Schulz, C., Satoh, K., Toni, F.: Characterising and explaining inconsistency in logic programs. In: Logic Programming and Nonmonotonic Reasoning (LPNMR). pp. 467–479 (2015) 43. Simons, P.: Extending the stable model semantics with more expressive rules. In:
Gelfond et al. [