Choice Logics and Their Computational Properties

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 simplification, 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 specifically, interpretations ascribe a number, called satisfaction degree, to QCL- and 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 fine-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 defined, 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 define 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 define a framework that captures both QCL and CCL, as well as infinitely 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 NP- to ∆2P-completeness with QCL and CCL being located in between (Θ2P-complete).

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

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 infinite-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 fit 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 defined in this framework, and finally 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 defined as a set of propositional variables such that a ∈ I if and only if a is set to true by I. If I satisfies 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.

Definition 1. The set of choice connectives CL of a choice logic L is a finite set of symbols such that CL∩{¬, ∧, ∨} = ∅. The set FL of formulas of L is defined 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 finite satisfaction degree that this formula can be ascribed.

Definition 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 optL : FL → N with

1. optL(a) = 1, for every a ∈ U;
2. optL(¬F) = 1;
3. optL(F ∧G) = max(optL(F), optL(G));
4. optL(F ∨G) = max(optL(F), optL(G));

The optionality of a classical formula is always 1. For any choice connective ◦, the optionality of F ◦G is bounded such that optL(F ◦G) ≤ (optL(F)+1) · (optL(G)+1). The reason for this is that there are optL(F) many finite degrees that could be ascribed to F, plus the infinite degree ∞. Likewise for G. Thus, there are at most (optL(F)+1) · (optL(G)+1) possibilities when combining the degrees of F and G.

Next, we define the satisfaction degree of a formula. In the following, we write N for (N ∪ {∞}).

Definition 3. The satisfaction degree of a choice connective ◦ ∈ CL in a choice logic L is given by a function deg ◦L : N2 ×N2 →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 degL : 2U × FL → N with

1. degL(I, F ∧G) = max(degL(I, F), degL(I,G));
2. degL(I, F ∨G) = min(degL(I, F), degL(I,G));
3. degL(I, F ◦ G) = deg ◦L(k, ℓ,m, n) for every ◦ ∈ CL, where k = optL(F), ℓ = optL(G), m = degL(I, F), and n = degL(I, G).

We also write I |=Lm F for degL(I, F) = m. If m < ∞, we say that I satisfies F (to a finite degree), and if m = ∞, then I does not satisfy F. If F is a classical formula, then I |=L1 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 optL(⊤) = optL(⊥) = 1, degL(I, ⊤) = 1 and degL(I, ⊥) = ∞ for any interpretation I in every choice logic.

The semantics of the classical connectives are fixed 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 satisfied. Conversely, we use the minimum degree for F ∨ G since satisfying either option suffices, and we do not need to concern ourselves with the less preferable option. Observe that it is still necessary to define optL(F ∨ G) = max(optL(F), optL(G)), as the case that either option is not satisfied has to be allowed for. As for negation, note that ¬F can only assume the degrees 1 or ∞. In order to define a form of negation that results in different degrees of satisfaction, we would need to keep track of degrees of dissatisfaction. We 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 Definitions 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 degL(I, F) ≤ optL(F) or degL(I, F) = ∞.

Moreover, note that only those variables that actually occur in a formula F can influence optL(F) and degL(I, F), which means that we can assume I ⊆ var(F) for any interpretation I that we are dealing with.

An interpretation that satisfies a formula to a finite degree will be referred to as a model of that formula. But often we are interested only in the most preferable models.

Definition 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 degL(I, F) ̸= ∞ and, for all other interpretations J , degL(I, F ) ≤ degL(J , F ).

By the above definition, Prf L(F) = ∅ if and only if degL(I, F) = ∞ for all interpretations I.

2.2 Examples of Choice Logics

To define a choice logic L, it suffices 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:

Definition 5. QCL is the choice logic such that CQCL = { #� ×}, and, if k = optQCL(F), ℓ = optQCL(G), m = degQCL(I, F), and n = degQCL(I,G) for some F, G, I, then

Here, we can see how optionality is used to penalize non-satisfaction: if F is satisfied, then degQCL(I, F #� ×G) = degQCL(I, F) ≤ optL(F); if F is not satisfied, but G is, then deg QCL(I , F #� ×G) = degQCL(I, G) + optL(F) > optL(F). Thus, any interpretation which satisfies 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).

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

Definition 6. CCL is the choice logic such that CCCL = { #� ⊙}, and, if k = optCCL(F), ℓ = optCCL(G), m = degCCL(I, F), and n = degCCL(I,G) for some F, G, I, then

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 define 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 fine-grained manner.

Definition 7. LCL is the choice logic such that CLCL = { #� ⋄ }, and, if k = optLCL(F), ℓ = optLCL(G), m = degLCL(I, F), and n = degLCL(I,G) for some F, G, I, then

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)).

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

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 define a choice logic that does not use optionality. We call the following new logic Simple Conjunctive Choice Logic (SCCL).

Definition 8. SCCL is the choice logic such that CSCCL = { #� ⊛}, and, if k = optSCCL(F), m = degSCCL(I, F), and n = degSCCL(I,G) for some F, G, I, then

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 define #� × 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 first 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 definition 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 defined 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:

Definition 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 degL(I, F) = m. By DL we denote the set of all degrees obtainable in a choice logic L.

Proposition 1. Let L be a choice logic. Let V be a finite 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 , degL(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 degL(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 degL(J , SJ ) = degL(J ∗ ,H) = s(J). Now, F = ∨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.

Definition 10. Two formulas A and B of a choice logic L are strongly equivalent, written as A ≡Ls B, if Prf L(F) = Prf L(F [A/B]) for all L-formulas F .

Strong equivalence is a crucial notion towards simplification, thus a characterization that avoids going through infinitely many formulas is needed. We show that strong equivalence often can be decided via simpler equivalence notions.

Definition 11. Two formulas A and B of a choice logic L are degree-equivalent, written as A ≡Ld B, if degL(I,A) = degL(I,B) for all interpretations I.

Lemma 2. Let L be a choice logic. If A ≡Ld 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].

Definition 12. Two L-formulas A and B are fully equivalent, written as A ≡Lf B, if A ≡Ld B and optL(A) = optL(B).

Lemma 3. Let L be a choice logic. Then A ≡Lf B if and only if F ≡Lf 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.

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 first 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.

Definition 13. A choice logic L is called optionality-ignoring if for all ◦ ∈ CL, degL(I, F ◦ G) = degL(I, F ′ ◦ G′ ) whenever degL(I, F) = degL(I, F ′ ) and degL(I,G) = degL(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 ≡Ls B iff A ≡Ld 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.

Definition 14. A choice logic L is called optionalitydifferentiating if for all L-formulas A and B with optL(A) ̸= optL(B), there is an L-formula F such that F ̸≡Ld 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 optQCL(A) ̸= optQCL(B). Then F = ((A ∧ ⊥) #� ×a) has the desired property: (A∧⊥) can never be satisfied, and since optQCL(A∧⊥) = optQCL(A), F is satisfied by {a} with a degree of optQCL(A) + 1. Likewise, F [A/B] is satisfied by {a} with a degree of optQCL(B) + 1.

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

Proof. The if-direction is by Proposition 4. So, let A ≡Ls B. By Proposition 4, A ≡Ld B. Towards a contradiction, assume optL(A) ̸= optL(B). Since L is optionality-differentiating, A′ ̸≡Ld 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 ≡Ls 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 optL(A) ̸= optL(B), while for all L-formulas F we have that F ≡Ld F[A/B]. This implies A ≡Ls B. But A ̸≡Lf B, since optL(A) ̸= optL(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 degree- or 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 optionality- and 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.

Definition 15. A choice logic L is called tractable if the optionality- and degree functions of every choice connective in L are polynomial-time computable.

All logics presented in this paper are tractable in this sense. The first 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 degL(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 degL(I, F) ≤ k. These two problems are straightforward generalizations of model checking and satisfiability 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.

Definition 16. We define 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 coNP 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 coNP-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 coNP in any tractable choice logic L where DL ̸= {1,∞}.

We turn to L-PREFMODELSAT and first 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 optL(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 defined 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.

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 optL(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, degL(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 ≡Lf B holds for given L-formulas A and B, as well as L-DEGREEEQUIVALENCE and LSTRONGEQUIVALENCE which are defined 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 coNP-complete; (2) L-STRONGEQUIVALENCE is coNPcomplete if L is optionality-ignoring or -differentiating.

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

5 Conclusion

We defined and investigated a general framework for choice logics that captures both QCL and CCL, but also allows to define new logics as examplified 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 definition of our framework and some further results regardings choice logics can be found in the master thesis of the first author [Bernreiter, 2020]. Moreover, ASP encodings have been provided in [Bernreiter et al., 2020].

Regarding future work, new choice logics may be defined 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 fit 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.