Encoding Choice Logics in ASP? Michael Bernreiter, Jan Maly, and Stefan Woltran DBAI, TU Wien, Austria, {mbernrei,jmaly,woltran}@dbai.tuwien.ac.at Abstract. Choice Logics are a tool to express and reason about pref- erences. A choice logic extends classical propositional logic by adding non-classical binary connectives which express a certain form of ordering over interpretations that satisfy the connective; examples in the literature are Qualitative Choice Logic (QCL) which introduces the concept of or- dered disjunction and Conjunctive Choice Logic (CCL) where an ordered variant of conjunction has been proposed. These logics have in common that interpretations ascribe a natural number, called satisfaction degree, to formulas; the lower this satisfaction degree, the more preferable the interpretation. In this paper, we present a general framework to capture several such logics and show how choice logics defined in our framework can be encoded using Answer Set Programming. (ASP). Keywords: Preferences, Choice Logics, Answer Set Programming 1 Introduction Preferences are of interest in many areas of research such as economics, psychol- ogy, philosophy, but also computer science. Artificial intelligence, databases, and other fields are often concerned with analyzing ”human choice behavior” [13]. One formal framework in which preferences can be expressed is Qualitative Choice Logic (QCL) [4]. QCL extends classical propositional logic by a binary #» connective ×, called ordered disjunction. Let F and G be formulas. Then the #» intuitive meaning of F ×G is that if possible, F should be satisfied. If this is not possible, then it is still acceptable, but less preferable, to satisfy only G. Satisfy- ing neither F or G is not acceptable. More specifically, the satisfaction relation of QCL ascribes a natural number (called satisfaction degree) to a formula, given some interpretation. We prefer those interpretations that result in the smallest satisfaction degree for a formula. A further logic based on ordered connectives, called Conjunctive Choice Logic (CCL), has later been introduced in [2]. CCL #» replaces the ordered disjunction of QCL by another binary connective , called #» ordered conjunction. The intuitive meaning of F G is that if possible, F and G should be satisfied. If this is not possible, then at least F should be satisfied. ? This work was funded by the Austrian Science Fund (FWF) under grant number Y698 and P31890. Copyright © 2020 for this paper by its authors. Use permitted under Creative Com- mons License Attribution 4.0 International (CC BY 4.0). 2 Michael Bernreiter et al. In this paper, we will generalize QCL and CCL by defining a framework for logics in which preferences can be expressed by extending propositional logic with additional non-classical connectives. A logic of this framework will be referred to as a choice logic (CL). For instance, our framework allows to combine QCL and CCL into a new logic in a straightforward way. We provide some preliminary results for general CLs in terms of equivalence. The main contribution of the paper, however, is to encode choice logics from our framework by means of Answer Set Programming (ASP). While there is a significant amount of literature on adding preferences to core ASP (see, e.g. [6, 5, 9]), only a few papers encoded fundamental preference mechanisms in (standard) ASP. Work in this direction includes, for instance, en- codings for the voting domain [7, 12], and a translation from ASP with Resources (RASP) to plain ASP [8]. In fact, we opted here also for encodings in standard ASP, since our general framework of choice logics allows for connectives that can be quite different to concrete ASP add-ons. 2 Introducing QCL and CCL We briefly summarize the definitions of the two choice logics that motivate our general framework, namely QCL, introduced by Brewka et al. [4], and CCL, introduced by Boudjelida and Benferhat [2]. In their original papers, both logics use slightly different notation for the same concepts. For the sake of uniformity, we stick to one notation that is a mixture of the notation of both papers. #» QCL is an extension of propositional logic that adds a new connective ×. Definition 1. The set of QCL-formulas FQCL is defined inductively as follows: 1. x ∈ FQCL , where x is a propositional variable; 2. if F ∈ FQCL , then (¬F ) ∈ FQCL ; #» 3. if F, G ∈ FQCL , then (F ◦ G) ∈ FQCL for ◦ ∈ {∧, ∨, ×}. Observe that every classical propositional formula is also a QCL-formula. The semantics of QCL is based on satisfaction degrees. Interpretations ascribe a natural number to formulas. The lower this number (satisfaction degree) is, the more preferable this interpretation is for that particular formula. Before we can define the inference relation for satisfaction degrees, we need the concept of optionality, which expresses the number of satisfaction degrees that a formula can possibly have. Definition 2. Let x be a propositional variable, and let F and G be QCL for- mulas. Then the optionality of a QCL formula is defined as follows: 1. opt(F ) = 1 if either F = x or F = ¬G; 2. opt(F ◦ G) = max(opt(F ), opt(G)) for ◦ ∈ {∧, ∨}; #» 3. opt(F ×G) = opt(F ) + opt(G). Now we can define the notion of satisfaction degree.1 1 Alternative satisfaction relations for QCL formulas have been proposed in [1]. These #» do not alter the semantics of ×, but rather change how the classical connectives (¬, ∧, and ∨) operate with respect to the satisfaction degree. Encoding Choice Logics in ASP 3 Definition 3. Let I be an interpretation, x be a propositional variable, and F and G be QCL formulas. Then the satisfaction degree k ∈ N ∪ {∞} of a QCL formula under I is defined as follows: 1. I |∼QCL k x with k = 1 if x ∈ I and k = ∞ otherwise; QCL 2. I |∼k ¬F with k = 1 if I |∼QCL ∞ F and k = ∞ otherwise; QCL 3. I |∼k F ∧ G with k = max(m, n) for I |∼QCLm F and I |∼QCL n G: QCL QCL QCL 4. I |∼k F ∨ G with ( k = min(m, n) for I |∼m F and I |∼ n G; QCL #» I |∼QCL k F for k < ∞ or 5. I |∼k F ×G iff I |∼QCL ∞ F, I |∼QCL m G, and k = m + opt(F ). We observe that the satisfaction degree of a formula under a given inter- pretation is unique. If there is a k ∈ N such that I |∼QCL k F , we say that I satisfies F with a degree of k. Otherwise, we say that F is not satisfied under #» I. As an example, let us consider the formula F = ((x ∧ y)×x). Intuitively, F expresses that it is preferable to satisfy both x and y. If this is not possible, then it is still acceptable to satisfy only x. Formally, this means {x, y} |∼QCL1 F and {x} |∼QCL 2 F , but ∅ |∼QCL ∞ F . Since the purpose of QCL is to express preference, we are often interested in those models that satisfy a formula with minimal satisfaction degree, i.e. we are interested in the preferred models of a formula. Definition 4. Let I be an interpretation and let F be a QCL-formula. Then I is a preferred model of F if I |∼QCL k F with k 6= ∞ and for all other interpretations J we have J |∼QCL m F with k ≤ m. Now let us consider CCL. Syntactically, QCL and CCL are equivalent, but we #» #» write instead of × for the choice connective. The semantics of CCL only differs in the definition of the satisfaction degree of the choice connective. That means, the optionality of a formula in CCL is defined the same way as in QCL and the inference relation for the classical connectives remains unchanged between CCL and QCL. The semantics of the choice connective is as follows: Definition 5. Let I be an interpretation and let F and G be CCL formulas. #» Then the satisfaction degree of the CCL formula F G under I is k where  m  if I |∼CCL 1 F and I |∼CCL m G CCL k = m + opt(G) if I |∼m F , m 6= 1, and m 6= ∞  ∞ otherwise  #» The intuitive meaning of a formula A B is that A and B is the most preferred outcome but, if that is not possible, only A is also acceptable but less preferred. 3 A Framework for Choice Logics QCL and CCL are two logics that only differ in the definition of the semantics of the choice operator. Furthermore, the choice operators considered in QCL and 4 Michael Bernreiter et al. CCL are not the only sensible choice operators. Consider, for example a choice connective that expresses that one prefers A to B but satisfying both or neither is not acceptable. This connective can express preferences between options that can not be chosen together, for example events at the same time slot. Therefore, we propose a general framework for choice logics (CL) that captures QCL and CCL and can also express other interesting choice connectives. Syntactically, our framework closely resembles QCL and CCL, with the main difference that we allow, in general, arbitrary many choice connectives. Definition 6. The set of choice connectives CL of a choice logic L is a finite set of binary connectives such that CL ∩ {¬, ∧, ∨} = ∅. The set FL of formulas of a choice logic L is defined inductively as follows: 1. x ∈ FL , where x is a propositional variable; 2. if F ∈ FL , then (¬F ) ∈ FL ; 3. if F, G ∈ FL , then (F ◦ G) ∈ FL for ◦ ∈ {∧, ∨} ∪ CL . #» For CQCL = {×} we retrieve the syntax of QCL and for CL = {} we retrieve the syntax of propositional logic. For any choice logic, the semantics of the classical connectives for optionality and satisfaction degree are the same as for QCL and CCL. The semantics of a choice connective depends on the intended meaning of the connective. However, we can give reasonable restrictions for the semantics of choice connectives, for example the following upper bound for the optionality of a choice connective: optL (F ◦ G) ≤ (optL (F ) + 1) · (optL (G) + 1). The idea is that F can have at most optL (F ) many finite satisfaction degrees, plus the infinite degree ∞, i.e. there are at most optL (F ) + 1 degrees for F . Analogously for G. Thus, there are (optL (F ) + 1) · (optL (G) + 1) possible com- binations for how satisfaction degrees can be ascribed to (F ◦ G). In addition to giving an upper bound, we can also give the following lower bound: optL (F ◦ G) ≥ max(optL (F ), optL (G)). A choice connective should introduce new ways to distinguish between interpre- tations, or at least not give less options for doing so. Lastly, for any reasonable choice connectives, the optionality of (F ◦G) should only depend on the optionality of F and G. No other factors, such as the structure of F or G, should have an influence. Definition 7. Let x be a propositional variable, and let F and G be formulas of a choice logic L. Then the optionality of an L-formula is given by the function optL : FL → N such that 1. optL (F ) = 1 if either F = x or F = ¬G; 2. optL (F ◦ G) = max(optL (F ), optL (G)) for ◦ ∈ {∧, ∨}; Encoding Choice Logics in ASP 5 3. for every ◦ ∈ CL there is a function f : N2 → N such that optL (F ◦ G) = f (optL (F ), optL (G)) with max(optL (F ), optL (G)) ≤ optL (F ◦ G) ≤ (optL (F ) + 1) · (optL (G) + 1). We are now ready to define the notion of satisfaction degrees for an arbitrary choice logic. For the semantics of choice connectives, we impose two crucial re- strictions. Firstly, the satisfaction degree of a formula under any given interpre- tation should never be bigger than its optionality, unless the degree is ∞. After all, the purpose of optionality is to assert the number of satisfaction degrees that a formula can possibly have. Secondly, the satisfaction degree of a formula F ◦ G under any given interpretation should only depend on the optionalities and satisfaction degrees of F and G. The structure of the formula or interpre- tation should have no impact on the satisfaction degree. For example, whether an interpretation assigns an even or uneven number of propositional variables to true should have no influence on the satisfaction degree. Therefore, the satisfaction degrees in a choice logic are defined as follows. To simplify notation, we write degL (I, F ) = k if I |∼L k F holds. Definition 8. Let L be a choice logic, I be an interpretation, x be a proposi- tional variable, and F and G be L-formulas. Then the satisfaction degree of an L-formula under I is defined as 1. I |∼Lk x with k = 1 if x ∈ I and k = ∞ otherwise: 2. I |∼L L k ¬F with k = 1 if I |∼∞ F and k = ∞ otherwise; 3. I |∼k F ∧ G with k = max(m, n) if I |∼L L L m F and I |∼n G; L L L 4. I |∼k F ∨ G with k = min(m, n) if I |∼m F and I |∼n G; 5. for every ◦ ∈ CL there is a function g : (N ∪ {∞})4 → (N ∪ {∞}) such that degL (I, F ◦ G) = g(optL (F ), optL (G), degL (I, F ), degL (I, G)) with degL (I, F ◦ G) ≤ optL (F ◦ G) or degL (I, F ◦ G) = ∞. As before, we say that I satisfies F with a degree of k. If I satisfies F with a finite degree, then I is called a model of F . Furthermore, we can define preferred models analogously to QCL. Definition 9. Let I be an interpretation and let F be a formula of some choice logic L. Then I is a preferred model of F , written as I ∈ M odL (F ), if degL (I, F ) 6= ∞ and for all other interpretations J we have degL (I, F ) ≤ degL (J , F ). 3.1 Examples for Choice Logics A CL is characterized by its choice connectives and by the meaning ascribed to said connectives. We have already seen the definition of QCL and CCL and it is evident that they can be expressed within our framework. As discussed #» above, we would like a connective ⊕ that expresses the following situation: It is 6 Michael Bernreiter et al. preferable to satisfy F ; if this is not possible, then G should be satisfied, but it is not acceptable to satisfy both F and G. This connective is based on exclusive #» disjunction (XOR), similar to how × is based on regular disjunction. We name this connective ordered exclusive disjunction, and call the corresponding choice logic Exclusive Disjunctive Choice Logic (XCL). #» Definition 10. XCL is the choice logic such that CXCL = {⊕}, #» optXCL (F ⊕G) = optXCL (F ) + optXCL (G), and     degXCL (I, F ) if degXCL (I, F ) < ∞ and degXCL (I, G) = ∞   #»   degXCL (I, F ⊕G) = degXCL (I, G) + optXCL (F ) if degXCL (I, F ) = ∞  and degXCL (I, G) < ∞      ∞ otherwise #» We note that this connective can also be expressed in QCL as ((F ×G) ∧ ¬(F ∧ G)). But if this type of preference has to be expressed often in a given system, then a dedicated choice connective can simplify specifications. Other, simple, choice connectives can not directly be expressed in QCL, for example because they ignore the optionality of a formula. Definition 11. L1 is the choice logic such that CL1 = {◦}, optL1 (F ◦ G) = optL1 (F ) + 1, and  degL1 (I, F )  if degL1 (I, F ) < ∞ and degL1 (I, G) < ∞ degL1 (I, F ◦ G) = degL1 (I, F ) + 1 if degL1 (I, F ) < ∞ and degL1 (I, G) = ∞  ∞ otherwise  The idea behind F ◦ G in L1 is that it is preferable to satisfy both F and G. If this is not possible, at least F should be satisfied. In this sense, the choice con- nective of L1 fulfills the same purpose as ordered conjunction in CCL. However, L1 does not use optionality to penalize less preferable interpretations. Instead, the degree of such interpretations is simply incremented by 1. The framework also allows for CLs with multiple choice connectives. For example, one could define a CL that combines the choice connectives of QCL and CCL. #» #» Definition 12. QCCL is the choice logic such that CQCCL = {×, }, #» #» optQCCL (F ×G) = optQCL (F ×G), #» #» optQCCL (F G) = optCCL (F G), #» #» degQCCL (I, F ×G) = degQCL (I, F ×G), and #» #» degQCCL (I, F G) = degCCL (I, F G). Encoding Choice Logics in ASP 7 Since our framework is not very restrictive, there are infinitely many CLs. This includes more exotic CLs than the ones we have seen, with less intuitive properties. 3.2 Equivalence of formulas An important question in any logic is, when are two formulas equivalent. There are different ways to formalize equivalence between two choice formulas. The weakest one is to say that F and G are equivalent if they have the same preferred models, i.e. if M odL (F ) = M odL (G). A stronger notion would be the following. Definition 13. Let F and G be formulas of some choice logic L. F and G are degree-equivalent, written as F ≡L d G, if for all interpretations I we have that degL (I, F ) = degL (I, G). It is easy to see that degree-equivalence of two formulas implies that they also have the same preferred models. However, degree-equivalence does not imply that two formulas can be used interchangeably. This property is usually called strong equivalence [11]. Definition 14. Let A and B be formulas of some choice logic L. A and B are strongly equivalent, written as A ≡L s B, if M odL (F ) = M odL (F [A/B]) for all L-formulas F . In general, two formulas that are degree-equivalent are not necessarily strongly equivalent. However, for some logics, like L1 , it can be checked that degree- equivalence and strong equivalence coincide. We can show that the two concepts coincide for logics that completely ignore the optionality of formulas. Definition 15. A choice logic L is called optionality-ignoring if for all ◦ ∈ CL it holds that if degL (I, F ) = degL (I, F 0 ) and degL (I, G) = degL (I, G0 ), then degL (I, F ◦ G) = degL (I, F 0 ◦ G0 ). Theorem 1. Let L be an optionality-ignoring choice logic. Then A ≡L s B iff A ≡L d B. Proof. Assume first that A ≡L d B. By the definition of a choice logic, the sat- isfaction degree of a formula only depends on the satisfaction degree and the optionality of its subformulas. Now, if a logic is optionality ignoring, then the satisfaction degree of a formula only depends on the satisfaction degree of its subformulas. Therefore, A ≡L L d B implies F ≡d F [A/B] and hence A ≡s B. L L L Assume now that A 6≡d B. We want to show that A 6≡s B, i.e. that there is a formula F such that M odL (F ) 6= M odL (F [A/B]). Since A 6≡L L d B, there exists an interpretation I such that I |=m A and L I |=n B with m 6= n. Let k = min(m, n). We claim that there is a formula G such that the minimum degree that I satisfies G is k. Assume k = m. Then the following formula has the desired property. ^   ^  A∧ x ∧ ¬x . x∈I x∈var(A)\I 8 Michael Bernreiter et al. A similar construction works in the case that k = n. By renaming the variables, we can assume that there are formulas G and H and interpretations IG , IH such that IG |=L L L k G, IH |=k H, J 6|=l G, H for any interpretation J and l < k, and G and H are variable disjoint from each other as well as from A and B. Additionally, we can assume that I ∩ IG = ∅, I ∩ IH = ∅, and IG ∩ IH = ∅. We now construct F = (A ∧ G) ∨ (x ∧ H), where x is a fresh variable. Observe that the minimal degree with which F (or F [A/B]) can possibly be satisfied is k, as either G or H need to be satisfied. Furthermore, IH ∪ {x} |=L L k F and IH ∪ {x} |=k F [A/B]. This means that any preferred model of F must satisfy F with a degree of k. The same is true for preferred models of F [A/B]. Also observe that since x is not contained in I or IG the model I ∪ IG does not satisfy (x ∧ H). Assume k = m. Then I |=L L k A, and therefore I ∪ IG |=k (A ∧ G). Thus, I ∪ IG |=k F , i.e. I ∪ IG ∈ M odL (F ). Analogously, since I |=L L n B, we have that I ∪ IG |=Ln (B ∧ G). Therefore I ∪ IG |= L n F [A/B]. Since n > k, we have I ∪ IG 6∈ M odL (F [A/B]). The case k = n is similar. t u In order to guarantee strong equivalence for every choice logic, both the optionality and the satisfaction degree of two formulas must be the same. Observation 2 Let L be an arbitrary choice logic. If both, A ≡L d B and optL (F ) = optL (G), hold, then A ≡L s B. Clearly, the reverse of Observation 2 is not always true, as Theorem 1 shows. However, for some logics, for example QCL and QCCL, it can be shown that the reverse holds, i.e. two formulas are strongly equivalent if and only if they are degree equivalent and have the same optionality. 4 ASP Encoding We will provide a system written in Clingo 5 with which arbitrary choice logics can be encoded easily. Given a formula as input, each answer set of the encoding (composed of Listings 2–6 below) reports an interpretation together with its satisfaction degree. If one wishes to encode a CL that is not implemented in this system yet, then it suffices to specify the semantics of the CL’s choice connectives in Listing 5. All other functionalities, such as syntax and the semantics of the classical connectives are fixed and readily provided by the encoding. Based on this core encoding, other problems such as finding preferred models or checking for equivalence are then presented in Listings 7, 8, and 10. Input formulas will be contained in the predicate inputformula/1. Classical connectives are represented by functions neg/1, and/2, as well as or/2. Choice connectives can be described with the function pref/3. The first argument of pref/3 is a string that tells us which choice connective we are dealing with. For #» #» example, Listing 1 shows the encoding of ((a×b) ∨ (¬a c)). Encoding Choice Logics in ASP 9 Listing 1. input.lp 1 inputformula ( 2 o r ( p r e f ( ' q c l ' , a , b ) , p r e f ( ' c c l ' , neg ( a ) , c ) ) 3 ). Encoding choice connectives as ternary functions allows for adding new choice connectives and specifying their semantics without worrying about the syntactic implications of doing so. To process the input formula syntactically, we dissect it into subformulas and atoms. Listing 2. base.lp, Part 1 1 s u b f o r m u l a (F , F) :− i n p u t f o r m u l a (F ) . 2 s u b f o r m u l a (F ,G) :− s u b f o r m u l a (F , neg (G) ) . 3 s u b f o r m u l a (F ,G) :− s u b f o r m u l a (F , and (G, ) ) . 4 s u b f o r m u l a (F ,G) :− s u b f o r m u l a (F , and ( ,G) ) . 5 s u b f o r m u l a (F ,G) :− s u b f o r m u l a (F , o r (G, ) ) . 6 s u b f o r m u l a (F ,G) :− s u b f o r m u l a (F , o r ( ,G) ) . 7 s u b f o r m u l a (F ,G) :− s u b f o r m u l a (F , p r e f ( , G, ) ) . 8 s u b f o r m u l a (F ,G) :− s u b f o r m u l a (F , p r e f ( , ,G) ) . 9 10 −atom (F) :− s u b f o r m u l a ( , F ) , F = neg ( ) . 11 −atom (F) :− s u b f o r m u l a ( , F ) , F = and ( , ) . 12 −atom (F) :− s u b f o r m u l a ( , F ) , F = o r ( , ) . 13 −atom (F) :− s u b f o r m u l a ( , F ) , F = p r e f ( , , ) . 14 atom (F) :− s u b f o r m u l a ( , F ) , not −atom (F ) . The above program will yield the fact atom(x) for every constant x that occurs in the input formula. We can use this to guess all relevant interpretations. Listing 3. base.lp, Part 2 1 { i n (F) : atom (F ) } . 2 out (F) :− atom (F ) , not i n (F ) . As for semantics, we will compute the optionality and satisfaction degree of every subformula, and therefore also of the input formula. In Listing 4, we can see how this can be done for the classical connectives. Note that we use the constant #sup, which is built into Clingo, for ∞. Listing 4. base.lp, Part 3 1 opt (F , 1 ) :− s u b f o r m u l a ( , F ) , atom (F ) . 2 opt (F , 1 ) :− s u b f o r m u l a ( , F ) , F = neg ( ) . 3 opt (F ,X) :− s u b f o r m u l a ( , F ) , F = and (G,H) , opt (G,X) , opt (H,Y) , 4 X >= Y. 5 opt (F ,Y) :− s u b f o r m u l a ( , F ) , F = and (G,H) , opt (G,X) , opt (H,Y) , 6 X < Y. 7 opt (F ,X) :− s u b f o r m u l a ( , F ) , F = o r (G,H) , opt (G,X) , opt (H,Y) , 8 X >= Y. 9 opt (F ,Y) :− s u b f o r m u l a ( , F ) , F = o r (G,H) , opt (G,X) , opt (H,Y) , 10 X < Y. 10 Michael Bernreiter et al. 11 12 deg (F , 1 ) :− s u b f o r m u l a ( , F ) , atom (F ) , i n (F ) . 13 deg (F,# sup ) :− s u b f o r m u l a ( , F ) , atom (F ) , out (F ) . 14 deg (F , 1 ) :− s u b f o r m u l a ( , F ) , F = neg (G) , deg (G,# sup ) . 15 deg (F,# sup ) :− s u b f o r m u l a ( , F ) , F = neg (G) , deg (G,K) , K < #sup . 16 deg (F ,X) :− s u b f o r m u l a ( , F ) , F = and (G,H) , deg (G,X) , deg (H,Y) , 17 X >= Y. 18 deg (F ,Y) :− s u b f o r m u l a ( , F ) , F = and (G,H) , deg (G,X) , deg (H,Y) , 19 X < Y. 20 deg (F ,X) :− s u b f o r m u l a ( , F ) , F = o r (G,H) , deg (G,X) , deg (H,Y) , 21 X < Y. 22 deg (F ,Y) :− s u b f o r m u l a ( , F ) , F = o r (G,H) , deg (G,X) , deg (H,Y) , 23 X >= Y. To encode the semantics of the choice connectives, we will use the predicates optIn/3, optOut/4, degIn/5, and degOut/6. Recall that optL (F ◦ G) is a func- tion over optL (F ) and optL (G). This function can be encoded via optIn/3 and optOut/4. The first argument in both of these predicates is the string identifying which choice connective we are dealing with. The second and third arguments are the optionalities of F and G respectively. The fourth argument in optOut/4 is the result of the function call, i.e. the optionality of F ◦ G. The function for the satisfaction degree of the choice connective can be encoded analogously, ex- cept that degL (I, F ◦ G) is a function over optL (F ), degL (I, F ), optL (G), and degL (I, G). Listing 5 shows the specification of QCCL (cf. Definition 12). Listing 5. qccl.lp 1 % D e f i n i t i o n o f QCL c o n n e c t i v e 2 3 optOut ( ' q c l ' , Opt1 , Opt2 , Z ) :− 4 o p t I n ( ' q c l ' , Opt1 , Opt2 ) , Z = Opt1 + Opt2 . 5 6 degOut ( ' q c l ' , Opt1 , Deg1 , Opt2 , Deg2 , Deg1 ) :− 7 degIn ( ' q c l ' , Opt1 , Deg1 , Opt2 , Deg2 ) , 8 Deg1 < #sup . 9 degOut ( ' q c l ' , Opt1 , Deg1 , Opt2 , Deg2 , Deg2 + Opt1 ) :− 10 degIn ( ' q c l ' , Opt1 , Deg1 , Opt2 , Deg2 ) , 11 Deg1 = #sup , Deg2 < #sup . 12 degOut ( ' q c l ' , Opt1 , Deg1 , Opt2 , Deg2 , #sup ) :− 13 degIn ( ' q c l ' , Opt1 , Deg1 , Opt2 , Deg2 ) , 14 Deg1 = #sup , Deg2 = #sup . 15 16 % D e f i n i t i o n o f CCL c o n n e c t i v e 17 18 optOut ( ' c c l ' , X, Y, Z ) :− o p t I n ( ' c c l ' , X, Y) , Z = X + Y. 19 20 degOut ( ' c c l ' , Opt1 , Deg1 , Opt2 , Deg2 , Deg2 ) :− 21 degIn ( ' c c l ' , Opt1 , Deg1 , Opt2 , Deg2 ) , 22 Deg1 = 1 . 23 degOut ( ' c c l ' , Opt1 , Deg1 , Opt2 , Deg2 , Deg1 + Opt2 ) :− Encoding Choice Logics in ASP 11 24 degIn ( ' c c l ' , Opt1 , Deg1 , Opt2 , Deg2 ) , 25 Deg1 > 1 , Deg1 < #sup . 26 degOut ( ' c c l ' , Opt1 , Deg1 , Opt2 , Deg2 , #sup ) :− 27 degIn ( ' c c l ' , Opt1 , Deg1 , Opt2 , Deg2 ) , 28 Deg1 = #sup . We can use this encoding of the optionality and degree functions to compute the values of opt/2 and deg/2 for the choice connectives. This ensures that the custom defined choice connectives are integrated into the base system. Listing 6. base.lp, Part 4 1 o p t I n (CL, X, Y) :− s u b f o r m u l a ( , F ) , F = p r e f (CL, G,H) , 2 opt (G,X) , opt (H,Y ) . 3 opt (F , Z ) :− s u b f o r m u l a ( , F ) , F = p r e f (CL, G,H) , 4 opt (G,X) , opt (H,Y) , optOut (CL, X, Y, Z ) . 5 6 degIn (CL, Opt1 , Deg1 , Opt2 , Deg2 ) :− s u b f o r m u l a ( , F ) , 7 F = p r e f (CL, G,H) , opt (G, Opt1 ) , opt (H, Opt2 ) , 8 deg (G, Deg1 ) , deg (H, Deg2 ) . 9 deg (F , Z ) :− s u b f o r m u l a ( , F ) , F = p r e f (CL, G,H) , 10 opt (G, Opt1 ) , opt (H, Opt2 ) , deg (G, Deg1 ) , deg (H, Deg2 ) , 11 degOut (CL, Opt1 , Deg1 , Opt2 , Deg2 , Z ) . 4.1 Computing Preferred Models To compute all models of the input formula, one has to simply exclude those answer sets that result in an infinite satisfaction degree. Note that, for the sake of a cleaner output, we introduce a predicate deg/1, which holds the satisfaction degree of the input formula. Listing 7. models.lp 1 deg (K) :− i n p u t f o r m u l a (F ) , deg (F ,K) . 2 :− deg(#sup ) . 3 #show i n / 1 . 4 #show deg / 1 . Execute the following bash command to find all models of a formula: $ c l i n g o b a s e . l p q c c l . l p i n p u t . l p models . l p 0 Preferred models of the input formula can be computed with Clingo’s #minimize statement. Instead of minimizing over deg/1, we minimize over the newly intro- duced predicate p/1, which only holds finite satisfaction degrees. This is simply to avoid warning messages, since the #minimize statement is not designed to work with #sup. Listing 8. pref models.lp 1 deg (K) :− i n p u t f o r m u l a (F ) , deg (F ,K) . 12 Michael Bernreiter et al. 2 :− deg(#sup ) . 3 p (K) :− deg (K) , K < #sup . 4 #minimize {X: p (X) } . 5 #show i n / 1 . 6 #show deg / 1 . This bash command gives the preferred model of the given formula: $ c l i n g o −−opt−mode=optN −−q u i e t =1 b a s e . l p q c c l . l p i n p u t . l p pref models . lp 4.2 Checking for Equivalence Some problems, i.e. checking whether two formulas are equivalent, require more than one input formula. Recall, for example, that two QCL formulas are strongly equivalent if they are degree equivalent and have the same optionality (see Ob- servation 2 and the remark following it). In what follows we discuss how to test strong equivalence in QCL using our encoding. We introduce the predi- cates inputformula1/1 and inputformula2/1. In Listing 9, we see the encoding #» #» #» #» of F1 = (a×(b×c)) and F2 = ((a×b)×c). Note that F1 and F2 are strongly equivalent, since ordered disjunction is associative. Listing 9. input2.lp 1 inputformula1 ( 2 pref ( ' qcl ' , a , pref ( ' qcl ' , b , c )) 3 ). 4 inputformula2 ( 5 pref ( ' qcl ' , pref ( ' qcl ' , a , b ) , c ) 6 ). Instead of directly checking whether F1 and F2 are strongly equivalent, we solve the complementary problem: If we find an interpretation (i.e. an answer set) where F1 and F2 are ascribed different satisfaction degrees, or show that the optionalities of F1 and F2 are not equal, then F1 and F2 are not strongly equivalent. See Listing 10 for how this can be implemented. The two input formulas are strongly equivalent if and only if the program is unsatisfiable. Listing 10. strong equiv.lp 1 i n p u t f o r m u l a (F) :− i n p u t f o r m u l a 1 (F ) . 2 i n p u t f o r m u l a (F) :− i n p u t f o r m u l a 2 (F ) . 3 4 s a m e d e g r e e :− i n p u t f o r m u l a 1 (F ) , i n p u t f o r m u l a 2 (G) , 5 deg (F ,K) , deg (G, L ) , K=L . 6 s a m e o p t i o n a l i t y :− i n p u t f o r m u l a 1 (F ) , i n p u t f o r m u l a 2 (G) , 7 opt (F ,K) , opt (G, L ) , K=L . 8 :− s a m e d e g r e e , s a m e o p t i o n a l i t y . 9 10 #show i n / 1 . Encoding Choice Logics in ASP 13 Note that Listing 10 also includes the rules inputformula(F) :− inputformula1(F) and inputformula(F) :− inputformula2(F). If this were not the case, then input- formula1/1 and inputformula2/1 could not be processed correctly by the base program. The following program call has to be made to check whether two for- mulas are degree-equivalent and have the same optionality: $ c l i n g o base . lp q c c l . lp input . lp s t r o n g e q u i v . lp To check directly for strong equivalence, instead of solving the complementary problem, one could employ the saturation technique described by Egly et al. [10]. This would require modifications to the base program, as default negation can not be used with this technique. Of course, one could also check for degree-equivalence. This can be done analogously to Listing 10, except that we do not need to verify whether the two formulas have the same optionality or not. 5 Conclusion In this paper, we introduced a framework for choice logics that encompasses both QCL and CCL. Furthermore, we showed how logics in this framework can be encoded via ASP, and how certain problems, such as finding preferred models for a given formula, or checking whether two formulas are strongly equivalent, can be solved using this encoding. The encodings as provided in this paper are available under https://github.com/mbernr/choice-logics-asp. There we also provide specifications for further variants of choice logics. The described ASP system can also be used in conjunction with other sys- tems. As an alternative to encoding the choice connectives of a CL in pure ASP, the optionality- and degree functions could be described externally. For exam- ple, in Clingo 5, Python or Lua can be used to encode functions. Specifying the semantics of a CL in this way might be more convenient for some users. Further- more, it is possible to make calls to Clingo 5 programs from other environments, such as Python. This allows for a system in which the business logic runs in Python, but when reasoning about preferences is needed, the ASP program can be employed. A further possible field of study is to investigate the CL framework more closely, by looking at some of the properties of choice logics. Since the definition of a CL is not very restrictive, one could examine certain subgroups of choice logics that exhibit certain, possibly desirable, properties. Lastly, instead of encoding choice logics within ASP, it would also be possible to extend ASP itself by choice connectives. This has already been done with ordered disjunction, resulting in Logic Programming with Ordered Disjunction (LPOD) [3, 6]. 14 Michael Bernreiter et al. References 1. Benferhat, S., Sedki, K.: Two alternatives for handling preferences in qualitative choice logic. Fuzzy Sets Syst. 159(15), 1889–1912 (2008), https://doi.org/10.1016/ j.fss.2008.02.014 2. Boudjelida, A., Benferhat, S.: Conjunctive choice logic. In: International Sympo- sium on Artificial Intelligence and Mathematics, ISAIM 2016, Fort Lauderdale, Florida, USA, January 4-6, 2016 (2016), http://isaim2016.cs.virginia.edu/papers/ ISAIM2016\ Boudjelida\ Benferhat.pdf 3. Brewka, G.: Answer sets and qualitative decision making. Synthese 146(1-2), 171– 187 (2005), https://doi.org/10.1007/s11229-005-9084-7 4. Brewka, G., Benferhat, S., Berre, D.L.: Qualitative choice logic. Artif. Intell. 157(1- 2), 203–237 (2004), https://doi.org/10.1016/j.artint.2004.04.006 5. Brewka, G., Delgrande, J.P., Romero, J., Schaub, T.: asprin: Customizing answer set preferences without a headache. In: Bonet, B., Koenig, S. (eds.) Proceedings of the Twenty-Ninth AAAI Conference on Artificial Intelligence, January 25-30, 2015, Austin, Texas, USA. pp. 1467–1474. AAAI Press (2015), http://www.aaai. org/ocs/index.php/AAAI/AAAI15/paper/view/9535 6. Brewka, G., Niemelä, I., Syrjänen, T.: Logic programs with ordered disjunction. Comput. Intell. 20(2), 335–357 (2004), https://doi.org/10.1111/j.0824-7935.2004. 00241.x 7. Charwat, G., Pfandler, A.: Democratix: A declarative approach to winner deter- mination. In: Walsh, T. (ed.) Algorithmic Decision Theory - 4th International Conference, ADT 2015, Lexington, KY, USA, September 27-30, 2015, Proceed- ings. LNCS, vol. 9346, pp. 253–269. Springer (2015), https://doi.org/10.1007/ 978-3-319-23114-3\ 16 8. Costantini, S., Formisano, A., Petturiti, D.: Extending and implementing RASP. Fundam. Inform. 105(1-2), 1–33 (2010), https://doi.org/10.3233/FI-2010-356 9. Delgrande, J.P., Schaub, T., Tompits, H.: A framework for compiling preferences in logic programs. Theory Pract. Log. Program. 3(2), 129–187 (2003), https://doi. org/10.1017/S1471068402001539 10. Egly, U., Gaggl, S.A., Woltran, S.: Answer-set programming encodings for argu- mentation frameworks. Argument & Computation 1(2), 147–177 (2010), https: //doi.org/10.1080/19462166.2010.486479 11. Faber, W., Truszczynski, M., Woltran, S.: Abstract preference frameworks - a unify- ing perspective on separability and strong equivalence. In: desJardins, M., Littman, M.L. (eds.) Proceedings of the Twenty-Seventh AAAI Conference on Artificial In- telligence, July 14-18, 2013, Bellevue, Washington, USA. pp. 297–303. AAAI Press (2013), http://www.aaai.org/ocs/index.php/AAAI/AAAI13/paper/view/6294 12. de Haan, R., Slavkovik, M.: Answer set programming for judgment aggregation. In: Kraus, S. (ed.) Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, Macao, China, August 10-16, 2019. pp. 1668– 1674. ijcai.org (2019), https://doi.org/10.24963/ijcai.2019/231 13. Pigozzi, G., Tsoukiàs, A., Viappiani, P.: Preferences in artificial intelligence. Ann. Math. Artif. Intell. 77(3-4), 361–401 (2016), https://doi.org/10.1007/ s10472-015-9475-5