=Paper=
{{Paper
|id=Vol-2678/paper1
|storemode=property
|title=
|pdfUrl=https://ceur-ws.org/Vol-2678/paper1.pdf
|volume=Vol-2678
|authors=Michael Bernreiter,Jan Maly,Stefan Woltran
|dblpUrl=https://dblp.org/rec/conf/iclp/BernreiterMW20
}}
====
https://ceur-ws.org/Vol-2678/paper1.pdf
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