Unsatisfiable Core Shrinking for Anytime Answer Set Optimization

1 Introduction

In answer set programming (ASP), programs are associated with stable models [Gelfond and Lifschitz, 1991; Niemelä, 1999; Marek et al., 2008; Lifschitz, 2008; Eiter et al., 2009; Brewka et al., 2011], i.e., classical models satisfying a stability condition: only necessary information is included in a model of the input program under the assumptions provided by the model itself for the unknown knowledge in the program, where unknown knowledge is encoded by means of default negation. Reasoning in presence of unknown knowledge is common for rational agents acting in the real world. It is also common that real world agents cannot meet all their desiderata, and therefore ASP programs may come with soft literals for representing numerical preferences over jointly incompatible conditions. Stable models are therefore associated with a cost given by the number of the unsatisfied soft literals, so that stable models of minimum cost are preferred.

It is important here to stress the meaning of the word preferred: any stable model describes a plausible scenario for the knowledge represented in the input program, even if it may be only an admissible solution of non optimum cost. In fact, many rational agents would still accept suboptimal solutions, possibly with an estimate on the maximum distance to the optimum cost. This flexibility is also justified by the intrinsic complexity of the problem: the computation of an optimum stable model requires in general at least linearly many calls to a S P 2 oracle [Buccafurri et al., 2000], and it is therefore practically unfeasible for the hardest instances.

∗This work is based on a paper presented at the 32nd International Conference on Logic Programming (ICLP 2016) [Alviano and Dodaro, 2016], and was partially supported by the National Group for Scientific Computation (GNCS-INDAM), and by project "Smarter Solutions in the Big Data World (S2BDW)" funded by the Italian Ministry for Economic development (MISE), PON "Imprese e competitività" 2014-2020.

According to the above observations, a good algorithm for answer set optimization should produce better and better stable models during the computation of an optimum stable model. Algorithms having this property are called anytime in the literature [Alviano et al., 2014; Bliem et al., 2016]. However, the most efficient algorithms are not anytime by themselves: they are based on unsatisfiable core analysis [Alviano et al., 2015b], which means that they try to satisfy all soft literals, possibly replacing those in the input program with less restricting constraints until an optimum stable model is found.

Anytime variants of these algorithms are obtained thanks to following simple observation [Alviano and Dodaro, 2016b]: Unsatisfiable cores are often non-minimal, and their sizes can be significantly reduced by a few additional oracle calls, where each call may either return a smaller core, or a stable model possibly improving the current overestimate. Within this respect, we implemented two strategies, referred to as linear and reiterated progression based shrinking.

Interestingly, the overhead introduced by the additional oracle calls is often mitigated by the performance gain obtained thanks to the smaller unsatisfiable cores that the algorithm has to analyze. Indeed, we provide empirical evidence that often the running time of our core based algorithm sensibly decreases when core shrinking is performed (Section 4). The advantage of introducing our strategy for core shrinking is also confirmed by a comparison with CLASP [Gebser et al., 2015a]: even if our solver, WASP [Alviano et al., 2015a; Alviano and Dodaro, 2016a], is in general slower than CLASP at completing stable model searches, its performance is sufficiently improved by core shrinking that the two solvers are almost on par in terms of solved instances, with the crucial difference that WASP provides both overestimates and underestimates during the computation, while ones or the others are produced by CLASP only after running to completion.

2 Background

Let A be a set of (propositional) atoms comprising ⊥. A literal is an atom p preceded by zero or more occurrences of the default negation symbol ∼. A rule r is an implication H(r) ←B(r), where H(r) is a disjunction of atoms, and B(r) is a conjunction of literals. H(r) and B(r) are called head and body of r, and abusing of notation also denote the sets of their elements. If H(r) ⊆{⊥}, then r is called integrity constraint. A program P is a set of rules. Let At(P) denote the set of atoms occurring in P.

An interpretation I is a set of atoms not containing ⊥. Relation |= is inductively defined as follows: for p ∈A , I |= p if p ∈ I; I |= ∼ℓ if I ̸|= ℓ; for a rule r, I |= B(r) if I |= ℓ for all ℓ ∈ B(r), and I |= r if I ∩H(r) ̸= /0 whenever I |=B(r); for a program P, I |=P if I |= r for all r ∈P. I is a model of a literal, rule, or program p if I |=p.

The reduct P I of a program P with respect to an interpretation I is obtained from P by removing any rule r such that I ̸|= B(r) is removed, and then by removing any negated literal. An interpretation I is a stable model of a program P if I |=P, and there is no J ⊂ I such that J |=P I . Let SM(P) denote the set of stable models of P. A program P is coherent if SM(P) ̸= /0; otherwise, P is incoherent.

In order to simplify the presentation, a program P may include count constraints of the form COUNT{ℓ1, . . . ,ℓn} ≥ k, where ℓ1, . . . ,ℓn (n ≥ 0) are literals, and k ≥ 0, to enforce |{i ∈ [1..n] | I |= ℓi}| ≥ k for all I ∈ SM(P).

For a set S of literals, called soft, the cost of an interpretation I is S(I) := |{ℓ ∈ S | I ̸|= ℓ}|, that is, the number of false soft literals. I is an optimum stable model of a program P with respect to S if I ∈ SM(P), and there is no J ∈ SM(P) such that S(J) < S(I). Let OSM(P,S) denote the set of optimum stable models of P with respect to S. Optimum stable model search is the following computational problem: Given a (coherent) program P and a set of soft literals S, compute an optimum stable model I ∗ ∈ OSM(P, S).

Example 1 Let P1 be the following program:

Its stable models are I1 = {b, c}, I2 = {a, b} and I3 = {a, c, d}, and the associated reducts are the following:

P I1

1 : b← c←

P I2

1 : a← b∨c←a b∨d ←a b←

P I3

1 : a← b∨c←a b∨d ←a

If S = {∼a,∼b,∼c,∼d} is a set of soft literals, the associated costs are S(I1) = S(I2) = 2, and S(I3) = 3. Hence, OSM(P1, S) = {I1, I2}. ■

3 Optimum Stable Model Search via Unsatisfiable Core Analysis

Modern ASP solvers accept as input a set L of literals, called assumptions, in addition to the usual logic program P, and return a stable model I of P such that L ⊆ I, if it exists; otherwise, they return a set C ⊆ L such that P∪{⊥←∼p | p ∈C} is incoherent, which is called unsatisfiable core.

Example 2 Consider program P1 from Example 1. If S = {∼a,∼b,∼c,∼d} is the set of assumptions, the unsatisfiable cores are {∼a,∼b}, {∼a,∼c}, {∼b,∼c}, {∼b,∼d}, and their supersets. ■

The algorithm presented in this paper is ONE, reported as Algorithm 1 (lines 4-10 will be injected later to shrink unsatisfiable cores). A stable model containing all soft literals is searched (line 2). If found, it is an optimum stable model. Otherwise, an unsatisfiable core {p0, . . . , pn} is returned; since at least one of p0, . . . , pn must be false in any optimum stable model, the lower bound is increased by one, and the problem is relaxed so that the next call to function solve has to search for a stable model satisfying at least n literals among p0, . . . , pn. Symmetry breakers of the form ⊥← si,∼si+1 are also added to P, so that si is true if and only if at least n-i+1 literals among p0, . . . , pn are true.

Example 3 Consider program P1 and soft literals S = {∼a,∼b,∼c,∼d} from Example 1. A stable model for the program P1 and assumptions S is searched, and an unsatisfiable core is returned. Assume that the returned unsatisfiable core is S itself. The lower bound lb is set to 1, the set S is now equal to {s1, s2, s3} and P1 is extended with the following rules:

A stable model for the assumptions {s1,s2,s3} is searched and an unsatisfiable core, say {s1}, is returned. The lower bound lb is set to 2, the set S is now equal to {s2,s3}. (Note that the program is extended with the count constraint COUNT{s1} ≥ 0, which however is trivially satisfied.) A stable model for the assumptions {s2,s3} is searched and the answer set I ′1 = {b,c,s2,s3} is found. Thus, the algorithm terminates returning I ′1 ∩ {a, b, c, d} = {b, c} = I1. ■

The analyzed unsatisfiable cores significantly influence the execution of the algorithm, as the set of assumptions and the introduced rules are different for different unsatisfiable cores.

Example 4 Suppose that the first unsatisfiable core returned by function solve for P1 and S from Example 1 is {∼a,∼b,∼c}. Set S becomes {∼b,s1,s2} and P1 is extended with the following rules:

The next unsatisfiable core may be {∼d,s1}; therefore, S becomes {s2, s3}, and P1 is extended with the following rules:

At this point a stable model, say I ′1 = {b,c,s2,s3}, is found, and I ′1 ∩{a,b,c,d}={b,c}= I1 is returned. ■

Note that the algorithm described in this section is completely silent, as it essentially runs to completion without printing any suboptimal stable models. The goal of the next section is to circumvent such a drawback.

3.1 Unsatisfiable Core Shrinking

Unsatisfiable cores returned by function solve are not subset minimal in general. The non-minimality of the unsatisfiable core is justified both theoretically and practically: linearly many coherence checks are required in general to verify

Algorithm 1: Unsatisfiable Core Analysis with ONE

Input : A coherent programP, and a nonempty set of soft literals S. Output: An optimum stable model I ∗ ∈ OSM(P, S). 1 lb :=0; ub :=¥; V :=At(P); // init bounds and visible atoms 2 (res, I,C) := solve(P,{p ∈ S}); 3 if res is COHERENT then I ∗ := I ∩V; return I ∗ ; 11 Let C be {p0, . . . , pn} (for some n ≥ 0), and s1, . . . , sn be fresh atoms; 12 P :=P∪{si ←∼∼si | i ∈ [1..n]}∪{⊥←si,∼si+1 | i ∈ [1..n-1]}∪{COUNT{p0, . . . , pn,∼s1, . . . ,∼sn}≥n}; 13 lb := lb+1; S := (S\C)∪{s1, . . . ,sn}; goto 2; // try to solve the relaxed problem

4 m :=-1; pr :=1; 5 Let C be {p0, . . . , pn} (for some n ≥ 0); 6 (res, I,C′ ) := solve_with_budget(P,{pi | i ∈ [0..m+pr]}); 7 if res is INCOHERENT thenC :=C′ ; // smaller core found 8 if res is COHERENT and lb+S(I) <ub then I ∗ := I ∩V; ub := lb+S(I); 9 if m+2 · pr ≥ |C|-1 then m :=m+pr; pr :=1/2; // reiterate progression 10 if m+2 · pr < |C|-1 then pr :=2 · pr; goto 5; // increase progression

the minimality of an unsatisfiable core, hence giving a D P 3 - complete problem; on the other hand, extracting an unsatisfiable core after a stable model search failure is quite easy and usually implemented by identifying the assumptions involved in the refutation. The non minimality of the analyzed unsatisfiable cores may affect negatively the performance of subsequent calls to function solve due to aggregation over large sets. However, it also gives an opportunity to improve Algorithm 1: the size of unsatisfiable cores can be reduced by performing a few stable model searches within a given budget on the running time. In more detail, Algorithm 2 is injected in Algorithm 1. It implements a progression search in the unsatisfiable core {p0, . . . , pn}: the size of the assumptions passed to function solve_with_budget is doubled at each call (line 10), and the progression is reiterated when all assumptions are covered (line 9). If solve_with_budget terminates within the given budget, it either returns a smaller unsatisfiable core (line 7), or a stable model that possibly improves the current upper bound (line 8).

Example 5 Consider again the program from Example 3 and the unsatisfiable core {∼a,∼b,∼c,∼d} returned after the first call to function solve. The shrinking process searches a stable model with assumption {∼a}, and I1 = {b,c} may be found within the allotted budget. In any case, a stable model satisfying the assumptions {∼a,∼b} is searched, and the unsatisfiable core {∼a,∼b} may be returned if the budget is sufficient. Otherwise, the progression is reiterated, and one more soft literal is added to the assumptions. Hence, {∼a,∼b,∼c} may be returned as an unsatisfiable core if the budget is sufficient. Otherwise, the original unsatisfiable core is processed. ■

As an alternative, the shrinking procedure reported in Algorithm 2 can be modified as follows: variable pr is not doubled in line 10, but instead it is incremented by one, i.e., pr := pr+1. The resulting procedure is called linear based shrinking. For unsatisfiable cores of size 4 or smaller, as those considered in Example 5, the two shrinking procedures coincide, while in general linear based shrinking performs more stable model searches.

4 Implementation and Experiment

Algorithm ONE [Alviano et al., 2015c] has been implemented in WASP, an ASP solver based on completion [Alviano and Dodaro, 2016c] also supporting, among other algorithms, linear search sat-unsat (LINSU). Within LINSU, a first stable model is searched to obtain an upper bound of the optimum cost, and subsequent searches are constrained to improve the current upper bound, until an incoherence arises. The implementation of ONE optionally includes the two shrinking procedures described in Section 3.1, so that both underestimates and overestimates can be produced by WASP in any case, weighted or unweighted. Currently, the time budget of function solve_with_budget is fixed to 10 seconds, but the architecture of WASP can easily accommodate alternative options, such as a budget proportional to the time required to find the unsatisfiable core to be shrank.

WASP also implements disjoint cores analysis, which is essentially a preliminary step where only soft literals in the input are passed as assumptions to function solve, while new soft literals introduced by the analysis of detected cores are temporarily ignored. Disjoint cores analysis terminates with the detection of a stable model, and after that algorithm ONE is run not distinguishing between initial and new soft literals.

In order to assess empirically the impact of these shrinking procedures to the performance of WASP, benchmarks (with soft literals) from the ASP Competition 2015 [Gebser et al., 2015b] were considered, namely Abstract Dialectal Framework, Still Life, Crossing Minimization, Max Clique, MaxSAT, Steiner Tree, System Synthesis, Valves Location, and Video Streaming. Moreover, WASP was also compared with CLASP [Gebser et al., 2015a], which implements linear search sat-unsat (strategy bb,1) and OLL (strategy usc,1 with disjoint cores analysis; [Andres et al., 2012; Morgado et al., 2014]), a core based algorithm that inspired the definition of ONE. Both solvers were tested with the disjoint cores analysis. The experiments were run on an Intel Xeon 2.4 GHz with 16 GB of memory, and time and memory were limited to 20 minutes and 15 GB, respectively.

An overview of the obtained results is given in Figure 1. As a first comment, the fact that CLASP is in general faster than WASP to complete stable model searches is confirmed by comparing the performance of the two solvers running linear search sat-unsat (CLASP solves 29 instances more than WASP) or the core based algorithms (difference of 9 instances). This gap is completely filled by adding the shrinking procedures. Concerning the average execution time of the tested algorithms, the graph highlights that core based algorithms are faster than linear search sat-unsat in more testcases. Moreover, and more important, the addition of core shrinking does not add overhead to WASP. The main reason for this performance improvement is that shrinking a core often implies that subsequently found unsatisfiable cores are smaller: The cumulative number of literals in the analyzed cores is reduced by at least 68% when shrinking is performed (excluding Steiner Tree, System Synthesis and Video Streaming, for which WASP found few unsatisfiable cores). The budget is reached at least once in each problem, and often no more than 2 times, with a peak of 20-25 times on average for instances of Max Clique and Still Life.

Another advantage of unsatisfiable core shrinking is that better and better stable models are possibly discovered while computing an optimum stable model. In order to measure the impact of our strategies within this respect, let us define the estimate error e of the last stable model produced by Algorithm 1 as follows:

Hence, the cost associated with the stable model returned by Algorithm 1 is at most e(ub, lb) times greater than the cost of an optimum stable model. Such a measure is not applicable to instances of Abstract Dialectical Framework and System Synthesis because of technicality not discussed in this paper.

Table 1 reports the number of instances for which WASP produced a stable model within a given error estimate. In particular, the first row shows the number of instances for which an optimum stable model was computed (error estimate is 0). The last row, instead, shows the number of instances solved with error estimate bounded by 1, and smaller values for the error estimate are considered in the intermediate rows. It is interesting to observe that the stable model produced after the analysis of all disjoint cores is already sufficient to obtain an error estimate bounded by 100% for many tested instances. However, many of these stable models have an error estimate greater than 25%. In this case, adding core shrinking leads to better results.

For the sake of completeness, also CLASP is included in Table 1. However, since CLASP does not print any lower bound, the best value for lb produced by WASP is combined with the upper bounds given by CLASP running LINSU and OLL. If an error estimate of 100% is acceptable, then the number of stable models produced by CLASP is aligned with WASP, or even better. However, when the error estimate must be less or equal than 50%, the combination of disjoint cores analysis and core shrinking implemented by WASP leads to better results in this benchmark.

5 Conclusion

The combination of ASP programs and soft literals is important to ease the modeling of optimization problems. However, the computation of optimum stable models is often very hard, and suboptimal stable models may be the only affordable solutions in some cases. Despite that fact, efficient algorithms based on unsatisfiable core analysis are not anytime. A concrete strategy to turn them into anytime algorithms is given by a shrinking procedure applied to unsatisfiable cores before their analysis: better and better stable models are produced, and eventually a performance gain is obtained thanks to the reduced size of the analyzed unsatisfiable cores. (An alternative technique was introduced in MaxSAT, where one literal is iteratively removed from the unsatisfiable core, either obtaining a smaller unsatisfiable core, or a necessary literal in the processed unsatisfiable core [Nadel, 2010; Nadel et al., 2014].) On the instances of the Sixth ASP Competition, our implementation is often able to provide (suboptimal) stable models with a guarantee of distance to the optimum cost of around 10%.