# choice_logics_and_their_computational_properties__fe555282.pdf

Choice Logics and Their Computational Properties

Michael Bernreiter , Jan Maly and Stefan Woltran Institute of Logic and Computation, TU Wien, Austria {mbernrei, jmaly, woltran}@dbai.tuwien.ac.at

Qualitative Choice Logic (QCL) and Conjunctive Choice Logic (CCL) are formalisms for preference handling, with especially QCL being well established in the ﬁeld of AI. So far, analyses of these logics need to be done on a case-by-case basis, albeit they share several common features. This calls for a more general choice logic framework, with QCL and CCL as well as some of their derivatives being particular instantiations. We provide such a framework, which allows us, on the one hand, to easily deﬁne new choice logics and, on the other hand, to examine properties of different choice logics in a uniform setting. In particular, we investigate strong equivalence, a core concept in nonclassical logics for understanding formula simpliﬁcation, and computational complexity. Our analysis also yields new results for QCL and CCL. For example, we show that the main reasoning task regarding preferred models is Θ2P-complete for QCL and CCL, while being 2P-complete for a newly introduced choice logic.

1 Introduction Representing preferences and reasoning about them is a key challenge in many areas of AI research. One of the most fruitful approaches to preference representation has been the use of logic-based formalisms [Domshlak et al., 2011; Pigozzi et al., 2016]. Two closely related examples from the literature are Qualitative Choice Logic (QCL) [Brewka et al., 2004a] and Conjunctive Choice Logic (CCL) [Boudjelida and Benferhat, 2016]. Especially QCL has proven to be a useful preference formalism, with applications ranging from logic programming [Brewka et al., 2004b] to alert correlation [Benferhat and Sedki, 2008a] to database querying [Lietard et al., 2014]. However, several key computational properties of QCL and CCL have not been studied yet. This includes strong equivalence, a tool to understand formula simpliﬁcation, and the computational complexity of main reasoning tasks. Moreover, QCL and CCL are certainly not the only possible logic-based formalisms. QCL extends classical propositional logic with a non-classical connective # called ordered disjunction. Intuitively, F # G means that it is preferable to

satisfy F but, if that is not possible, then satisfying G is also acceptable. Similarly, CCL introduces ordered conjunction (# ), where the intended meaning of F # G is that it is most preferable to satisfy both F and G, but satisfying only F is also acceptable. More speciﬁcally, interpretations ascribe a number, called satisfaction degree, to QCLand CCLformulas. The preferred models of a formula are those models with the least degree. Other natural preferences cannot be succinctly represented in QCL and CCL. For example, one could think of a more ﬁne-grained choice connective: given F G, it would be best to satisfy both F and G, second best to satisfy only F, and third best to satisfy only G. Or one could desire a connective with the same basic behavior as # in QCL, but in which satisfaction degrees are handled in a different way. There is a multitude of interesting logics related to QCL and CCL that have yet to be deﬁned, and which may very well prove to be as useful as QCL. In this paper, we propose a general framework for choice logics that, on the one hand, makes it easy to deﬁne new choice logics by specifying one or more choice connectives and, on the other hand, allows us to settle open questions regarding the computational properties of QCL and CCL in a uniform way. In detail, our main contributions are as follows:

We formally deﬁne a framework that captures both QCL and CCL, as well as inﬁnitely many new related logics. To showcase the versatility of our framework we explicitly introduce two such new logics called Lexicographic Choice Logic (LCL) and Simple Conjunctive Choice Logic (SCCL).

We characterize strong equivalence via simpler equivalence notions for large classes of choice logics. This further enables us to analyze properties related to strong equivalence more easily, and also provides valuable insights into the nature of choice logics.

We analyze the computational complexity of choice logics in detail.1 For example, we show that the complexity of the main decision problem regarding preferred models ranges from NPto 2P-completeness with QCL and CCL being located in between (Θ2P-complete).

1The complexity of some decision problems pertaining to QCL was conjectured in [Lang, 2004] but never formally investigated.

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

Related Work. QCL and CCL are not the only logicbased preference representation formalisms. Other prominent examples include the preference logics introduced by von Wright [1963] and in [van Benthem et al., 2009]; for a more complete overview, see the surveys [Domshlak et al., 2011; Bienvenu et al., 2010]. Most of these formalisms differ from choice logics in that they only represent preferences, while QCL and CCL integrate the representation of truth and preference in one formalism. One exception is recent work by Charalambidis et al. [2020], which is conceptually closely related to our LCL, but differs in that formulas are assigned lists of truth values instead of satisfaction degrees. From a technical standpoint, many non-monotonic logics are closely related to QCL, as they are inherently connected to preferences [Shoham, 1987]. This is particularly true for propositional circumscription and possibilistic logic [Brewka et al., 2004a]. However, unlike choice logics, these formalisms are not primarily designed to represent preferences and often rely on constructs outside of the logical language (circumscription policy, possibility distribution) to represent knowledge. It is also worth noting that choice logics are technically very different from traditional inﬁnite-valued logics [Gottwald, 2001] as, for example, choice logics use classical interpretations that make atoms either true or false. There are also systems that are based on QCL s ordered disjunction, but do not ﬁt into our framework. We mention here the modal logic from [Jiang et al., 2015] and prioritized disjunction for game strategies [Zhang and Thielscher, 2015].

2 Choice Logic Framework We shall start with introducing our general framework, then show how both existing and new logics can be deﬁned in this framework, and ﬁnally give a synthesis result that holds for any choice logic of our framework. In what follows, PL stands for classical propositional logic, U denotes the alphabet of propositional variables, and an interpretation I is deﬁned as a set of propositional variables such that a I if and only if a is set to true by I. If I satisﬁes a classical formula F, we write I |= F.

2.1 Syntax and Semantics A choice logic has two types of connectives: classical connectives (here we use , , and ), and binary choice connectives, with which preferences can be expressed. Deﬁnition 1. The set of choice connectives CL of a choice logic L is a ﬁnite set of symbols such that CL { , , } = . The set FL of formulas of L is deﬁned inductively as follows: (i) a FL for all a U; (ii) if F FL, then ( F) FL; (iii) if F, G FL, then (F G) FL for ({ , } CL). var(F) denotes the set of all variables in a formula F FL.

For example, CQCL = {# } and CPL = . Formulas that do not contain a choice connective are simply classical formulas. The semantics of a choice logic is given by two functions, satisfaction degree and optionality. The satisfaction degree of a formula given an interpretation is either a natural number or . The lower this degree, the more preferable the interpretation. The optionality of a formula describes the maximum ﬁnite satisfaction degree that this formula can be ascribed.

Deﬁnition 2. The optionality of a choice connective CL in a choice logic L is given by a function opt L : N2 N such that opt L(k, ℓ) (k + 1) (ℓ+ 1) for all k, ℓ N. The optionality of an L-formula is given via opt L : FL N with

1. opt L(a) = 1, for every a U;

2. opt L( F) = 1;

3. opt L(F G) = max(opt L(F), opt L(G));

4. opt L(F G) = max(opt L(F), opt L(G));

5. opt L(F G) = opt L(opt L(F), opt L(G)) for CL.

The optionality of a classical formula is always 1. For any choice connective , the optionality of F G is bounded such that opt L(F G) (opt L(F)+1) (opt L(G)+1). The reason for this is that there are opt L(F) many ﬁnite degrees that could be ascribed to F, plus the inﬁnite degree . Likewise for G. Thus, there are at most (opt L(F)+1) (opt L(G)+1) possibilities when combining the degrees of F and G. Next, we deﬁne the satisfaction degree of a formula. In the following, we write N for (N { }).

Deﬁnition 3. The satisfaction degree of a choice connective CL in a choice logic L is given by a function deg L : N2 N 2 N such that either deg L(k, ℓ, m, n) opt L(k, ℓ) or deg L(k, ℓ, m, n) = for all k, ℓ N and all m, n N. The satisfaction degree of an L-formula under an interpretation is given via deg L : 2U FL N with

1. deg L(I, a) = 1 if a I, otherwise, for every a U;

2. deg L(I, F) = 1 if deg L(I, F) = , otherwise;

3. deg L(I, F G) = max(deg L(I, F), deg L(I, G));

4. deg L(I, F G) = min(deg L(I, F), deg L(I, G));

5. deg L(I, F G) = deg L(k, ℓ, m, n) for every CL, where k = opt L(F), ℓ= opt L(G), m = deg L(I, F), and n = deg L(I, G).

We also write I |=L m F for deg L(I, F) = m. If m < , we say that I satisﬁes F (to a ﬁnite degree), and if m = , then I does not satisfy F. If F is a classical formula, then I |=L 1 F I |= F and I |=L F I |= F. The symbols and are shorthand for the formulas (a a) and (a a), where a can be any variable. We have opt L( ) = opt L( ) = 1, deg L(I, ) = 1 and deg L(I, ) = for any interpretation I in every choice logic. The semantics of the classical connectives are ﬁxed and are the same as for QCL and CCL. F G is assigned the maximum degree of F and G because both formulas need to be satisﬁed. Conversely, we use the minimum degree for F G since satisfying either option sufﬁces, and we do not need to concern ourselves with the less preferable option. Observe that it is still necessary to deﬁne opt L(F G) = max(opt L(F), opt L(G)), as the case that either option is not satisﬁed has to be allowed for. As for negation, note that F can only assume the degrees 1 or . In order to deﬁne a form of negation that results in different degrees of satisfaction, we would need to keep track of degrees of dissatisfaction. We

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

observe that the semantics of the classical connectives used here are not the only possible ones. See also the brief discussion on PQCL and QCL+ in Section 2.2. From Deﬁnitions 2 and 3 it follows that the satisfaction degree of a choice logic formula is bounded by its optionality as intended, i.e., for all interpretations I and all L-formulas F, either deg L(I, F) opt L(F) or deg L(I, F) = . Moreover, note that only those variables that actually occur in a formula F can inﬂuence opt L(F) and deg L(I, F), which means that we can assume I var(F) for any interpretation I that we are dealing with. An interpretation that satisﬁes a formula to a ﬁnite degree will be referred to as a model of that formula. But often we are interested only in the most preferable models.

Deﬁnition 4. Let L be a choice logic. Then an interpretation I is a preferred model of an L-formula F, written as I Prf L(F), if deg L(I, F) = and, for all other interpretations J , deg L(I, F) deg L(J , F).

By the above deﬁnition, Prf L(F) = if and only if deg L(I, F) = for all interpretations I.

2.2 Examples of Choice Logics

To deﬁne a choice logic L, it sufﬁces to specify the choice connectives CL of that logic, and to provide the optionalityand satisfaction degree functions of every CL. The simplest example for a choice logic is classical propositional logic, where CPL = . Since all PL-formulas are classical formulas, I Prf PL(F) I |= F. QCL can be expressed in our framework as follows:

Deﬁnition 5. QCL is the choice logic such that CQCL = {# }, and, if k = opt QCL(F), ℓ= opt QCL(G), m = deg QCL(I, F), and n = deg QCL(I, G) for some F, G, I, then

opt QCL(F # G) = opt # QCL(k, ℓ) = k + ℓ, and

deg QCL(I, F # G) = deg # QCL(k, ℓ, m, n)

m if m < ; n + k if m = , n < ; otherwise.

Here, we can see how optionality is used to penalize non-satisfaction: if F is satisﬁed, then deg QCL(I, F # G) = deg QCL(I, F) opt L(F); if F is not satisﬁed, but G is, then deg QCL(I, F # G) = deg QCL(I, G) + opt L(F) > opt L(F). Thus, any interpretation which satisﬁes F is automatically more preferable than one that does not. The fourth column of Table 1 illustrates QCL semantics on a simple example. From there, we can infer that {a} and {a, b} are preferred models of a# b, while and {b} are not. We know that # is associative from [Brewka et al., 2004a], which means that given arbitrary QCL-formulas A, B, and C, the formulas ((A# B)# C) and (A# (B # C)) always have the same optionality and satisfaction degrees. We can therefore write F1 # F2 . . . # Fn to express that we prefer F1 to F2, F2 to F3, and so on. For variables a1, . . . , an with ai = aj for all i = j, we have that {ai} |=QCL i (a1 # a2 . . . # an).

I a b a b a# b a# b a# b a# b

{b} 1 2 3 {a} 1 1 2 2 2 {a, b} 1 1 1 1 1 1

Table 1: The classical connectives , and the choice connectives # (QCL), # (CCL), # (LCL), and # (SCCL) applied to atoms.

Next, we formally deﬁne CCL. However, our function for the satisfaction degree of # differs from the one given in [Boudjelida and Benferhat, 2016]. This is because the original deﬁnition of CCL, although it can be expressed in our framework if desired, fails to capture the intended meaning of ordered conjunction.2

Deﬁnition 6. CCL is the choice logic such that CCCL = {# }, and, if k = opt CCL(F), ℓ= opt CCL(G), m = deg CCL(I, F), and n = deg CCL(I, G) for some F, G, I, then

opt CCL(F # G) = k + ℓ, and

deg CCL(I, F # G) =

n if m = 1, n < ; m + ℓ if m < and (m > 1 or n = ); otherwise.

Intuitively, given F # G, it is best to satisfy both F and G, while satisfying only F is less preferable, but still acceptable. As intended, # is associative under this new semantics for CCL. This will be shown in Section 3 (see Lemma 7). For a series of distinct propositional variables, we have that {a1, . . . , a(n i+1)} |=CCL i (a1 # a2 . . . # an). While QCL and CCL feature only a single choice connective, our framework now easily allows to deﬁne a choice logic with the choice connectives of both QCL and CCL, i.e. CQCCL = {# , # }, opt # QCCL = opt # QCL, deg # QCCL = deg # QCL, and likewise for CCL and # . We now introduce a new logic, called Lexicographic Choice Logic (LCL), whose choice connective deals with satisfaction degrees in a more ﬁne-grained manner. Deﬁnition 7. LCL is the choice logic such that CLCL = {# }, and, if k = opt LCL(F), ℓ= opt LCL(G), m = deg LCL(I, F), and n = deg LCL(I, G) for some F, G, I, then

opt LCL(F # G) = (k + 1) (ℓ+ 1) 1, and

deg LCL(I, F # G) =

(m 1) ℓ+ n if m < , n < ; k ℓ+ m if m < , n = ; k ℓ+ k + n if m = , n < ; otherwise.

Given F # G it is best to satisfy both F and G, second best to satisfy only F, and third best to satisfy only G. Satisfying neither F nor G is not acceptable. Let F = (a# (b# c)).

2In our understanding, under the semantics described in [Boudjelida and Benferhat, 2016, Deﬁnition 8], the formula a# b will always be ascribed a degree of either or 1.

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

The only interpretation that ascribes a degree of to F is . The remaining 7 interpretations applicable to F each result in a different degree, ranging from 1 to 7. For example, {a, b, c} |=LCL 1 F, {a, b} |=LCL 2 F, {a, c} |=LCL 3 F, and so on until {c} |=LCL 7 F. In this way, # enables us to succinctly encode lexicographic orderings over variables. It is also possible to deﬁne a choice logic that does not use optionality. We call the following new logic Simple Conjunctive Choice Logic (SCCL). Deﬁnition 8. SCCL is the choice logic such that CSCCL = {# }, and, if k = opt SCCL(F), m = deg SCCL(I, F), and n = deg SCCL(I, G) for some F, G, I, then

opt SCCL(F # G) = k + 1, and

deg SCCL(I, F # G) =

m if m < , n < ; m + 1 if m < , n = ; otherwise.

SCCL is similar to CCL in that the intended meaning of F # G is the same as that of F # G, i.e., satisfying F and G is most preferable, but satisfying only F is also acceptable. However, SCCL does not use optionality to penalize less preferable interpretations. Instead, the degree of such interpretations is simply incremented by 1. Note that # is not associative, since {a, b} ascribes a degree of 1 to (a# (b# c)) and a degree of 2 to ((a# b)# c). Lastly, we want to discuss two variants of QCL introduced in [Benferhat and Sedki, 2008b] called PQCL and QCL+. Both of these logics deﬁne # in the same way as standard QCL, but differ in how classical connectives deal with satisfaction degrees. The alternative conjunctions and disjunctions featured in PQCL and QCL+ can be implemented in our framework as choice connectives, if desired. In fact, some behave more like choice connectives than classical connectives, as, for example, the conjunction of PQCL favors interpretations that ascribe a lower satisfaction degree to the ﬁrst operand rather than the second. The semantics of # in LCL is built on this principle, and is actually an extension of in PQCL. The alternative deﬁnition for negation in PQCL and QCL+ is more involved, but can be simulated in our framework by restricting ourselves to formulas where negations appear only in front of atoms. This means that PQCL and QCL+ can be captured by our framework as fragments.

2.3 Expressiveness It can be shown that any logic deﬁned in our framework is powerful enough to express arbitrary assignments of satisfaction degrees to interpretations by a forumula as long as the degrees are obtainable in the following sense:

Deﬁnition 9. A degree m N is called obtainable in a choice logic L if there exists an interpretation I and an Lformula F such that deg L(I, F) = m. By DL we denote the set of all degrees obtainable in a choice logic L. For example, DPL = {1, } and DQCL = N. Proposition 1. Let L be a choice logic. Let V be a ﬁnite set of propositional variables, and let s be a function s: 2V DL. Then there is an L-formula F with var(F) V such that, for all I V , deg L(I, F) = s(I).

Proof. Consider any interpretation J V . Let GJ be a classical formula that characterizes J over V , i.e. J |= GJ , but J |= GJ for all J V such that J = J . Since s(J ) DL, there is a formula H such that deg L(J , H) = s(J ) for some interpretation J . We obtain the formula SJ by replacing every variable in H that occurs in J by , and all other variables in H by . Then deg L(J , SJ ) = deg L(J , H) = s(J ). Now, F = W J V (GJ SJ ) is an L-formula with the desired properties.

3 Strong Equivalence We now investigate strong equivalence in the sense of replaceability [Faber et al., 2013] of preferred models. F[A/B] denotes the substitution of an occurrence of A in F by B. Deﬁnition 10. Two formulas A and B of a choice logic L are strongly equivalent, written as A L s B, if Prf L(F) = Prf L(F[A/B]) for all L-formulas F. Strong equivalence is a crucial notion towards simpliﬁcation, thus a characterization that avoids going through inﬁnitely many formulas is needed. We show that strong equivalence often can be decided via simpler equivalence notions. Deﬁnition 11. Two formulas A and B of a choice logic L are degree-equivalent, written as A L d B, if deg L(I, A) = deg L(I, B) for all interpretations I. Lemma 2. Let L be a choice logic. If A L d B, then Prf L(A) = Prf L(B).

The converse of Lemma 2 is not true: a and (a# b) have the same preferred models in QCL, but {b} |=QCL a, while {b} |=QCL 2 (a# b). Since the satisfaction degree of a formula might also depend on optionality, the notion of degreeequivalence is not strong enough in many cases; we thus also consider the following notion, which actually appears under the name of strong equivalence in [Brewka et al., 2004a]. Deﬁnition 12. Two L-formulas A and B are fully equivalent, written as A L f B, if A L d B and opt L(A) = opt L(B).

Lemma 3. Let L be a choice logic. Then A L f B if and only if F L f F[A/B] for all L-formulas F.

The above lemma states that two formulas are fully equivalent if and only if they can be substituted for each other without affecting satisfaction degree or optionality. This is even stronger than strong equivalence which only demands that substitution does not affect preferred models. Proposition 4. A L f B = A L s B = A L d B for any choice logic L and all L-formulas A, B. In general, all three equivalence notions are different. For example, in SCCL, a and (a# a) are not fully equivalent, since they differ in optionality, but they are strongly equivalent, since optionality does not impact satisfaction degrees in SCCL. On the other hand, in QCL, a and (a# a) are degreeequivalent and F = (((a# b) (c# d)) a c) has {b} as a preferred model, but replacing the ﬁrst occurrence of a in F by a# a means {b} is no longer preferred. However, for natural classes of choice logics strong equivalence coincides with either degree-equivalence or full equivalence.

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

Deﬁnition 13. A choice logic L is called optionality-ignoring if for all CL, deg L(I, F G) = deg L(I, F G ) whenever deg L(I, F) = deg L(I, F ) and deg L(I, G) = deg L(I, G ).

It is easy to see that PL and SCCL are optionality-ignoring, while QCL, CCL, and LCL are not.

Proposition 5. Let L be an optionality-ignoring choice logic. Then A L s B iff A L d B for all L-formulas A, B.

Similar to the above result, we can characterize strong equivalence by full equivalence in choice logics where, as soon as two formulas differ in optionality, they can no longer be safely substituted for each other without affecting satisfaction degrees.

Deﬁnition 14. A choice logic L is called optionalitydifferentiating if for all L-formulas A and B with opt L(A) = opt L(B), there is an L-formula F such that F L d F[A/B].

PL, QCL, CCL, and LCL are optionality-differentiating (while SCCL is not). We show this for QCL: Consider any A, B such that opt QCL(A) = opt QCL(B). Then F = ((A )# a) has the desired property: (A ) can never be satisﬁed, and since opt QCL(A ) = opt QCL(A), F is satisﬁed by {a} with a degree of opt QCL(A) + 1. Likewise, F[A/B] is satisﬁed by {a} with a degree of opt QCL(B) + 1.

Proposition 6. Let L be an optionality-differentiating choice logic. Then A L s B iff A L f B for all L-formulas A, B.

Proof. The if-direction is by Proposition 4. So, let A L s B. By Proposition 4, A L d B. Towards a contradiction, assume opt L(A) = opt L(B). Since L is optionality-differentiating, A L d A [A/B] for some A FL, i.e. A occurs in A . Let B = A [A/B]. By the contrapositive of Proposition 4, Prf L(F) = Prf L(F[A /B ]) for some F FL. Since replacing A by A [A/B] in F is the same as simply replacing A by B in F (i.e. F[A /B ] = F[A /A [A/B]] = F[A/B]), Prf L(F) =Prf L(F[A/B]). This contradicts A L s B.

In fact, strong equivalence and full equivalence are interchangeable only for optionality-differentiating choice logics. Consider a non optionality-differentiating L. Then there are L-formulas A and B such that opt L(A) = opt L(B), while for all L-formulas F we have that F L d F[A/B]. This implies A L s B. But A L f B, since opt L(A) = opt L(B). In Section 2.2, we discussed associativity of # in QCL. A matching strong equivalence result can now be achieved for CCL as well, and it is easily proven using Proposition 6.

Lemma 7. Choice connective # CCCL is associative, i.e. ((F # G)# H) CCL s (F # (G# H)) for any F, G, H FCCL.

To conclude, knowing whether a choice logic is optionality-ignoring (e.g. SCCL) or optionalitydifferentiating (e.g. QCL, CCL, LCL) is useful, since it allows to decide strong equivalence via degreeor full equivalence. However, note that choice logics which are neither optionality-ignoring nor -differentiating do exist.

4 Computational Complexity

Next, we examine the computational complexity of choice logics. So far we have imposed only few restrictions on optionalityand degree functions, which means that there are choice logics whose semantics are given by computationally expensive or even undecidable functions. For reasons of practicality, we focus on so-called tractable choice logics.

Deﬁnition 15. A choice logic L is called tractable if the optionalityand degree functions of every choice connective in L are polynomial-time computable.

All logics presented in this paper are tractable in this sense. The ﬁrst decision problems that we look at are concerned with satisfaction degrees: in L-DEGREECHECKING we ask whether, given an L-formula F, an interpretation I, and a satisfaction degree k N, it holds that deg L(I, F) k; in L-DEGREESAT we ask whether, given an L-formula F and a satisfaction degree k N, there is an interpretation I such that deg L(I, F) k. These two problems are straightforward generalizations of model checking and satisﬁability for classical propositional logic, and they do not differ in complexity from their classical counterparts.

Proposition 8. For any tractable choice logic L, LDEGREECHECKING is in P; L-DEGREESAT is NP-complete.

The picture changes when we reformulate the problems in terms of preferred models.

Deﬁnition 16. We deﬁne decision problems

L-PREFMODELCHECKING: given F FL and an interpretation I, does I Prf L(F) hold;

L-PREFMODELSAT: given F FL and variable a, is there an interpretation I Prf L(F) such that a I.

Proposition 9. L-PREFMODELCHECKING is in co NP for any tractable choice logic L.

Note that PL-PREFMODELCHECKING is identical to PLDEGREECHECKING, since I Prf PL(F) I |=PL 1 F. Hence, we cannot expect co NP-hardness in general, but we show the result for all logics where degrees other than 1 and are obtainable, and thus for QCL, CCL, SCCL, and LCL.

Proposition 10. L-PREFMODELCHECKING is complete for co NP in any tractable choice logic L where DL = {1, }.

We turn to L-PREFMODELSAT and ﬁrst give an upper bound for the optionality of choice logic formulas relative to their size. In the following, |F| denotes the total number of variables occurrences in F, e.g. |(x x y)| = 3.

Lemma 11. Let L be a choice logic. Then, for every Lformula F it holds that opt L(F) < 2(|F |2).

This is likely not a tight bound, but it is good enough for our purposes. Recall that 2P is the class of decision problems that can be solved in polynomial time on a deterministic Turing machine with access to an arbitrary number of NPoracle calls. Θ2P is deﬁned analogously but only a logarithmic number of NP-oracle calls is permitted.

Proposition 12. L-PREFMODELSAT is in 2P and NP-hard for any tractable choice logic L.

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

L = PL L {QCL, CCL, SCCL} L = LCL Opt-diff./ignor. Tract.

L-DEGREECHECKING in P in P in P in P in P L-DEGREESAT NP-c NP-c NP-c NP-c NP-c L-PREFMODELCHECKING in P co NP-c co NP-c in co NP in co NP L-PREFMODELSAT NP-c Θ2P-c 2P-c in 2P/NP-h in 2P/NP-h L-FULLEQUIVALENCE co NP-c co NP-c co NP-c co NP-c co NP-c L-DEGREEEQUIVALENCE co NP-c co NP-c co NP-c co NP-c co NP-c L-STRONGEQUIVALENCE co NP-c co NP-c co NP-c co NP-c ?

Table 2: Summary of complexity results. Opt-diff./ignor. stands for tractable L which are either optionality-ignoring or optionalitydifferentiating. Tract. stands for tractable L.

These are tight bounds in the sense that there are choice logics for which L-PREFMODELSAT is 2P-complete (Proposition 15) and choice logics for which it is NPcomplete (just take L = PL). However, there are also choice logics for which the complexity lies between these two classes. The key is to restrict optionality.

Proposition 13. L-PREFMODELSAT is in Θ2P for every tractable choice logic L in which for some constant c and all L-formulas F it holds that opt L(F) O(|F|c).

This implies that L-PREFMODELSAT is in Θ2P for L {QCL, CCL, SCCL}. In fact, these logics are Θ2P-complete.

Proposition 14. L-PREFMODELSAT is Θ2P-complete for L {QCL, CCL, SCCL}.

Proof. We show Θ2P-hardness for QCL (CCL and SCCL are similar) via reduction from the Θ2P-complete problem LOGLEXMAXSAT [Creignou et al., 2018]. Consider an instance of LOGLEXMAXSAT, where, given a PL-formula F and an ordering x1 > > xn over n of the variables in F, where n log(|F|), we ask whether xn is true in the lexicographically largest interpretation J {x1, . . . , xn} that can be extended to a model of F. We construct an instance (F , xn) of QCL-PREFMODELSAT as follows: Let Ji be the lexicographically i-th largest interpretation over the given ordering, e.g. J1 = {x1, . . . , xn}, J2 = {x1, . . . , xn 1}, and J(2n) = . Every Ji can be characterized by a classical formula Ai such that |Ai| O(n) and I |= Ai iff I {x1, . . . , xn} = Ji for all I. Now construct F = F (A1 # A2 # # A(2n)). Observe that |F | is polynomial in |F| since n log(|F|). For all I, deg L(I, F ) = i, where i < , iff I {x1, . . . , xn} = Ji and I |= F.

In contrast, LCL allows to represent the lexicographic order with an exponentially smaller formula than QCL, CCL, and SCCL. For LCL, we can thus drop the condition n log(|F|) in the construction above, yielding a reduction from LEXMAXSAT, which is 2P-hard [Creignou et al., 2018].

Proposition 15. LCL-PREFMODELSAT is 2P-complete.

Finally, we consider L-FULLEQUIVALENCE, the problem of deciding whether A L f B holds for given L-formulas A and B, as well as L-DEGREEEQUIVALENCE and LSTRONGEQUIVALENCE which are deﬁned analogously. In the following result, hardness follows from PL; membership of (2) is by our characterizations in Section 3.

Proposition 16. For any tractable choice logic L, (1) L-FULLEQUIVALENCE and L-DEGREEEQUIVALENCE are co NP-complete; (2) L-STRONGEQUIVALENCE is co NPcomplete if L is optionality-ignoring or -differentiating.

Table 2 summarizes our complexity results for tractable choice logics, thus including all speciﬁc logics studied so far; a full analysis may be conducted in a similar way by using oracles for the optionalityand satisfaction degree functions.

5 Conclusion

We deﬁned and investigated a general framework for choice logics that captures both QCL and CCL, but also allows to deﬁne new logics as exampliﬁed via SCCL and LCL. We have shown that strong equivalence is interchangeable with degree-equivalence for optionality-ignoring choice logics (e.g. SCCL) and with full equivalence for optionalitydifferentiating choice logics (e.g. QCL, CCL, LCL). Moreover, the computational complexity of tractable choice logics was investigated in detail. An initial deﬁnition of our framework and some further results regardings choice logics can be found in the master thesis of the ﬁrst author [Bernreiter, 2020]. Moreover, ASP encodings have been provided in [Bernreiter et al., 2020]. Regarding future work, new choice logics may be deﬁned explicitly with concrete use cases in mind. Furthermore, some properties of our framework have yet to be investigated. This includes a characterization of associativity, general concepts towards normal forms (as examined for QCL and CCL in [Brewka et al., 2004a; Boudjelida and Benferhat, 2016]) as well as nonmonotonic consequence relations for choice logics and how they can ﬁt into the framework of [Kraus et al., 1990] (examined for QCL in [Brewka et al., 2004a]). Investigating the computational complexity of these nonmonotonic consequence relations in a general manner may also yield interesting results. Furthermore, the complexity of checking for strong equivalence is still unknown for choice logics that are neither optionality-ignoring nor optionality-differentiating.

Acknowledgments

We thank the anonymous reviewers for their valuable feedback. This work was funded by the Austrian Science Fund (FWF) under the grants Y698 and P31890.

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)

References [Benferhat and Sedki, 2008a] Salem Benferhat and Karima Sedki. Alert correlation based on a logical handling of administrator preferences and knowledge. In Eduardo Fern andez-Medina, Manu Malek, and Javier Hernando, editors, SECRYPT 2008, Proceedings of the International Conference on Security and Cryptography, Porto, Portugal, July 26-29, 2008, pages 50 56. INSTICC Press, 2008. [Benferhat and Sedki, 2008b] Salem Benferhat and Karima Sedki. Two alternatives for handling preferences in qualitative choice logic. Fuzzy Sets Syst., 159(15):1889 1912, 2008. [Bernreiter et al., 2020] Michael Bernreiter, Jan Maly, and Stefan Woltran. Encoding choice logics in ASP. In Proceedings of the 13th Workshop on Answer Set Programming and Other Computing Paradigms, afﬁliated with the 36th International Conference on Logic Programming, University of Calabria, Rende, Italy September 18-24, 2020, 2020. [Bernreiter, 2020] Michael Bernreiter. A general framework for choice logics. Master s thesis, TU Wien, 2020. [Bienvenu et al., 2010] Meghyn Bienvenu, J erˆome Lang, and Nic Wilson. From preference logics to preference languages, and back. In Fangzhen Lin, Ulrike Sattler, and Miroslaw Truszczynski, editors, Principles of Knowledge Representation and Reasoning: Proceedings of the Twelfth International Conference, KR 2010, Toronto, Ontario, Canada, May 9-13, 2010, pages 414 424. AAAI Press, 2010. [Boudjelida and Benferhat, 2016] Abdelhamid Boudjelida and Salem Benferhat. Conjunctive choice logic. In International Symposium on Artiﬁcial Intelligence and Mathematics, ISAIM 2016, Fort Lauderdale, Florida, USA, January 4-6, 2016, 2016. [Brewka et al., 2004a] Gerhard Brewka, Salem Benferhat, and Daniel Le Berre. Qualitative choice logic. Artif. Intell., 157(1-2):203 237, 2004. [Brewka et al., 2004b] Gerhard Brewka, Ilkka Niemel a, and Tommi Syrj anen. Logic programs with ordered disjunction. Comput. Intell., 20(2):335 357, 2004. [Charalambidis et al., 2020] Angelos Charalambidis, Giorgos Papadimitriou, Panos Rondogiannis, and Antonis Troumpoukis. Lexicographic logic: a many-valued logic for preference representation. Co RR, abs/2012.10940, 2020. [Creignou et al., 2018] Nadia Creignou, Reinhard Pichler, and Stefan Woltran. Do hard SAT-related reasoning tasks become easier in the krom fragment? Log. Methods Comput. Sci., 14(4), 2018. [Domshlak et al., 2011] Carmel Domshlak, Eyke H ullermeier, Souhila Kaci, and Henri Prade. Preferences in AI: an overview. Artif. Intell., 175(7-8):1037 1052, 2011. [Faber et al., 2013] Wolfgang Faber, Miroslaw Truszczynski, and Stefan Woltran. Abstract preference frameworks

- a unifying perspective on separability and strong equivalence. In Marie des Jardins and Michael L. Littman, editors, Proceedings of the Twenty-Seventh AAAI Conference on Artiﬁcial Intelligence, July 14-18, 2013, Bellevue, Washington, USA, pages 297 303. AAAI Press, 2013. [Gottwald, 2001] Siegfried Gottwald. A Treatise on Many Valued Logics, volume 3. Baldock: research studies press, 2001. [Jiang et al., 2015] Guifei Jiang, Dongmo Zhang, Laurent Perrussel, and Heng Zhang. A logic for collective choice. In Gerhard Weiss, Pinar Yolum, Rafael H. Bordini, and Edith Elkind, editors, Proceedings of the 2015 International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2015, Istanbul, Turkey, May 4-8, 2015, pages 979 987. ACM, 2015. [Kraus et al., 1990] Sarit Kraus, Daniel Lehmann, and Menachem Magidor. Nonmonotonic reasoning, preferential models and cumulative logics. Artif. Intell., 44(1-2):167 207, 1990. [Lang, 2004] J erˆome Lang. Logical preference representation and combinatorial vote. Ann. Math. Artif. Intell., 42(13):37 71, 2004. [Lietard et al., 2014] Ludovic Lietard, Allel Hadjali, and Daniel Rocacher. Towards a gradual QCL model for database querying. In Anne Laurent, Olivier Strauss, Bernadette Bouchon-Meunier, and Ronald R. Yager, editors, Information Processing and Management of Uncertainty in Knowledge-Based Systems - 15th International Conference, IPMU 2014, Montpellier, France, July 15-19, 2014, Proceedings, Part III, volume 444 of Communications in Computer and Information Science, pages 130 139. Springer, 2014. [Pigozzi et al., 2016] Gabriella Pigozzi, Alexis Tsouki as, and Paolo Viappiani. Preferences in artiﬁcial intelligence. Ann. Math. Artif. Intell., 77(3-4):361 401, 2016. [Shoham, 1987] Yoav Shoham. Nonmonotonic logics: Meaning and utility. In John P. Mc Dermott, editor, Proceedings of the 10th International Joint Conference on Artiﬁcial Intelligence. Milan, Italy, August 23-28, 1987, pages 388 393. Morgan Kaufmann, 1987. [van Benthem et al., 2009] Johan van Benthem, Patrick Girard, and Olivier Roy. Everything else being equal: A modal logic for Ceteris Paribus preferences. J. Philos. Log., 38(1):83 125, 2009. [von Wright, 1963] Georg Henrik von Wright. The Logic of Preference. Edinburgh University Press, 1963. [Zhang and Thielscher, 2015] Dongmo Zhang and Michael Thielscher. Representing and reasoning about game strategies. J. Philos. Log., 44(2):203 236, 2015.

Proceedings of the Thirtieth International Joint Conference on Artiﬁcial Intelligence (IJCAI-21)