A Formal Approach for Cautious Reasoning in Answer Set Programming (Extended Abstract)

1 Introduction

Abstract solvers are a method to formally analyse solving algorithms. In this methodology, the states of a computation are represented as nodes of a graph, the solving techniques as edges between such nodes, the solving process as a path in the graph, and formal properties of the algorithms are reduced to related graph properties. This framework enjoys some advantages w.r.t. traditional ways such as pseudo-codebased descriptions, e.g., being based on formal and wellknown, yet simple, mathematical objects like graphs, which helps (i) comparing solving algorithms by means of comparison of their related graphs, (ii) mixing techniques in different algorithms in order to design novel solving solutions, by means of mixing arcs in the related graphs, and (iii) stating and proving formal properties of the solving algorithms, by means of reachability within the related graphs. Abstract solvers methodology was introduced in 2006 for Propositional Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) [Nieuwenhuis et al., 2006], and was the basis for the design and implementation of the BARCELOGIC SMT solver awarded as winner of some tracks at the 2005 SMT Competition. Then, it proved to be useful in various fields such as Quantified SAT [Brochenin and Maratea, 2015b], Answer Set Programming [Lierler, 2011; Lierler and Truszczynski, 2011; Brochenin et al., 2014], and Constraint ASP [Lierler, 2014], for analysing current algorithms, proposing and/or implementing new solvers based on the analysis.

∗ Summary of the ICLP 2019 paper [Amendola et al., 2019].

†Contact Author

In ASP, abstract solvers have been so far mainly applied to ASP solvers for brave reasoning tasks where, given an input query and a knowledge base, answers are witnessed by some stable model [Gelfond and Lifschitz, 1988], or answer set.

However, in ASP, also cautious reasoning has been deeply studied in the literature: differently from the previous task, answers here must be witnessed by all stable models. This task has found a significant number of interesting applications as well, including consistent query answering [Arenas et al., 2003; Manna et al., 2013], data integration [Eiter, 2005], multi-context systems [Brewka and Eiter, 2007], and ontology-based reasoning [Eiter et al., 2008]. Two of the most well-known ASP solvers, i.e., DLV [Leone et al., 2006] and CLASP [Gebser et al., 2012], have been extended for computing cautious consequences of ASP programs. Several algorithms for cautious reasoning in ASP, including those implemented in DLV and CLASP, borrowed from the backbone computation of Boolean formulas [Janota et al., 2015], have been presented in a unified, high-level view in [Alviano et al., 2014]. Moreover, some of these techniques have been implemented on top of the ASP solver WASP [Alviano et al., 2019], and further strategies have been analyzed through abstract solvers in [Brochenin and Maratea, 2015a].

In this paper we design, implement and test novel abstract solutions for cautious reasoning tasks in ASP. We show how to improve the current abstract solvers with further techniques borrowed from backbone computation in SAT, in order to design new solving algorithms. In particular, we import a technique called "chunk", which generalizes previous techniques by testing a set of atoms simultaneously, and core-based algorithms, which can be considered either a solution per se, or a way for pruning the set of atoms to be considered, given that they can not guarantee completeness. By doing so, we also formally show, through a uniform treatment, a strong relation among algorithms for solving cautious reasoning tasks in ASP and those for computing backbones of Boolean formulas. Finally, we implement some of the new solutions in the solver WASP and we show that their performances are comparable to state-of-the-art solutions. This paper is a summary of the best technical ICLP 2019 paper [Amendola et al., 2019].

2 Preliminaries

Here, we recall basics on Answer Set Programming (ASP); Boolean logic formulas; and abstract solvers framework.

2.1 Boolean Formulas and Answer Set Programs

We define ASP programs and Conjunctive Normal Form (CNF) formulas so as to underline similarities, thus to compare algorithms on CNF formulas and ASP programs.

Syntax. Let Σbe a propositional signature. An element a ∈ Σ is called atom or positive literal. The negation of an atom a, i.e., ¬a, is called negative literal. Given a literal l, we define |l| = a, if l = a or l = ¬a, for some a ∈ Σ. For a set of atoms X ⊆ Σ, a literal relative to X is a literal l s.t. |l| ∈ X, and lit(X) is the set of all literals relative to X. We set ¯l = a, if l = ¬a, and ¯l = ¬a, if l = a. A clause is a set of literals (seen as a disjunction). A CNF formula is a set of clauses (seen as a conjunction). Given a set of literals M, we denote by M + (resp., M -) the set of positive (resp., negative) literals of M, and by M the set {¯l | l ∈ M}. M is consistent if l ∈ M implies ¯l ̸∈ M. A rule is a pair (A,B), written A ← B, where B is a set of literals and A is an atom or ∅. A program is a finite set of rules. Given a set of literals M, a program Π and a CNF formula Φ, we denote by atoms(M), atoms(Π) and atoms(Φ) respectively the set of atoms occurring in M, Π , and Φ. Note that in Boolean logic ¬ is classical negation, while in ASP it is negation by default.

Semantics. Let X be a set of atoms, Φ a CNF formula, and Π a program. An assignment to X is a total mapping from X to {⊥,⊤}. A consistent set M of literals is an assignment to atoms(M) s.t. a ∈ M iff a is mapped to ⊤, and ¬a ∈ M iff a is mapped to ⊥. A model of Φ is an assignment M to atoms(Φ) s.t. for each clause C ∈ Φ, M∩C ̸= ∅. A model of Π is an assignment M to atoms(Π) s.t. for each rule (A, B) ∈ Π , A∩M ̸= ∅ or B ̸⊆ M. Let M(Φ) be the set of all models of Φ. The reduct Π X of Π w.r.t. to X is obtained from Π by deleting each rule A ← B+ ∪B- s.t. X∩atoms(B-) ̸= ∅ and replacing each remaining rule with A ← B+. An answer set of Π is a model M s.t. M + is minimal among the M + 0 s.t. M0 is a model of Π M+ . Let AS(Π) be the set of all answer sets of Π. We define backbone(Φ) = ⋂M∈M(Φ) M +and cautious (Π ) = ⋂M∈AS(Π) M +.

2.2 Abstract Solvers

Abstract solvers are graphs that represent the status of the computation, and how it changes in response to an application of a technique in a search for a solution with certain properties, e.g., the satisfiability of a formula. We present the notion of states, transition rules, and abstract solver graphs.

States. Let X be a set of atoms. We denote by A(X) the set of action relative to X. A record relative to X is a string L from lit(X) without repetitions. We may view a record as the set containing all its elements stripped from their annotations. For example, we may view ¬ab as {¬a, b}, and hence as the assignment that maps a to ⊥ and b to ⊤. Let Π be a program, and X = atoms(Π). The set of the states relative to Π is the union of: core states relative to

Π: LO,U,A,P where O,U ⊆ X, A ∈ A(X), and P is a program depending by Π, O, U, A (e.g., ¬ab{a,b},∅,A,P , ∅{a},{b},A,P , ¬a¬b¬c∅,∅,A,P ); control states relative to X: Cont(O,U) where O,U ⊆ X (e.g., Cont({a, b}, {a}), Cont({a, b, c}, ∅), Cont(∅, ∅)); terminal states relative to X: Ok(W) where W ⊆ X (e.g., Ok({a, b, c}), Ok(∅)). Intuitively, these states represent computation steps of the algorithms that search for assignments with certain properties, in our case backbone or cautious consequences. Core states LO,U,A,P and control states Cont(O,U) represent all the intermediate steps of the computation, where L is the current state of the computation of a model; O is the current over-approximation of the solution; U is the current underapproximation of the solution; and A is the action currently carried out. Intuitively, a core state represents the computation within a call to an ASP oracle, i.e., an ASP solver, while a control state controls the computation between different calls to ASP oracles, depending on over- and under-approximation. Terminal states represent the end of the computation.

Transition Rules. Transition rules are of the form:

where ruleName is the name of the rule; S =⇒ S′ represents a transition from the state S to the state S′ ; and conditions is a set of conditions for the rule to be applied. We also consider a special transition rule, Oracle, reported in Figure 1. Intuitively, it represents an oracle call to an ASP [resp., SAT] solver by providing as result a set of literals L corresponding to the output of an ASP [resp., SAT] solver, i.e., L is an answer set of a program [resp., a model of a formula], if such an answer set [resp., model] exists, and to lit(atoms(P)), otherwise. Transition rules will be organized into Return rules, dealing with the outcome of an oracle call, or the application of a given technique, depending on the status of the set of literals L returned; and Control rules, starting from a control state and directing the computation depending on the content of the over- and under-approximation.

Abstract Solver Graphs. Given a program Π, and a set of transition rules T, an abstract solver graph G(Π, T) = 〈VX,ET 〉 is such that VX is the set of all states relative to X = atoms(Π); and (S, S′ ) ∈ ET if a transition rule of the form S =⇒ S′ can be applied. Moreover, S′ ∈ VX is reachable from S ∈ VX if there is a path from S to S′ ; there is a state in VX called initial state (from which the computation starts, depending on the specific algorithm); a state reachable from the initial state is called reachable state (it represents a possible state of a computation); and no cycle is reachable if there is no reachable state which is reachable from itself.

Definition 1. Given a program Π [a CNF formula Φ] and a set of transition rules T, we say that an abstract solver graph G(Π, T) [G(Φ, T)] solves cautious reasoning [backbone computation], if (i) G(Π, T) [resp., G(Φ, T)] is finite and no cycle is reachable; and (ii) the unique terminal reachable state is Ok(cautious(Π)) [resp., Ok(backbone(Π))].

3 Abstract Solvers for Cautious Consequences

In this section, without loss of generality, we focus on the computation of cautious consequences for an ASP program.

Oracle ∅O,U,A,P =⇒ LO,U,A,P if { L ∈ AS(P ), or AS(P ) = ∅ and L = lit(atoms(P )) F ailover LO,U,over,P =⇒Cont(O,O) if { L is inconsistent Return Failunder LO,U,underS,P =⇒Cont(O,U ∪S) if { L is inconsistent, and S = ∅ or S = {a} rules Failchunk LO,U,chunkN,P =⇒Cont(O,U ∪N) if { L is inconsistent F ind LO,U,A,P =⇒Cont(O ∩L,U) if { L is consistent and L ̸= ∅ Terminal Cont(O,U) =⇒Ok(O) if { O = U Control OverApprox Cont(O,U) =⇒ ∅O,U,over,P if { O ̸= U rules UnderApprox Cont(O,U) =⇒ ∅O,U,under{a},P if { a ∈ O \ U Chunk Cont(O,U) =⇒∅O,U,chunkN,P if { N ⊆ O \ U and N ̸= ∅

In the following we assume that all abstract solvers share the same general structure. In particular, given a program Π, over-approximation O is set to atoms(Π), while the underapproximation U is empty. Note that U ⊆ cautious(Π) ⊆ O. Iteratively either under-approximation or over-approximation are applied. When U = O, the set of cautious consequences, O, has been found and the computation terminates. It means that the state Ok(O) is a reachable state. Hence, the full extent of states relative to X becomes useful. The unique terminal state is Ok(W), where W = cautious(Π).

3.1 Solving Techniques

In this section, we report three techniques, namely overapproximation, under-approximation, and chunking.

Over-approximation. We set A(atoms(Π)) = {over}, and P =Π∪ {←O}. The initial state is ∅atoms(Π),∅,over,P . We set ov = {Fail over , Find , Terminal , OverApprox } (see Figure 1), and OS(Π) = (Vatoms(Π), {Oracle} ∪ ov). Intuitively, Failover means that a call to an oracle did not find an answer set, so O is the solution. If Find is triggered, instead, we go to a control state where O is updated according to the answer set found: then, if O = U a solution is found through Terminal , otherwise the search is restarted (L = ∅) in an oracle state with OverApprox. Thus, in OS(Π), the oracle is called to find answer sets that reduce the over-approximation O in the over action, unless no answer set exists. If an answer set M is found, then M ∩ O ̸= ∅, as P = Π ∪ {← O}.

Under-approximation. Let A(atoms(Π)) = {under∅} ∪ {under{a} | a ∈ atoms(Π)}, let P = Π ∪ {← a}, if A = under{a}, and P = Π, if A = under∅. The initial state is ∅atoms(Π),∅,under∅,P . We set un = {Fail under , Find , Terminal , UnderApprox } (see Figure 1), and US(Π) = (Vatoms(Π), {Oracle} ∪ un). Intuitively, Failunder updates over- and under-approximations in case a test on the atom a failed, and leads to a control state, while UnderApprox restarts a new test if Find is not applicable. In US(Π), again, a first oracle call takes place with the action under∅, which provides first over-approximation, then calls with actions under{a}, where a is the tested atom.

Chunking. In [Janota et al., 2015] a more general technique for under-approximation that allows to test multiple literals at once is presented. Let A(atoms(Π)) = {chunkN |

N ⊆ atoms(Π)}, and P = Π ∪ {← N}, if A = chunkN. The initial state is ∅atoms(Π),∅,chunk∅,P . Let ch = {Failchunk , Find,Terminal ,Chunk} (see Figure 1) and CS(Π) = (Vatoms(Π), {Oracle} ∪ ch). In particular, Failchunk updates the over- and under-approximations accordingly in case the test on the set N fails (the ASP oracle call failed, thus all literals in N must be cautious consequences), and goes to a control state. Meanwhile, Chunk restarts a new ASP oracle call with a new (nonempty) set N such that N ⊆ O \ U in case the computation must continue.

3.2 Designing NewAbstract Solvers

The composition of techniques described so far can be applied to computing cautious consequences of a program, but actually is not included in any solver. This outlines another important feature of the abstract solvers methodology, i.e., its capability to design new solutions by combining techniques implemented in different solvers. We can mix techniques from Section 3.1 to compute either cautious consequences or backbones.

Theorem 1. Let Π be a program, and S ⊆ {ov, un, ch} s.t. S ̸= ∅. Then, (Vatoms(Π), {Oracle} ∪ ⋃x∈S x) solves cautious reasoning and backbone computation.

Core-based Methods. We now model core-based algorithms from [Janota et al., 2015] in terms of abstract solvers, in particular Algorithm 6, and apply it to the computation of cautious consequences of ASP programs. Let A(atoms(Π)) = {coreN | N ⊆ lit(atoms(Π))}, and P = Π ∪ {← l|l ∈ N}, if A = coreN. The initial state is ∅atoms(Π),∅,core atoms(Π) ,P . Moreover, given a logic program Π, we say that a set C ⊆ lit(atoms(Π)) is a core of Π, if Π ∪ {← l|l ∈ C} is incoherent. By cores(Π) we denote the set of all cores of Π. Cores have two important properties: (1) if C is a core, then all of its supersets are also cores; (2) p ∈ atoms(Π) is a cautious consequence of Π iff {¬p} is a core. To define an abstract solver graph, we start with the rule

It represents an oracle call to compute a set of literals L, which is a core of P and a subset of N, whenever P is incoherent; and an answer set of P, otherwise. Then, we introduce two intermediate control states, namely PreN and Eval .

Moreover, we introduce the following set of return rules:

and the following set of control rules:

Let in be the set of rules defined above, and let FS(Π) = (Vatoms(Π), in), which represents Algorithm 6 in [Janota et al., 2015]. In particular, PreN is reached in case of inconsistency, where N is the set of literals that may be used for the potential upcoming core action; and Eval is reached in case of consistency. From an outermost state Eval , a new core is started with NewSet , whenever there is a gap between overand under-approximation; otherwise, Final leads to the terminal state. Fail 1pre and Fail 2pre lead to the intermediate type of control state, PreN, that can either restart a core action with Continue, or continue with the Main rule.

Theorem 2. Let Π be a program. Then, the only reachable terminal states are either Cont(O,U) or Ok(O), for some O,U ⊆ atoms(Π): (i) if Ok(O) is reachable, then FS(Π) solves cautious reasoning; (ii) if Cont(O,U) is reachable, then U ⊆ cautious(Π) ⊆ O.

Chunking and core-based methods can be combined using our methodology to abstract Algorithm 7 from [Janota et al., 2015]. Such a combination will be used in the experiments.

4 Experimental Analysis

The abstract solvers reported in this paper have been used for implementing several algorithms in WASP [Alviano et al., 2015; Alviano et al., 2019], resulting in two new versions of WASP, namely WASP-CHUNK, i.e., WASP running the algorithm based on chunking, and WASP-CB, i.e., WASP running the algorithm based on cores. Both versions can limit the size of the chunk, reported in the following using the suffixes -2 and -20% representing that the size of the chunk is set to 2 and to the 20% of the number of atoms, respectively.

The performance of these versions of WASP was measured on the benchmarks considered in [Alviano et al., 2018], which includes (i) all the 193 instances from the latest ASP Competitions [Gebser et al., 2017] involving non-ground queries; (ii) 115 instances of ASP Competitions classified as easy, that is, those for which a stable model is found within 20 seconds of computation by mainstream ASP systems.

As a reference to the state of the art, we report the performance of CLASP [Gebser et al., 2012], which implements algorithm OR (i.e., over-approximation), and the best performing algorithms implemented by WASP [Alviano et al., 2014; Alviano et al., 2018], namely OR, ICT (i.e., underapproximation), OPT, and CM. We refer the reader to [Alviano et al., 2014; Alviano et al., 2018; Di Rosa et al., 2008], for a detailed description of such algorithms.

Results are shown in the cactus plots of Figure 2 and Figure 3, where for each algorithm the number of solved instances in a given time is reported, producing an aggregated view of its overall performance.

Concerning benchmark (i), we observe that WASP cannot reach the performance of CLASP on the execution of algorithm OR, and indeed CLASP solved 41 instances more than WASP-OR. However, a better performance is obtained by WASP-CB-20% and by WASP-OPT, which actually solve 13 instances more than CLASP. Moreover, we observe that even a small size of the chunk may influence the performance of the algorithms. Indeed, WASP-CB solves 13 instances more than WASP-CB-2. Finally, we observe that WASP-CHUNK20% and WASP-CHUNK-2 are not competitive to algorithms based on cores.

Concerning benchmark (ii), we observe that CLASP is the best performing solver solving 53 instances. If we focus on WASP, the best performance is obtained by WASP-CHUNK2, WASP-OR, WASP-CM, and WASP-CHUNK-20% which are able to solve 41, 41, 41, and 40 instances, respectively. Moreover, WASP-CB cannot reach the same performance on this benchmark, solving only 25 instances, whereas WASP-CB20% and WASP-CB-2 solve 37 and 39 instances, respectively.

5 Conclusion

In this paper we modeled through abstract solvers advanced techniques for solving cautious reasoning tasks in ASP. We also designed new solving procedures, and implemented them in WASP. The results of the experiments showed that our implementation is competitive to state-of-the-art approaches.