Answer Set Programming, Deductive Learning, Non-Ground Nogood Learning

1 Introduction↩︎

Conflict-Driven Nogood Learning (CDNL) is a major success factor for high-performance state-of-the-art ASP systems [1]. When a conflict occurs, new propositional nogoods are learned that prevent the same conflict from re-occurring, which improves search performance.

Previous work has failed to address the question whether learned nogoods can be generalised and re-used to speed up the solving of different instances of the same problem. This paper aims to fill this gap. We present an extension of CDNL that learns non-ground constraints. The idea is that whole parts of the search tree can be pruned when these learned constraints are added to the original program. We presume the common distinction between an unvarying problem encoding and separate inputs consisting only of facts. A problem instance is specified by the problem encoding and a set of input facts. We aim to derive non-ground constraints from the problem encoding that are valid for all possible inputs and which can be employed to speed up solving new instances. In practice, instances are often not random but share some similarities that are reflected by nogoods learned during solving. This led us to assume the existence of non-ground nogoods capable of significantly speeding up solving of practical problem instances.

CDNL and Explanation-Based Learning (EBL) [2]–[4] are our starting point. EBL is a well-known logic-based machine learning technique which learns first-order rules that are entailed by the background knowledge (in our case, the problem encoding). We combine CDNL with EBL to learn non-ground nogoods while solving prior problem instances. Since the number of generalised nogoods can be overwhelming, choosing those that will actually pay off is particularly challenging. Our basic idea is to generalise those non-ground conflicts that occur most often, i.e., we generalise propositional nogoods learned from frequently violated nogoods. The underlying assumption is that nogoods learned from frequent conflicts will also be able to prevent many conflicts.

A realistic hardware configuration example and a graph colouring problem are used for demonstration and experimentation purposes. Results show that both lazy-grounding and ground-and-solve systems benefit from our approach. By adding learned constraints to the problem encodings, up to 64% more configuration instances can be solved and graph colouring instances can be solved much faster. Learning itself requires low computational resources.

We believe that we have developed an innovative tool supporting the design of efficient answer-set programs. This view is supported by encouraging experimental results. Our main contributions can be summarized as follows:

• We present a motivating practical example and describe how some redundant constraints can be derived from a given encoding. We also sketch how non-minimal nogoods can be reduced.

• Next, we introduce a novel approach combining CDNL and EBL to automatically learn correct non-ground nogoods while solving an answer-set program. A pseudo-code algorithm is given.

• We suggest techniques to make learned nogoods use only predicates from the input program, the means to choose from the wide range of possible generalisations, and methods to quickly conduct learning under limited resources.

• Finally, we experimentally compare the effects of various learned constraints on two domains. Results demonstrate the practical benefits of our approach.

2 Preliminaries↩︎

2.1 Answer Set Programming↩︎

An answer-set program \(P\)is a finite set of non-ground rules of the form \[\label{eq:rule} h \leftarrow b_1,~\ldots,~b_m,~\mathrm{not}~b_{m+1},~\ldots,~\mathrm{not}~b_n.\tag{1}\] where \(h\) and \(b_1,\dots,b_n\) are atoms. A classical atom is an expression \(p(t_1,\dots,t_n)\) where \(p\) is an \(n\)-ary predicate and \(t_1,\dots,t_n\) are terms. A term is a variable, a constant, or a complex term involving arithmetics. A NaF-literal is either an atom \(a\) or its negation \(\mathrm{not}~a\). Negation as failure (NaF) refers to the absence of information, i.e., an atom is assumed to be false as long as it is not proven to be true. If \(l\) is a literal, then \(\overline{l}\) denotes its complement (i.e., \(\overline{\mathrm{not}~a} = a\) and \(\overline{a} = \mathrm{not}~a\)).

Given a rule \(r\), \(\mathrm{H}(r)=\{h\}\) is called the head of \(r\), and \(\mathrm{B}(r) = \{ b_1,~\ldots,~b_m,~\mathrm{not}~b_{m+1},~\ldots\), \(\mathrm{not}~b_n \}\) is called the body of \(r\). A rule \(r\) where the head is absent (\(\mathrm{H}(r) = \{\}\)), e.g., \(\leftarrow b.\), is called constraint. A rule \(r\) where the body is absent (\(\mathrm{B}(r) = \{\}\)), e.g., \(h \leftarrow.\), is called fact. Given an answer-set program \(P\), the universe of \(P\), denoted by \(U_P\), is the set of constants appearing in \(P\). By \(\mathcal{A}\) we denote the set of classical atoms constructible from predicates of \(P\) with constants in \(U_P\). The set of all literals is denoted by \(\mathcal{L}= \mathcal{A}\cup \{ \mathrm{not}~a \mid a \in \mathcal{A}\}\). The \(\mathrm{facts}\) function maps a program \(P\) to all ground atoms defined by facts in \(P\), i.e., \(\mathrm{facts}(P) = \{ \mathrm{H}(r) \mid r \in P\text{ and } \mathrm{B}(r) = \emptyset \}\).

The \(\mathrm{vars}\) function maps any structure containing variables to the set of variables it contains, e.g., for a rule \(r_1\colon \mathrm{a}(X) \leftarrow \mathrm{b}(X,Y).\), \(\mathrm{vars}(r_1) = \{ X, Y \}\). The set \(\mathcal{V}\supset \mathrm{vars}(P)\) includes all variables from a program and also variables that can additionally be used by a solver, it is usually infinite. A literal \(l\) or rule \(r\) is ground if \(\mathrm{vars}(l) = \emptyset\) or \(\mathrm{vars}(r) = \emptyset\), respectively. A program \(P\) is ground if all its rules \(r \in P\) are. A substitution \(\sigma\colon \mathcal{V}\rightarrow \mathcal{V}\cup U_P\) is a mapping from variables to variables or constants. A substitution is called grounding for a set of variables \(V \subseteq \mathcal{V}\) if for every \(v \in V\) there exists a constant \(c \in U_P\) s.t.\(\varsigma(v) = c\). The function \(\nu_A\colon \mathcal{A}\to \{ \mathbf{T}, \mathbf{M}, \mathbf{F}, \mathbf{U}\}\) for a (partial) assignment \(A\) maps an atom to the truth value the atom is currently assigned in the given assignment (\(\mathbf{M}\) stands for must-be-true and \(\mathbf{U}\) for currently unassigned).

A nogood is a set of Boolean signed literals \(\{ \mathbf{T}\; a_1, \dots, \mathbf{T}\; a_n, \dots, \mathbf{F}\; a_{n+1}, \dots, \mathbf{F}\; a_m \}\) which means that an answer set may not satisfy all the literals in the nogood. A literal in a nogood differs from a NaF-literal in a rule semantically: In a nogood, negation as failure has no role. A nogood is violated by an assignment \(A\) if \(\nu_A(a_i) \in \{ \mathbf{T}, \mathbf{M}\}\) for all \(i \in \{1, \dots, n \}\) and \(\nu_A(a_j) = \mathbf{F}\) for all \(j \in \{ n + 1, \dots, m \}\). Sometimes, we will represent nogoods not by sets but by fixed-order multisets, because we need the possibility of duplicates and of fixed positions to be able to map literals between ground and non-ground nogoods. When this is the case, \(\omega[i]\) denotes the literal at position \(i\) in nogood \(\omega\).

For ASP semantics, we refer to .

Aggregates and choice rules are common extensions to the input language of ASP [5]. Aggregate atoms are used to express arithmetic constraints on sets of atoms (e.g., cardinality constraints). A choice rule expresses that a subset of a set of atoms will be included in an answer set. This does not clash with the subset-minimality of answer sets because choice rules are translated to normal rules involving additional atoms whose predicates we call choice predicates. For simplicity, we only consider choice rules without bounds (which are the only ones currently supported by Alpha). A choice rule is of the form , but the head \(h\) is not a classical atom but a choice atom of the form \(\{ C_1; \dots; C_n \}\), where for \(n > 0\) and \(0 \leq i \leq n\) each \(C_i\) is a choice element. A choice element has the form \(a \colon l_1, \dots, l_k\), where \(a\) is a classical atom and \(l_1, \dots, l_k\) are literals for \(k \geq 0\). If the body of a choice rule is satisfied, it means that for each \(C_i\) where the literals \(l_1, \dots, l_k\) are satisfied, the atom \(a\) may or may not be true in an answer set. A choice rule \(r\) can be translated to \(2n\) rules, two for each choice element \(a \colon l_1, \dots, l_k\): \[a \leftarrow \mathrm{B}(r), l_1, \dots, l_k, \mathrm{not}~\widehat{a}.\widehat{a} \leftarrow \mathrm{B}(r), l_1, \dots, l_k, \mathrm{not}~a.\] For both aggregates and choice rules, see for details.

The goal of our method is to generate non-ground nogoods which can be re-used for solving further problem instances. More formally, let \(P^\mathrm{E}\) be an ASP problem encoding. \(\mathit{InPred}\) and \(\mathit{OutPred}\) are sets of predicate symbols with defined arities. The input for \(P^\mathrm{E}\) is specified by a set of ground facts \(\mathit{InA}\) containing only predicate symbols from \(\mathit{InPred}\). The output of a problem instance \(P^\mathrm{E}\cup \mathit{InA}\) is the set of atoms of a stable model whose predicate symbols are in \(\mathit{OutPred}\).

A conflict for an ASP program \(P\) is a constraint \(C\) s.t.\(P \models_\mathrm{S}C\) where \(\models_\mathrm{S}\) refers to the skeptical ASP semantic, i.e., \(C\) must be true in all stable models of \(P\).

Let \(\models_\mathrm{F}\) be the implication relation based on standard FOL semantic. Since every stable model of an ASP program \(P\) is also a model for \(P\) if \(P\) is interpreted as an FOL program, it follows that if \(P \models_\mathrm{F}C\) then \(P \models_\mathrm{S}C\). It is well known that every stable-model of \(P\) is also a model of \(P \cup \mathrm{comp}(P)\), i.e., the extension of \(P\) by the axioms of the Clark completion. Note that for problem instances \(P^\mathrm{E}\cup \mathit{InA}\) the Clark completion changes depending on \(\mathit{InA}\). Since we are interested in conflicts which are independent of the input, we consider only the completion of the head literals which appear in \(P^\mathrm{E}\) but not in \(\mathit{InPred}\). We denote this restricted Clark completion for a program \(P\) and input predicates \(\mathit{InPred}\) as \(\mathrm{rComp}(P, \mathit{InPred})\). It holds that \(\mathrm{rComp}(P, \mathit{InPred}) \subseteq \mathrm{comp}(P)\) and \(P^\mathrm{E}\cup \mathrm{rComp}(P^\mathrm{E}\cup \mathit{InA}, \mathit{InPred})\) is the same for all problem instances \(P^\mathrm{E}\cup \mathit{InA}\).

2.1.0.1 Proof sketch:

Since \(\mathrm{rComp}(P, \mathit{InPred})\) depends only on \(P\), it holds that if \(P^\mathrm{E}\cup \mathrm{rComp}(P, \mathit{InPred})\) \(\models_\mathrm{F}C\) then \(P^\mathrm{E}\cup \mathrm{rComp}(P, \mathit{InPred}) \cup \mathit{InA}\models_\mathrm{F}C\) where \(\mathit{InA}\) is a finite set of ground facts whose predicate symbols are in \(\mathit{InPred}\). Because every stable model of \(P^\mathrm{E}\cup \mathit{InA}\) is also a model for \(P^\mathrm{E}\cup \mathrm{rComp}(P, \mathit{InPred}) \cup \mathit{InA}\) under FOL semantic and \(C\) is true in these models it follows that \(P^\mathrm{E}\cup \mathit{InA}\models_\mathrm{S}C\).

Consequently, adding a generalized conflict \(\mathit{GC}\) to \(P^\mathrm{E}\) does not change the set of outputs of \((P^\mathrm{E}, \mathit{InPred})\) for any input.

2.2 Conflict-Driven Nogood Learning (CDNL)↩︎

Conflict-Driven Clause Learning (CDCL) [6], [7] is a SAT solving technique that extends DPLL by conflict analysis and enables the solver to learn new clauses and to do non-chronological backtracking (“backjumping”). While the original definitions of CDCL are based on clauses, i.e., disjunctions of literals, we use the notion of nogoods and speak of Conflict-Driven Nogood Learning (CDNL) [1]. The two variants are equivalent since the conjunction of classically negated nogoods can be directly transformed to an equivalent conjunction of clauses by applying De Morgan’s laws.

CDCL- and CDNL-based solvers usually characterize each atom \(a\in \mathcal{A}\) by the following properties: its truth value, its antecedent clause, and its decision level, denoted respectively by \(\nu(a) \in \{ \mathbf{T}, \mathbf{F}, \mathbf{M}, \mathbf{U}\}\), \(\alpha(a) \in 2^\mathcal{L}\cup \{ \mathrm{NIL}\}\), and \(\delta(a) \in \{ -1, 0, 1, \dots, |\mathcal{A}| \}\). The truth value of an atom is the value currently assigned to it. By the antecedent clause of an atom we mean the cause of its current truth value. The antecedent clause of an atom whose current truth value has been implied is the nogood that was unit at the time the implication happened and thus forced the atom to assume its current value. The value \(\mathrm{NIL}\) is used instead if the current truth value of an atom results from a heuristic decision. The decision level of an atom denotes the depth of the decision tree at which it has been assigned, and \(-1\) if the atom is unassigned. The decision level of a literal is the same as the literal’s atom’s decision level (\(\delta(\mathrm{not}~a) = \delta(a)\)), and the antecedent of a literal is the one of its atom (\(\alpha(\mathrm{not}~a) = \alpha(a)\)). An assignment’s decision level is the decision level of the atom most recently assigned [6], [7].

When a nogood is violated during solving (i.e., all literals in the nogood are satisfied), the conflict is analysed and a new nogood may be learned. Learning starts with the violated nogood and resolves one literal assigned at the current (most recent) decision level with its antecedent. This is repeated with the nogood resulting from resolution (the “resolvent”) as long as it is possible. Resolution stops when the only literal in the resolvent that has been assigned at the current decision level is a decision literal, i.e., its antecedent is \(\mathrm{NIL}\). The resulting nogood is then “learned”, i.e., added to the set of known nogoods, and the solver executes a backjump [6].

First UIP clause learning is a modification of this algorithm that already stops resolution when only one literal from the current decision level remains in the nogood, even if its antecedent is not \(\mathrm{NIL}\). This is correct because this literal is a unique implication point (UIP), a node in the implication graph that lies on every path from the last decision to the conflict. Each UIP could be used to learn a new nogood, but modern SAT solvers stop already at the first UIP, i.e., the one nearest to the conflict [6].

2.3 Explanation-Based Learning↩︎

Explanation-Based Learning (EBL), a.k.a.Explanation-Based Generalization (EBG), is a logic-based learning technique that, in contrast to Inductive Logic Programming (ILP), learns only general rules that are entailed by background knowledge alone (and not by background knowledge together with some new hypotheses). Therefore, in EBL nothing factually new is learned from the example. In EBL, two proof trees are created simultaneously (one for the concrete example and one with variables instead of constants). Then, new rules can be obtained from the non-ground proof tree. The operationality criterion is a restriction which predicates can be used to express the learned rules. The purpose of operationality is to use only predicates that are easy to solve. A trade-off between operationality and generality is usually an issue in EBL. By choosing adequate general rules, EBL makes a knowledge base more efficient for the kind of problems that one would reasonably anticipate [2]–[4], [8], [9].

show that EBL/EBG and Partial Evaluation (PE) are equivalent to each other in the context of logic programming. PE is a program optimisation method that reformulates an input program in an equivalent but more efficient way. employs PE (and terms it “unfolding” of rules) in lazy-grounding answer set solving to learn new rules during solving. Learning is triggered by conflicts to prevent future occurrences of similar conflicts. Learned rules are constructed from constraints that are almost violated and in which atoms have been replaced by their definitions: The single literal in the constraint’s body that is not yet satisfied must not be satisfied. Learned rules are created and used online during solving.

3 A Motivating Example↩︎

The House Configuration Problem (HCP) serves as a motivating example. It is an abstraction of real-world hardware configuration problems and defined as follows:¹ Given an association of things to the persons they belong to, a domain of cabinet IDs, and a domain of room IDs, the task is to assign things to cabinets and cabinets to rooms such that there are at most five things in each cabinet and at most four cabinets in each room, and each room only contains things that belong to the same person. The problem encoding stays the same for all problem instances. Input facts of predicates \(\mathrm{personTOthing}/2\), \(\mathrm{cabinetDomain}/1\), and \(\mathrm{roomDomain}/1\) vary from instance to instance. Each answer set specifies one valid configuration.

We are guided by the original definition of HCP by and limit ourselves to the configuration aspects of the problem, neglecting reconfiguration for presentation purposes. The complete encoding is given in [lst:house].²

{ cabinet(C) } :- cabinetDomain(C).
{ room(R) } :- roomDomain(R).
room(R1) :- roomDomain(R1), roomDomain(R2), room(R2), R1 < R2.
cabinet(C1) :- cabinetDomain(C1), cabinetDomain(C2), cabinet(C2), C1 < C2.

{ cabinetTOthing(C,T) } :- cabinetDomain(C), thing(T).
thingHasCabinet(T) :- cabinetTOthing(C,T).
:- thing(T), not thingHasCabinet(T).
:- thing(T), cabinetDomain(C1), cabinetTOthing(C1,T), cabinetDomain(C2), cabinetTOthing(C2,T), C1 < C2.
:- 6 <= #count { T : cabinetTOthing(C,T), thing(T) }, cabinet(C).

{ roomTOcabinet(R,C) } :- roomDomain(R), cabinet(C).
cabinetHasRoom(C) :- roomTOcabinet(R,C).
:- cabinet(C), not cabinetHasRoom(C). %|\label{lst:house:constraint_cabinet_without_room}%|
:- cabinet(C), roomDomain(R1), roomTOcabinet(R1,C), roomDomain(R2), roomTOcabinet(R2,C), R1 < R2.
:- 5 <= #count { C : roomTOcabinet(R,C), cabinetDomain(C) }, room(R).

personTOroom(P,R) :- personTOthing(P,T), cabinetTOthing(C,T), roomTOcabinet(R,C). %|\label{lst:house:rule_personTOroom}%|
:- personTOroom(P1,R), personTOroom(P2,R), P1 < P2. %|\label{lst:house:most_violated_constraint}%|

room(R) :- roomTOcabinet(R,C).
room(R) :- personTOroom(P,R).
cabinet(C) :- cabinetTOthing(C,T). %|\label{lst:house:rule_cabinet}%|
cabinet(C) :- roomTOcabinet(R,C).
thing(T) :- personTOthing(P,T).

added the following redundant constraint to the problem: \[\begin{align} \label{eq:redundant95constraint} \leftarrow\; & \mathrm{cabinetTOthing}(C, \mathit{T1}), \mathrm{personTOthing}(\mathit{P1}, \mathit{T1}), \nonumber \\ & \mathrm{cabinetTOthing}(C, \mathit{T2}), \mathrm{personTOthing}(\mathit{P2}, \mathit{T2}), \mathit{P1} < \mathit{P2}. \end{align}\tag{2}\]

However, this constraint can be learned automatically. Using Alpha[10] to solve the smallest instance, the nogood that is violated most often and thus leads to the highest number of conflicts is \(\{ \mathbf{T}~\mathrm{personTOroom}(\mathit{P1}, R),\) \(\mathbf{T}~\mathrm{personTOroom}(\mathit{P2}, R),\) \(\mathit{P1} < \mathit{P2} \}\) which corresponds to the constraint in [lst:house:most_violated_constraint] of [lst:house]. This constraint forbids things of two different persons \(\mathit{P1}\) and \(\mathit{P2}\) from ending up in the same room \(R\). Using our method, the following non-ground constraint can be learned at the first UIP of the implication graphs of all these conflicts: \[\begin{align} \label{eq:1uip95constraint} \leftarrow\; \mathrm{roomTOcabinet}(R, C), &\; \mathrm{cabinetTOthing}(C, \mathit{T1}), \mathrm{personTOthing}(\mathit{P1}, \mathit{T1}), \nonumber \\ &\; \mathrm{cabinetTOthing}(C, \mathit{T2}), \mathrm{personTOthing}(\mathit{P2}, \mathit{T2}), \mathit{P1} < \mathit{P2}. \end{align}\tag{3}\]

This constraint can also be easily generated by applying the rule in [lst:house:rule_personTOroom] to the constraint in [lst:house:most_violated_constraint] of [lst:house] and by factorizing different literals of predicate \(\mathrm{roomTOcabinet}/2\). The automatically learned constraint is almost identical to the human-created one . However, it includes one additional literal \(\mathrm{roomTOcabinet}(R, C)\).

Learned non-ground constraints can be minimized by employing axioms of the Clark completion [11]. The Clark completion of a logic program is computed by completing the head literals of the clauses of the program, including the completion of facts. Every stable model of a program \(P\) must also satisfy the Clark completion \(\mathrm{comp}(P)\). For example, the completion of \(\mathrm{cabinetHasRoom(\mathit{C)}}\) is \(\exists R : \mathrm{roomTOcabinet(\mathit{R,C})} \leftarrow \mathrm{cabinetHasRoom(\mathit{C)}}\). To minimize the learned nogood by resolution we substitute the existential quantifier by a Skolem function resulting in the rule \(\mathrm{roomTOcabinet(\mathit{r(C),C})} \leftarrow \mathrm{cabinetHasRoom(\mathit{C)}}\).

To minimize the conflict, we have to prove that constraint is entailed. This is achieved by showing that the program in [lst:house] becomes unsatisfiable when the negation of constraint is added to this program. Consequently, it is sufficient to show that the program becomes unsatisfiable when the facts \(\mathrm{cabinetTOthing}(\mathit{c}, \mathit{t1}),\) \(\mathrm{personTOthing}(\mathit{p1}, \mathit{t1}),\) \(\mathrm{cabinetTOthing}(\mathit{c}, \mathit{t2}),\) \(\mathrm{personTOthing}(\mathit{p2}, \mathit{t2}),\) \(\mathit{p1} < \mathit{p2}\) are added, where \(\mathit{c}\), \(\mathit{t1}\), \(\mathit{t2}\), \(\mathit{p1}\), and \(\mathit{p2}\) are Skolem constants.

Every stable model of an ASP program is also a model of the program interpreted under the standard first-order logic (FOL) semantic. Consequently, if a program is unsatisfiable under FOL semantics, it is also unsatisfiable skeptical ASP semantics. From \(\mathrm{cabinetTOthing}(\mathit{c}, \mathit{t1})\) and the rule in [lst:house:rule_cabinet] we can deduce \(\mathrm{cabinet(\mathit{c})}\). From the constraint in [lst:house:constraint_cabinet_without_room] of [lst:house], we can deduce \(\mathrm{cabinetHasRoom(\mathit{c)}}\) interpreting the sentences in [lst:house] as FOL clauses. Exploiting the rule provided by the Clark completion of \(\mathrm{cabinetHasRoom(\mathit{C)}}\) as shown above, we can deduce \(\mathrm{roomTOcabinet(\mathit{r(c),c})}\). Finally, using all the deduced and given facts, constraint is violated. Since this constraint is implied by the program and we have shown that it is violated if the negation of constraint is added, constraint is implied. As a result, we have shown that indeed the learned non-ground constraint can be reduced by dropping \(\mathrm{roomTOcabinet}(R, C)\).

4 Conflict Generalisation↩︎

We propose to combine CDNL with EBL to facilitate the learning of general (i.e., non-ground) constraints. This can be done online (during solving), or offline. In the latter case, learned constraints are computed and recorded. A selection can then be made, for example either automatically based on metrics or by a human, and useful constraints can be added to the original program to improve solving performance in the future. In this section, we describe how offline conflict generalisation can be implemented in an ASP solver and exemplify this by means of a prototypical implementation in the lazy-grounding system Alpha[10]. The constraints learned by this method can be used by any ASP system, not only by the system employed for the learning task, because they are stated in pure ASP-Core-2 [5], using only predicates from the original program.

Parallelly conducting CDNL on the ground level and on the non-ground level when a conflict is encountered is the basic idea of combining CDNL with EBL to generalise learned nogoods. A key requirement for this is that for each ground nogood, a corresponding non-ground nogood is known that can be used for non-ground resolution. We will now describe how non-ground nogoods are maintained in Alpha. This can be implemented similarly in any other ASP system.

In Alpha, there are five types of nogoods:

• static nogoods that represent ground rules and are generated by the grounder;

• support nogoods that encode the situation that the body-representing atom of a rule must be true if the head of the rule is true;

• learned nogoods originating from CDNL;

• justification nogoods learned by justification analysis [12];

• and internal nogoods containing solver-internal atoms.

Non-ground nogoods for static and support nogoods are produced by the grounder as described in the following paragraphs. Non-ground nogoods for learned nogoods are produced by the conflict generalisation procedure that is the main contribution of this paper. Non-ground nogoods are not maintained for justification nogoods (because these nogoods depend too heavily on the specific problem instance) and for internal nogoods (because these are irrelevant to CDNL).

We now describe how non-ground nogoods for static and support nogoods are produced by the grounder. Let \(r\) be a rule of the form and \(\sigma\) be a substitution that is grounding for \(\mathrm{vars}(r)\). The grounder produces a ground rule \(r\sigma\) from \(r\) if no fact and no fixed-interpretation literal makes the body of \(r\sigma\) false. Because of this, facts and fixed-interpretation literals are actually omitted from the ground rule produced by the grounder.³ For simplicity of presentation, however, we assume here that the grounder does not eliminate any atoms known to be true from generated nogoods. This ensures a one-to-one relationship between literals in ground nogoods and literals in non-ground nogoods. Additional effort is necessary to map from ground literals to non-ground literals if true literals are eliminated from ground nogoods, but this is purely a matter of implementation. Not eliminating any literals from non-ground nogoods, however, is crucial.

A body-representing atom \(\beta(r,\sigma)\) is created for every ground rule \(r\sigma\). Similarly, \(\beta(r,\mathrm{vars}(r))\) is a fictitious atom representing the body of a non-ground rule \(r\). The latter atom contains a term that lists all the variables that occur in the rule \(r\), so that they can affect unification when a body-representing literal is used for resolution. This will become crucial in 4.1.

The following static nogoods are produced by the grounder from a rule \(r\) and a grounding substitution \(\sigma\) [13]: \[\begin{align} \tag{4} &\{ \mathbf{F}~\beta(r,\sigma), \mathbf{T}~b_1 \sigma, \dots, \mathbf{T}~b_m \sigma, \mathbf{F}~b_{m+1} \sigma, \dots, \mathbf{F}~b_n \sigma\}\\ \tag{5} &\{ \mathbf{F}~h\sigma, \mathbf{T}~\beta(r,\sigma)\}\\ \tag{6} &\{ \mathbf{T}~\beta(r,\sigma), \mathbf{F}~b_1 \sigma\}, \dots, \{ \mathbf{T}~\beta(r,\sigma), \mathbf{F}~b_m \sigma\}\\ \tag{7} &\{ \mathbf{T}~\beta(r,\sigma), \mathbf{T}~b_{m+1} \sigma\}, \dots, \{ \mathbf{T}~\beta(r,\sigma), \mathbf{T}~b_n \sigma\}\\ \tag{8} &\{ \mathbf{T}~h\sigma, \mathbf{F}~\beta(r,\sigma)\} \end{align}\] Nogood is a so-called support nogood and is produced by Alphacurrently only when an atom occurs in the head of just a single rule. If \(r\) is a constraint, only one nogood is created, which consists of the whole body of \(r\sigma\).

As a prerequisite for conflict generalisation, a solver must associate each ground nogood with a non-ground nogood. This non-ground nogood is obtained from a non-ground rule the same way as a ground nogood is obtained from a ground rule. This means that the non-ground nogoods are exactly the same ones as given above, except the substitution \(\sigma\) does not appear anywhere: The atom \(\beta(r,\sigma)\) becomes \(\beta(r,\mathrm{vars}(r))\), and any other ground atom \(a\sigma\) becomes just \(a\).

4.1 Non-ground CDNL↩︎

In this section, we describe how we extend CDNL to learn non-ground nogoods. The non-ground nogoods learned that way can then just be used as constraints and be added to the original program. When learning only constraints and no other kinds of rules, \(\mathbf{F}\) in nogoods can just be replaced by negation as failure.

Our main conflict generalisation algorithm is shown in 1. We represent nogoods by fixed-order multisets to be able to map between literals in ground and non-ground nogoods. The algorithm takes as input a violated ground nogood \(\omega\) and the current assignment \(A\). If the conflict occurred at decision level 0, UNSAT is returned in [alg:conflict-generalisation:AnalyzeConflict:return-UNSAT], otherwise two lists of learned nogoods are returned in [alg:conflict-generalisation:AnalyzeConflict:return-lists]. The first list contains ground nogoods and the second list contains non-ground nogoods. Each element of both lists corresponds to one UIP and both lists are ordered by distance from the conflict, i.e., the first element of both lists is a nogood learned at the first UIP and the last element of both lists is a nogood learned at the last UIP.

As long as the current nogood contains a literal from the current decision level⁴ with non-\(\mathrm{NIL}\)antecedent ([alg:conflict-generalisation:AnalyzeConflict:while]), it is resolved with the antecedent of such a literal to produce a new current nogood \(\omega\) (the resolvent, [alg:conflict-generalisation:AnalyzeConflict:Resolve]). If \(\omega\) contains exactly one literal on the current decision level ([alg:conflict-generalisation:AnalyzeConflict:UIP]), we have found a UIP and remember the current nogood (both ground and non-ground).

Resolution of ground nogoods is straightforward and well-known ([alg:resolution:ground-resolution]): The resolvent is the union of two input nogoods (\(\omega\) and the antecedent of \(l\), \(\alpha(l)\)), minus \(l\) that occurs in the first input nogood and its complement \(\bar{l}\) that occurs in the second input nogood.

Following the resolution on the non-ground level is more complex, however, and several special cases have to be considered. First, the non-ground nogood corresponding to \(\alpha(l)\) is identified and standardised apart from the current nogood (i.e., variables are renamed to avoid overlaps; [alg:resolution:identify-ngng]).⁵ Then, two steps of unification are necessary: First, in [alg:resolution:unify-resolution-literal], the two complementary resolution literals are unified s.t.variable occurrences are correctly updated in the resolvent. Then, an additional step is necessary only on the non-ground level: If the two ground input nogoods share some literals, duplicates are just removed during resolution, because a nogood is a set of literals. On the non-ground level, however, for each ground literal that occurs in both input nogoods, the corresponding non-ground literals must be unified before one of them can be removed ([alg:resolution:unify-duplicate-literals]). This is a restricted form of factoring that is guided by ground resolution. Note that in the context of CDNL, it is not possible for two input nogoods to contain complementary literals apart from the resolution literal, because all antecedents must be unit to entail a literal. Finally, after applying the computed unifier to both non-ground nogoods, the resolution step is the same as on the ground level ([alg:resolution:nonground-resolution]).

The connection between our suggestion of non-ground CDNL and EBL becomes apparent when viewing the violated nogood as the training instance. The implication graph utilised by CDNL constitutes a proof that the nogood is violated by giving a derivation for each literal in the nogood. Each arc in the implication graph that originates from unit propagation can be seen as a definite Horn clause that derives the literal assigned by the propagation step. Operationality in our setting is specified by demanding that nogoods are only learned at UIPs. The set of predicates allowed in learned nogoods is not restricted, because in ASP there are no predicates that are “easier to solve” than others. In lazy grounding, rules are even grounded only when (part of) their body is already satisfied [14], which alleviates the overhead of additional rules. Currently, facts from the ASP program are not regarded by our approach because they are not included in nogoods generated by state-of-the-art answer-set solvers. This ensures that learned constraints depend only on the rules from the problem encoding.

1 is correct because it derives constraints that are implied when the input program \(P\) is interpreted as an FOL program, and because such constraints are also true in all stable models of \(P\), as has been discussed in 2.1.

4.1.0.1 Replacing internal atoms in learned constraints.

Learned constraints may contain literals of solver-internal predicates. Literals of two kinds of such predicates, namely body-representing and choice predicates, can easily be replaced by equivalent (sets of) literals of predicates from the problem encoding. Only then can resulting constraints be correctly added to the input program.

A body-representing atom such as \(\beta(r,\mathrm{vars}(r))\) represents the body of non-ground rule \(r\). If a nogood contains a positive literal of such an atom, by definition this literal can just be replaced by the body of \(r\). This is equivalent to resolving with nogood above. If the head of \(r\) is the head of no other rule, \(\beta(r,\mathrm{vars}(r))\) can also be replaced by \(\mathrm{H}(r)\) by resolving with the support nogood . If a nogood contains a negative literal of a body-representing atom, it can be replaced by the negated head of \(r\) (which is equivalent to resolving with nogood above) or by an arbitrary negated body literal of \(r\) (equivalent to resolving with any of the nogoods in or ).

For choice rules, internal literals of a different kind are created, as has been described in 2.1. Because of this, atoms \(\widehat{a}\) may occur in learned nogoods. Due to the way choice rules are translated to normal rules, the literal \(\mathbf{F}~\widehat{a}\) is equivalent to \(\mathbf{T}~a\) and can simply be replaced. Similarly, \(\mathbf{T}~\widehat{a}\) is equivalent to \(\mathbf{F}~a\).

4.1.0.2 Choosing effective constraints.

Since the number of learnt constraints might be overwhelming, strategies to choose effective ones are of vital importance. Our approach is simple but effective: We count how many conflicts could be avoided if the additional non-ground constraints were already included in the input program.

Each ground nogood that is violated during a run of CDNL belongs to a class of nogoods that share the same non-ground nogood. When running 1 upon such a nogood violation, the lists of learned non-ground nogoods are associated with this class. When conflict generalisation terminates, the learned nogoods are printed together with the number of violations of their associated non-ground nogood, s.t.a (human) user can then select the most useful constraints. Since learned constraints can of course be equivalent to each other when variables are renamed, only one unique representation of each nogood is remembered. For example, the class of ground nogoods violated most often while Alphasolves the HCP (3) is identified by the non-ground nogood \(\{ \mathbf{T}~\mathrm{personTOroom}(\mathit{P1}, R),\) \(\mathbf{T}~\mathrm{personTOroom}(\mathit{P2}, R),\) \(\mathit{P1} < \mathit{P2} \}\).

Every UIP provides the opportunity to learn a constraint.We focused on the first and last UIP in our experiments, because ground CDNL very successfully learns only from the first UIP, and because we expect constraints from the last UIP also to be useful since they contain the decision from the current decision level. Investigating the usefulness of other UIPs, and finding other quality criteria to discriminate among learned constraints, belong to future work.

If no limit is imposed on the conflict generalisation algorithm, it runs until the problem is solved (one or more answer sets are found, or unsatisfiability is proven). To increase efficiency, resource consumption may be limited by stopping after a certain time or number of conflicts and then collecting results as if the problem had been solved. In our experiments, conflict generalisation was very effective even if resources were heavily limited, because the class of nogoods violated most often emerged at the very beginning of the solving process.

4.2 Continuation of the motivating example↩︎

The House Configuration Problem (HCP) was presented as a motivating example in 3. We have already presented the constraint that can automatically be learned at the first UIP.

When continuing along the implication graph until the last UIP, two different non-ground nogoods can be learned: namely, \(\Omega_\mathrm{min} \cup \{ \beta(r_\mathrm{r2c},\mathrm{vars}(r_\mathrm{r2c})) \}\) and \(\Omega_\mathrm{min} \cup \mathrm{B}(r_\mathrm{r2c})\), where: \[\begin{align} \Omega_\mathrm{min} = &~\{ \mathbf{T}~\mathrm{cabinetTOthing}(C, \mathit{T1}), \mathbf{T}~\mathrm{personTOthing}(\mathit{P1}, \mathit{T1}), \\ &~~~ \mathbf{T}~\mathrm{cabinetTOthing}(C, \mathit{T2}), \mathbf{T}~\mathrm{personTOthing}(\mathit{P2}, \mathit{T2}), \mathit{P1} < \mathit{P2} \} \\ r_\mathrm{r2c}\colon & \mathrm{roomTOcabinet}(R,C) \leftarrow \mathrm{roomDomain}(R), \mathrm{cabinet}(C), \mathrm{not}~\widehat{\mathrm{roomTOcabinet}(R,C)}. \end{align}\] In both nogoods, internal atoms can be replaced by ordinary atoms as described above to yield the following unique non-ground nogood⁶ learned at the last UIP: \[\begin{align} \label{eq:luip95constraint} \leftarrow\; & \mathrm{roomTOcabinet}(R, C), \underline{\smash{\mathrm{roomDomain}(R)}}, \underline{\smash{\mathrm{cabinet}(C)}}, \nonumber \\ & \mathrm{cabinetTOthing}(C, \mathit{T1}), \mathrm{personTOthing}(\mathit{P1}, \mathit{T1}), \nonumber \\ & \mathrm{cabinetTOthing}(C, \mathit{T2}), \mathrm{personTOthing}(\mathit{P2}, \mathit{T2}), \mathit{P1} < \mathit{P2}. \end{align}\tag{9}\] This nogood contains additional literals of domain predicates (underlined for emphasis), which is the only difference to the nogood learned at the first UIP.

Reduction of the non-minimal learned nogood as described in 3 has not yet been implemented in our system. An implementation based on first-order theorem proving is conceivable, in which undecidability could be avoided by imposing a bound on the number of constants, e.g., a maximal number of entities in a configuration.

5 Experimental Results↩︎

We conducted a set of experiments on encodings of the House Reconfiguration Problem (HRP) and on a Graph Colouring problem ([lst:3cc]) to demonstrate the feasibility of our approach. HRP extends HCP from 3, which has disregarded reconfiguration. All encodings and instances used for our experiments are available on our website.⁷ The HRP encoding was closely based on the encoding by , except that the redundant constraint has been removed, as described in 3, and due to syntactic restrictions of Alphasome aggregates had to be rewritten and optimization statements were not used at all. Note that for reasons of a fair comparison, all solvers used the same encodings in our experiments, even though solvers supporting aggregates could have profited from a more sophisticated encoding.

Graph Colouring problems are an abstraction to which many real-world problems can be mapped. We have designed 100 satisfiable and 100 unsatisfiable graph instances (“3CC” for “3-colourable chains”) containing repeated patterns that force some pairs of nodes to have the same colour. On 3CC, our approach was able to learn constraints that represent this pattern. This was only possible by adapting procedure FindNextLiteralForResolution in 1 to also use literals from the next-lower decision level (\(\delta(l) \geq \delta(A)-1\)) for resolution. The question how many decision levels to consider is an interesting topic for future work. From the constraints learned from the conflicts occurring most often, one from the first UIP and one from the last UIP were chosen manually for the experiments. Since these constraints represent only the conflict for one specific combination of the three colours, they were multiplied manually to cover all possible combinations.⁸ The constraints learned at the first UIP were then reduced manually, similarly as has been described in 3, yielding the following final constraint for red (and two more constraints for the other colours): \[\begin{align} \label{eq:3cc95reduced95constraints} \leftarrow\; & \mathrm{red}(\mathit{N12}), \mathrm{not}~\mathrm{red}(\mathit{N22}), \nonumber \\ & \mathrm{link}(\mathit{N12}, \mathit{N11}), \mathrm{link}(\mathit{N12}, \mathit{N21}), \mathrm{link}(\mathit{N11}, \mathit{N21}), \mathrm{link}(\mathit{N11}, \mathit{N22}), \mathrm{link}(\mathit{N21}, \mathit{N22}). \end{align}\tag{10}\]

blue(N) :- node(N), not red(N), not green(N).
red(N) :- node(N), not blue(N), not green(N).
green(N) :- node(N), not red(N), not blue(N).
:- link(N1,N2), blue(N1), blue(N2).
:- link(N1,N2), red(N1), red(N2).
:- link(N1,N2), green(N1), green(N2).

The ASP solvers Alpha⁹ v0.5.0 [10], dlv 2.0 [15], and clingo 5.4.0 [16] were used. Alphawas configured to ground rules strictly lazily and constraints permissively, as recommended by . The JVM was called with parameters -Xms1G -Xmx32G. For each problem instance, solvers searched for 10 answer sets.¹⁰

Experiments were run on machines each with two Intel^® Xeon^® CPU E5-2650 v4 @ 2.20GHz with 12 cores each, 252 GB of memory, and Ubuntu 16.04.1 LTS Linux. Benchmarks were scheduled with ABC Benchmarking System [17] and HTCondor.¹¹ pyrunlim¹² was used to measure time and memory consumption and to limit time consumption to 10 minutes per instance, memory to 40 GiB and swapping to 0. Care was taken to avoid interference between CPUs, e.g., by not running different benchmarks concurrently on the same machine.

To compare solving performance using encodings with and without learned constraints, cactus plots (2 [fig:cactus95hrp95clingo] [fig:cactus95hrp95dlv2] [fig:cactus953cc95kco95permissive] [fig:cactus953cc95clingo] [fig:cactus953cc95dlv2]) have been created in the usual way. The x axis gives the number of instances solved within real (i.e., wall-clock) time which is given on the y axis. Time is accumulated over all solved instances. Since we are investigating the effects of constraints on each solver and not comparing solvers against each other, maximum axis values vary between solvers. One curve has been drawn for each encoding: the original encoding, one encoding each with the additional constraint(s) learned automatically at the first/last UIP (/ for HRP), and one encoding in which only the reduced constraint(s) ( for HRP, for 3CC) are added to the original encoding.

Learned constraints improved solving performance in many cases. For HRP, Alphabenefited especially from the reduced constraint, but also from the constraint learned automatically at the first UIP. dlv2 profited most from the first-UIP constraint, but the reduced one was not far behind. The last-UIP constraint affected dlv2’s performance negatively, however. clingo profited only from the reduced constraint, while automatically learned constraints caused overall solving time to increase. Detailed analysis of grounding and solving times as reported by clingo (1) shows that this was due to additional grounding effort induced by learned constraints. With automatically learned constraints, more than half of the instances could not be solved within 10 minutes, therefore no median times (second quartiles) can be shown. In almost all time-out cases, clingo did not manage to finish grounding and start solving. For 3CC, all solvers perform best with the reduced constraints, while the 1st-UIP constraints also improve performance.

Learning itself is cheap: On the first author’s computer, the relevant HRP constraints are learned using the easiest instance in less than 6 seconds if search is stopped after 50 conflicts and in less than 14 seconds if search is carried out until the first answer set is found (our implementation has not yet been tuned for optimal performance). Performance for 3CC is similar. Computational complexity has not yet been analysed and could be addressed in future work.

The results show that our approach is able to improve ASP solving using both lazy-grounding and ground-and-solve systems. While effects vary between types of learned constraints and solver implementations, every system under investigation has profited from at least one learned constraint in both domains.

6 Conclusions↩︎

We have proposed an extension of CDNL that, while solving one problem instance, learns non-ground nogoods that can be used to speed up the solving of other problem instances. As far as we know, this is the first attempt to generalise and re-use knowledge learned during ASP solving. Experimental results showed compelling benefits of our approach: Both ground-and-solve systems and lazy-grounding systems performed significantly better on instances of a practical configuration problem and a graph colouring problem when using constraints learned by our method, solving more instances and/or solving the problems faster.

So far, we have been experimenting with encodings for two problem domains: a graph colouring problem, and an important part of many configuration domains (those where systems are composed hierarchically). However, it seems natural to assume that many domains feature redundant constraints that may not be obvious to a human modeller. We therefore see our approach mainly as a tool to support the design of efficient answer-set programs.

It remains to be clarified whether our approach could improve encodings used by the ASP competitions [18], which generally are already heavily optimised, or whether it would prove more useful when applied to encodings devised by inexperienced modellers.

6.0.0.1 Acknowledgments.

This work has been conducted in the scope of the research project DynaCon (FFG-PNr.:), which is funded by the Austrian Federal Ministry of Transport, Innovation and Technology (BMVIT) under the program “ICT of the Future” between 2017 and 2020,¹³ and in the scope of the research project Productive4.0, which is funded by EU-ECSEL under grant agreement no737459.

References↩︎