Soft constraints play a major role in AI, since they allow to restrict the set of possible worlds (obtained from hard constraints) to a small fraction of preferred or most plausible states. Only a few formalisms fully integrate soft and hard constraints. A prominent example is Qualitative Choice Logic (QCL), where propositional logic is augmented by a dedicated connective and preferred models are discriminated via acceptance degress determined by this connective. In this work, we follow an analogous approach in terms of syntax but propose an alternative semantics. The key idea is to assign to formulas a set of models plus a partial relation on these models. Preferred models are then obtained from this partial relation. We investigate properties of our logic which demonstrate that our semantics shows some favorable behavior compared to QCL. Moreover, we provide a partial complexity analysis of our logic.
One major problem for handling preferences or soft constraints is often the sheer
amount of alternatives. This makes the representation of preferences as an order
relation on the set of alternatives impractical in many applications. Languages
that represent preferences succinctly help to circumvent this problem, e.g.
CPNets (introduced in [
It is thus a natural, yet challenging, approach to apply preferences without
explicitly materializing the set of all alternatives. Indeed, many logical languages
in the area of knowledge representation propose an integration of hard and soft
constraints, see e.g. [
Our logic relies on a simple idea for the semantics, where every formula is not only assigned a set of models but also a partial relation on these models. The main aim of the paper is to evaluate our approach along the following axes of desired properties: 1. Extending propositional logic: Formulas without speci ed preference should behave like propositional formulas. 2. Rules of propositional logic: As many rules of propositional logic such as associativity and distributivity as possible should hold in the logic. 3. Expressiveness: Every partial order on every set of models should be expressible. 4. Simulate QCL on "basic choice formulas": Basic choice formulas are a fragment of QCL that behaves very naturally, hence our logic should be equivalent to QCL on this fragment. 5. Good computational properties: The complexity of problems like checking whether a model is preferred to another should remain on a complexity level comparable to similar problems in propositional logic.
As we will show, the rst, third and fourth requirements are fully satis ed by our logic. Concerning the second property, we show that many important rules of classical logic hold in our logic as well, but some don't. The fth property is still open as we only have preliminary results on the complexity of our logic.
The rest of the paper is structured roughly around these properties. The next section introduces the logic and discusses its de nition; as we will see the rst property follows directly from the de nition. Section 4 discusses equivalence of formulas in our logic and shows which rules of propositional logic are satis ed by our logic. We then proceed with the expressiveness of our logic addressing the third property from the above list. Section 5 then is concerned with the relation between our logic and QCL. Finally, Section 6 presents some partial results on the complexity of our logic.
Previous and Related Work. In the past, several preference logics were
proposed. Perhaps the most in uential work in this area is von Wright's paper
\The logic of preferences" [
Syntax. Syntactically, our logic is propositional logic with the connectives ^, _ and : extended by an additional connective .
De nition 1 The set PF (V ) of formulas of preference logic over a set of variables V is de ned recursively as: { v 2 PF (V ) for all v 2 V . { (A ^ B) 2 PF (V ) if A; B 2 PF (V ). { (A _ B) 2 PF (V ) if A; B 2 PF (V ). { (:A) 2 PF (V ) if A 2 PF (V ).
{ (A B) 2 PF (V ) if A; B 2 PF (V ).
For every V , we de ne ? = A ^ :A for some xed A 2 PF (V ) and > = :?.
The intended meaning of A B is A or B but preferably A. Therefore, from the perspective of truth A B is equivalent to A _ B.
De nition 2 Assume A 2 PF (V ). Then the propositional projection of A, denoted prop(A), is the propositional formula obtained from replacing every occurrence of in A with _.
Semantics. The semantics of our logic relies on two constituents, one related to truth and one related to preferences. The former is given by the classical evaluation of the propositional projection of the formula.
De nition 3 Let A 2 PF (V ). We call a set M V a model of A and write M j= A if it is a model of prop(A). MA denotes the set of all models of A.
Preferences, on the other hand, are represented by a relation between models. Let A 2 PF (V ) and M; N 2 MA. We de ne a relation RA on MA and write M A N if M is preferred to N for A. As usual, we write M >A N for M A N and not M A N as well as M =A N for M A N and M A N . The de nition of RA is based inductively on the relations of the subformulas of A and depends on the form of A. In the following we introduce and discuss the de nition for every type of formula separately. For atomic formulas, there is no reason to prefer any model over any other model.
De nition 4 RA = ; for A = v with v 2 V .
For A = :B, we observe that, in general, RB contains no information on the models of :B. For example, for B = ((a ^ c) (b ^ c)), it seems impossible to us, to use any preferences between the models fa; cg; fa; b; cg; fb; cg of B to justify any preferences between the models fag; fbg; fa; bg; fcg; ; of A. To circumvent this problem, we use the rather crude method of erasing all preferences. De nition 5 RA = ; for A = :B.
In practice, this is equivalent to using positive and negative literals instead of :. We chose the presented de nition, among other reasons, in order to follow the same intuition as QCL.
One of the major questions for formulas of the form A = B C for 2 f^; _; g is, how to deal with con icting preferences in RB and RC . In the case A = B C, we can use the additional information that the subformula B is "more important" than C. Hence, the preferences of B should "overwrite" the preferences of C. The preferences of C are only considered for models M and N if both do not satisfy B. Additionally, we, of course, need to add new preferences that codify that B is preferred to C.
De nition 6 For A = B
C, M
A N if: { M B N ; { M; N 2= MB and M C N ; { M 2 MB and N 2= MB.
In the other two cases, where both subformulas are equally important, there are two approaches to dealing with con icting preferences. The rst approach is combining the preferences of both subformulas. Intuitively, this means that if there is a reason to prefer M over N in one of the subformulas of A, then M is preferred to N in A. We believe that this is the correct notion for formulas of the form A = B ^ C.
De nition 7 For A = B ^ C, M
A N if: { M B N or M C N ; { there exists N 0 2 MA, such that M A N 0
A N ;
The second approach is to demand that both subformuals agree in their preference and ignoring inconclusive preferences. This approach appears to be a natural t for formulas of the form A = B _ C. We additionally have to treat the case that M is preferred to N in one of the subformulas, say B, but at least one of the two models does not satisfy C. In this case, we keep the preference of from B unless M does not model C but N does, as this can be seen as a preference of N over M for C.
De nition 8 For A = B _ C, M
A N if: { Either M >B N and M >C N holds or M =B N and M =C N holds. { Either N 62 MB and M C N holds or N 62 MC and M B N holds. Example 9 Let A = (a b) ^ (b a) over V = fa; bg. We have MA = ffa; bg; fag; fbgg and fa; bg >A fag, fa; bg >A fbg, and fag =A fbg. For B = (a b) _ (b a), we have MB = MA but RB is empty.
It is possible to use the rst approach for _ and the second one for ^. The resulting "strong or" and "weak and" are expressible in our language as we will see in Section 4. This concludes the de nition of RA. De nition 10 We call (MA; RA) the evaluation of A. We say that two formulas A; B are equivalent, in symbols A B, if (MA; RA) = (MB; RB).
We observe that the evaluation of ? = A ^ :A is given by (;; ;) and for > = :? we have as an evalution (2V ; ;). Furthermore, we observe that for any A, that (A _ ?) yields the same evaluation as A, while (A _ >) yields the same evaluation as >.
Another issue is the explicit transitivity in De nition 7. Otherwise, for example, A = (c _ (a b)) ^ (a _ (b c)) would lead to a non transitive relation containing a A b and b A c but not a A c. We next show that RA is indeed transitive, even though we only explicitly speci ed this for conjunction. Proposition 11 Let A be a formula and M; N; O 2 MA. Then M N A O implies M A O.
A N and Proof. We prove the claim by an induction on the formula complexity of A: The cases A = ai, A = B ^ C and A = :B are clear.
Now assume A = B _ C. First assume M; N; O j= B ^ C. Then we know M B N B O and M C N C O and hence by induction M B O and M C O. Obviously either M >B O or M =B O holds. Observe that M >B O holds if and only if M >B N or N >B O holds. We assume M >B N . Then M A N can only be true if M >C N holds. Hence M >C O and therefore M A O holds. On the other hand M =B O implies M =C O by a symmetric argument and hence also M A O. Now assume O 6j= B. Then N C O must hold. Furthermore, because N must be a model of C, we know that M C N must hold. Therefore, by induction, M C O, which implies M A O, because O 6j= B. Observe that N 6j= B and N A O imply O 6j= B and hence M A O by the argument above. Furthermore M 6j= B and M A N imply N 6j= B, hence again M A O. The remaing cases, O 6j= C, N 6j= C and M 6j= C are symmetric.
Finally, assume A = B C. If M B N B O or M; N; O 2 MC n MB and M C N C O we get M A O by induction. Observe that the only remaing possible cases are either M B N and O 2 MC n MB or M 2 MB, N; O 2 MC n MB and N B O. In both cases we know M 2 MB and O 2 MC n MB, hence M A O.
In general, the relation A is not re exive, hence it is not a partial order. It would be possible to change this, by de ning M =A M for all M 2 MA. From a technical standpoint, the resulting logic is nearly equivalent and basically all results in this paper would carry over to this logic. (Obviously, the results on expressiveness would change a bit, as only re exive relations could be expressed.) However, adding re exiveness would complicate notation in some places, therefore we omitted it from the de nition.
The main aim of the relation RA is to determine preferred models. We de ne them next.
De nition 12 Let A 2 PF (V ). We say that a model M 2 MA is a most preferred model of A if there is no N 2 MA such that N >A M . We write pref (A) for the set of most preferred models of A.
Two important concepts of equivalence of formulas are semantic equivalence and replacement equivalence. These two concepts coincide for propositional logic, but typically are distinct concepts in logics which are concerned with preferences. We show that the two concepts are closely related for our logic.
Replacements are denoted via C[A=B], which stands for the formula obtained from C by replacing an occurrence of A by B.
De nition 13 We say two formulas A; B 2 PF (V ) are replacement prefequivalent if for all C 2 PF (V ), pref (C[A=B]) = pref (C).
Theorem 14 A; B 2 PF (V ) are replacement equivalent i A B.
Proof. A B, i.e. (MA; RA) = (MB; RB), implies replacement pref-equivalence between A and B because the evaluation of a formula only depends on the evaluation of its subformulas and not on their syntax. So assume there are replacement pref-equivalent formulas A and B but (MA; RA) 6= (MB; RB). First assume MA 6= MB. Then, without loss of generality, there is a model M 2 MA such that M 62 MB holds. Consider the formula DM = Vv2M v ^ Vv2V nM :v. Now let C = A^DM . Then MC = fM g and MC(A=B) = ;. Hence, pref (C) = ffM gg and pref (C[A=B]) = ;. Now assume MA = MB and RA 6= RB. Wlog, there is (M; N ) 2 RA and (M; N ) 62 RB. For C = A ^ (DN DM ) (with DM , DN as used above), we get pref (C[A=B]) = ffN gg while pref (C) = ffM; N gg.
In what follows, we explore which rules of equivalence from propositional logic hold in our logic. Before analysing several rules, we provide a di erent characterization for RA in order to ease proofs. For sets X and Y we shall write X Y for X \ Y ; however, we use X Y also as short hand for X \ (Y Y ) when clear from the context. Furthermore, for a set of tuples X we write Xr for the reverse set, i.e. Xr := f(b; a) j (a; b) 2 Xg. We write X4Y for the symmetric di erence of X and Y , i.e X4Y := (X [ Y ) n (X \ Y ). Finally, we write trcl (R) for the transitive closure of a relation R.
Proposition 15 Let A; B; C 2 PF (V ), v 2 V . Then, the following holds: { If A = v or A = :B, then RA = ;. { If A = B ^ C, then RA = trcl (RB [ RC ) . { If A = B _ C, then RA = ((RB \ RC ) n (MRABr4RCr )) [ RB MA MBnMC [
{ If A = B C, then RA = RB [ RC MBnMA [ MB (MC n MB) .
Proof. We prove this by an induction on the formula complexity of a formula A: The cases A = v and A = :B are clear.
Assume A = B ^ C. It is clear that (M; N ) 2 (RB [ RC ) i M; N j= B, MA M; N j= C and (M; N ) 2 RB or (M; N ) 2 RC holds. Transitive closure of RA follows by de ntion of the semantics for conjunction cf. De nition 7. ?
Now assume A = B _ C. First observe that (M; N ) 2 (RB \ RC ) n (RAr4RBr) is equivalent to (M; N ) 2 RB, (M; N ) 2 RC and (N; M ) either in RB and RC or in neither. By induction, this is equivalent to M =B N and M =C N in the rst case and equivalent to M >B N and M >C N in the second. Now observe that (M; N ) 2 RB MA MBnMC holds if and only if N 6j= C and M B N . Finally, (M; N ) 2 RC MA MCnMB i N 6j= B and M C N .
Finally, assume A = B C. By induction (M; N ) 2 RB i M B N . (M; N ) 2 RC MCnMB i M; N 6j= B and M C N . Finally, (M; N ) 2 (MB (MC n MB)) i M j= B and N 6j= C.
Many classical rules of equivalence hold also for our preference logic.
Proof. For all A B in table 1, MA = MB follows easily from the rules of propositional logic. We show three of the >; ?-rules. First observe RA^> = trcl (RA [ ;) MA = RA. Then RA_? = RA MAn; [; ;nMA [(RA \;)n(RAr4;) = RA. And nally RA_> = RA MAn2V [ ; 2V [ (RA \ ;) n (RAr4;) = R> = ;. De Morgan's law and triple negation follow immediately from the de nition of : and the fact that they hold in classical logic. Commutativity is also clear by de nition. We show the associativity of :
R(A B) C = (RA [ RB MBnMA [ (MA (MB n MA)))[ RC MCn(MA[MB) [ ((MA [ MB)
(MC n (MA [ MB))) =
(MB n MA)) [ ((MA [ MB) (MC n (MA [ MB))) =
(MC n (MA [ MB)))[ (MA
((MB [ MC ) n MA)) = RA [ (RB [ RC MCnMB [ (MB
(MC n MB))) (MB[MC)nMA [ (MA ((MB [ MC ) n MA)) = RA (B C) Associativity of _ and the absorption rules can be shown similarly.
However, a few important rules from classical logic do not hold. Obviously double negation, i.e. ::A A is not true. Furthermore ^ is not associative. For example for A = :b ^ ((b a) ^ (a b)) we have (fag; fag) 2 RA but for B = (:b ^ (b a)) ^ (a b) we have RB = ;. For absorption, we have a _ (a ^ b) 6 a, a ^ (b a) 6 a and (a ^ b) a 6 a. Finally, the distribution law does not hold. For example A = a _ ((a b) ^ (b a)) implies (b; b) 2 RA but B = (a _ (a b)) ^ (a _ (b a)) implies (b; b) 62 RB.1 4
We want to show that every transitive relation on any set of models can be represented by our logic. As a helpful tool for this proof, we introduce two new connectives, the \strong or" and the \weak and" mentioned earlier. These are not necessary, as they can be expressed through the other connectives, but are useful short hands.
De nition 17 For formulas A and B we write A + B for (A _ (:A ^ B)) ^ (B _ (:B ^ A)) and A u B for (A _ B) ^ :(A ^ :B) ^ :(:A ^ B).
Proposition 18 A + B is evaluated as (MA [ MB; trcl (RA [ RB)) and A u B is evaluated as (MA \ MB; (RA \ RB) n (RAr4RBr)).
Proof. This is shown by an easy computation. In fact, MA+B = MA [ MB and MAuB = MA \ MB follows from classical logic.
For A + B we have
RA+B = trcl ((RA_(:A^B) [ RB_(:B^A)) MA[MB ); where RA_(:A^B) = (RA \ R:A^B) n (RAr4R:A^B) [ RA MA_(:A^B) MAnM:A^B [ r
R:A^B MA_(:A^B) M:A^BnMA Observe that MA_(:A^B) is a superset of MA and MA n M:A_B is MA. Hence RA MA_(:A^B) MAnM:A^B is (a super set of) RA MA , which is just RA. Furthermore, every tuple in RA_(:A^B) is either from RA or RB because R:A = ;. Therefore RA RA_(:A^B) RA [ RB holds. By symmetry also, RB RB_(:B^A) RA [ RB holds. Hence,
RA [ RB
RA_(:A^B) [ RB_(:B^A) and therefore RA+B = trcl (RA [ RB). 1 It is also possible to construct a (more complicated) counter example if we assume that the relation is always re exive For A u B we have
RAuB = trcl(RA_B [ R:(A^:B) [ R:(:A^B)) MA\MB = trcl(RA_B [ ; [ ;) MA\MB = trcl((RA \ RB) n (RAr4RBr) [ RA MA[MB MAnMB [
)
MA\MB = (RA \ RB) n (RAr4RBr) This concludes the proof.
We even prove that every relation can be represented with a special kind of formula, a formula without nested preferences: De nition 19 We say a formula A is a formula without nested preferences if for every subformula B C of A, does neither occur in B nor in C. Theorem 20 Let be a transitive relation on M P(V ), a set of models. Then, there exists a formula without nested preferences over the variables V that is evaluated to (M; ).
Proof. Say M1 M2 holds for M1; M2 2 M. We already used formulas DM1 and DM2 which have only M1 resp. M2 as a model in the proof of theorem 14. Then DM1 DM2 is evaluated as (fM1; M2g; f(M1; M2)g) and we say DM1 DM2 expresses M1 M2. Now let D1; : : : ; Dn for n = j j be formulas expressing all preferences in . Then D1 + + Dn + DM1 + + DMm for m = jM j is evaluated as (M; ). 5
We brie y review the main de nition for qualitative choice logic (QCL)
following [
De nition 21 The optionality of a formula A is given as folllows { opt (A) = 1 if A is an atom or of form :B; { opt (A) = max (opt (B); opt (C)) if A = B { opt (A) = opt (B) + opt (C) if A = B C. De nition 22 Let A be a formula and M 2 MA. The degree i of satisfaction (j=i) of A in M is de ned as { M j=1 A if A is an atom or of form :B; { for A = B ^ C: M j=k A i M j=m B, M j=n C and k = max (m; n) { for A = B _ C: M j=k A if
M j=k B and for no j < k: M j=j C, or
M j=k C and for no j < k: M j=j B; { for A = B C: M j=k A if M j=k B or (M j=1 :B, M j=m C, and k = m + opt (A)).
We can now de ne preferred models in QCL as follows.
De nition 23 An interpretation M is a preferred QCL model of a formula A if M 2 MA, M j=k A and there is no N such that N j=m A with m < k. We denote the set of QCL-preferred models of a formula A by pref QCL(A).
As we will see below the preferred models of QCL and our logic coincide on certain fragments. They are not equivalent, in general. In fact, this is on purpose, since, as we show next, QCL behaves unintuitively in certain cases. This is due to the quite syntactic-driven notion of satisfaction degrees.
Example 24 In QCL, there exist formulas A and B such that pref QCL(A) 6= pref QCL(A[B=B B]), i.e. in contrast to our logic, QCL does not account for neutrality w.r.t. the preferential connective. In fact, take A = ((a b)_(a c))^ :a and A0 obtained from A by replacing the rst occurrence of a in A by a a. First observe that MA = MA0 = ffbg; fcg; fb; cgg. For each M 2 MA we have M j=2 A, and thus each M 2 MA is a preferred QCL model of A. However, for A0 we observe that fbg j=3 A0 while fb; cg j=2 A0 and fcg j=2 A0. Thus only fb; cg and fcg are preferred QCL models of A0. Hence, pref QCL(A) 6= pref QCL(A0).
In order to clarify the relation between our logic and QCL, let us de ne certain normal forms.
{ Conjunctive Form if A is build of classical formulas, :; ^ and { Disjunctive Form if A is build of classical formulas, :; _ and { Normal Form if A is build of classical formulas and .
Formulas in Normal Form are called basic choice formulas in QCL. Theorem 26 Let M and N be models of a formula A in Conjunctive Form, such that M j=m A and N j=n A Then, m n implies M A N . Proof. We prove the result by induction on the formula complexity. If A is a classical formula or :B for some formula B the result is clear because every model has satisfaction degree 1.
Assume A = B ^ C for formulas B; C. If M has smaller satisfaction degree than N then the satisfaction degree of M is smaller than the satisfaction degree of N for either B or C, hence by induction N B M , resp. N C M . Therefore N A M .
Finally, assume A = B C for formulas B and C. We distinguish three cases: (1) if M and N are both models of B the satisfaction degrees of M and N are the same for A and B, hence, by induction M B N holds, therefore also M A N . (2) if M and N are both a model of C but not of B, the satisfaction degrees of M and N with respect to A only di ers in a constant from the satisfaction degrees with respect to C, hence, by induction, M A N . (3) if M is a model of B and N is not a model of B, we have M A N by de nition.
For formulas in Disjunctive Form, the relation between satisfaction degrees and the relational structure in our logic is the other way around. Theorem 27 Let M and N be models of a formula A in Disjunctive Form, such that M j=m A and N j=n A Then, M >A N implies m > n.
Proof. We prove the result by induction on the formula complexity. If A is a classical formula or :B for some formula B, the result is clear because RA = ;.
Assume A = B _ C for formulas B; C. There are three cases in which M is strictly preferred to N . First, M is strictly preferred to N for both B and C. Then the satisfaction degree of M is smaller than the satisfaction degree of N for both B or C by induction, hence also for A. Second, M and N are both models of B but N is not a model of C and M is preferred to N for B. Then, we know by induction that the satisfaction degree of M is smaller than the satisfaction degree of N for B and the satisfaction degree of N is in nity for C. The third case is symmetric to the second case.
Finally, assume A = B C for formulas B and C. We distinguish three cases: First, if M and N are both models of B then M >A N if and only if M >B N but as the satisfaction degrees of M and N are the same for A and B we know by induction that the satisfaction degree of M is smaller than the one of N . If M and N are both a model of C but not of B, then M >A N i M >C N but as the satisfaction degrees of M and N with respect to A only di ers in a constant from the satisfaction degrees with respect to C, we can apply induction again. Finally, if M is a model of B and N is not a model of B, we know that the satisfaction degree of M is smaller than the one of N by de nition. Corollary 28 Let M and N be models of a formula A in Normal Form, such that M j=m A and N j=n A Then, M A N i m n.
The following example further illustrates the di erence between QCL and our logic.
Example 29 First we observe that formulas (a b) _ (b a) and (a b) ^ (b a) are equally evaluated in QCL and our logic. Both deliver all models, f g f g a , b and fa; bg, as preferred models for both formulas, re ecting the fact that the preferences in the formula are cyclic.
On the other hand, let = (a ^ :b) (a ^ b) (:a ^ b) and = (:a ^ b) (a ^ b) (a ^ :b). Then the QCL-preferred model of ^ is fa; bg, while _ delivers two QCL-preferred models fag and fbg. Our logic takes a di erent view and combines the implictly obtained relations fag > fa; bg > fbg and fbg > fa; bg > fag. In fact, we have as preferred models for ^ , fa; bg, fag and fbg, re ecting that the relation becomes cyclic. For _ , we obtain the same preferred models, however for a di erent reason, namely that no relation appears in both subformulas. while QCL again delivers fag and fbg. 6
The basic computational problems in our logic are model checking, satis ability and testing if one model is preferred to another. By the de nition of truth in our logic, the rst two problems have the same complexity in our logic as in propositional logic, i.e. model checking is in P and satis ability is NP-complete. The complexity of the model preference problem, on the other hand, is still open. Problem 1 (Model preference) Let A 2 PF (V ) and let M and N be models of A. Does M A N hold?
While we do not know the complexity of the model preference problem on arbitrary preference formulas, we know the complexity for the fragments introduced in section 5.
Proposition 30 The model preference problem is in P for formulas in Disjunctive From.
Proof. By de nition, the relation between M and N does not depend on the relation between any other models for formulas in Disjunctive Form. Hence, we can easily track the relation between the models M and N in a bottom up manner through the syntax tree.
Observe that every formula in Normal Form is also in Disjunctive Form, hence the model preference problem for formulas in Normal Form is also in P. The model preference problem for formulas in Conjunctive From, on the other hand, is harder, because we have to compute the transitive closure of the relation in the ^ step. Indeed, this problem is NP-complete. We need a lemma and an additional de nition to prove this.
De nition 31 Let A 2 PF (V ) and let (M; N ) be a preference introduced by a subformula D = B C or D = B ^ C (via transitivity). We say the preference survives until A if there is no subformula E of A containing D such that { E = :F { E = F _ G and (M; N ) 62 RE { E = F ^ G and (M; N ) 62 (RF \ RG) { E = F
ME
G and (M; N ) 62 RF [ RG MGnMF Lemma 32 Let A be a formula in Conjunctive Form, such that some subformula D = B C or D = B ^ C of A introduces preferences (M; N ), (M 0; N ) and (M 0; N 0). Then, if (M; N ) and (M 0; N 0) survive until A then also (M 0; N ) survives until A. Proof. Let E be the smallest subformula of A such that (M 0; N ) does not survive until E. Obviously, E = :F is not possible. Now assume E = F ^ G and D is a subformula of F . Then (M 0; N ) does not survive until E if and only if either M 0 or N is not a model of E. But the rst case contradicts the assumption that (M 0; N 0) survives and the second case contradicts the assumption that (M; N ) survives. Now assume E = F G and D is a subformula of F . Then (M 0; N 0) survives until E if it survives until F which is does by choice of E. Finally, assume E = G F and D is a subformula of F . Then (M 0; N ) does not survive until E if and only if either M 0 or N is a model of G. However this leads to a contradiction as in the ^ case.
Proposition 33 The model preference problem is in NP for formulas in Conjunctive Form.
Proof. Let A 2 PF (V ) and let M; N be models of A. We enumerate all and ^ occurring in A as i and ^i and write Ai i Bi and Ai ^i Bi for the respective subformulas in A. Then, for every triple ( i; ^j ; k) we guess a sequence 1; N1; 2; N2; : : : ; Nn; n, for n = jAj4, where for every l n, Nl is a model and l is either i for some i or a triple ( i; ^j ; k). Furthermore, 1 is either i or a triple containing i as the rst element. Analogously, n is either k or a triple containing k is the last position.
Now, we label every triple either valid or unvalid in an order such that when we label a triple ( i; ^j ; k), we already labeled all triples containing ^m for all ^m contained in Aj ^j Bj . First, we verify, that i; k and all o and ^m occurring in the sequence guessed for the triple, are contained in Aj ^j Bj . If not, we label the triple unvalid. Otherwise, we check for every pair of models (Nl; Nl+1) if it is valid for its operator l+1. This is done in the following way:
If l+1 = o, we check if Nl j= Ao. Nl+1 6j= Ao and Nl+1 j= Bo, i.e. if Nl Ao oBo Nl+1. If no, the pair is not valid. If yes, we check if the preference survives until Aj ^j Bj and Nl Aj^jBj Nl+1 holds. Observe that this is a ptime check. If no, the pair is unvalid, if yes, the pair is valid.
So now assume l+1 = ( m; ^n; o). First, we check if the triple is valid. If no, the pair is unvalid. Otherwise, let 1; N1 ; 2; N2 ; : : : ; Nn ; n be the sequence guessed for ( m; ^n; o). If 1 = p, we check if Nl p N1 was introduced by Ap p Bp and survives until An ^n Bn. If 1 = ( i ; ^j ; k), we check if the pair (Nl; N1 ) is valid for that triple. Then, we do the same checks for n and Nl+1. If all these checks are positive, the pair is valid and if all the pairs occurring in the sequence are valid, the triple ( i; ^j ; k) is valid.
Now to check if M A N , we do the following, we go through the syntax tree of A in a bottom up manner and check if the preference M D N is introduced by any subformula, and if yes, if it survives until A. For subformulas Ai i Bi, it is clear how to check, if M Ai iBi N is introduced. For Aj ^j Bj , if M; N j= Aj ^j Bj we look for every valid triple ( i ^j ; k) containing ^j we check if (M; N1) is a valid pair for 1 and if (Nn; N ) is a valid pair for n. If both checks are positive for any valid triple, M Aj^jBj N is introduced.
The correctness of this algorithm relies on the following two facts: (1) If there is a valid sequence for a triple, then there is a valid sequence for that triple that contains each triple and each i at most once. (2) Let B = Ai ^i Bi be a subformula of A and let M; N be a models of B. Finally, let 1; N1; 2; N2; : : : ; Nn; n be a valid sequence for the triple ( j ; ^i; k). If M 1 N1 is valid and there exists a second sequence 1; N1 ; 2; N2 ; : : : ; Nn ; n also valid for the triple ( j ; ^i; k) and N 1 N1 is valid, then also N 1 N1 is valid.
The rst result guarantees that it su ces to look at sequence of length less than jAj4, the second result guarantees that it su ces to guess one sequence per triple. (1) holds, because if Ni i Ni+1 i+1 : : : Nj j Nj+1 is valid and i = j then Ni i Nj+1 is also valid by the de nition of validity. (2) follows from Lemma 32.
This proof does not work for arbitrary formulas, because Lemma 32 does not hold for arbitrary formulas. Assume, for example, that A B introduces (M; N ), (M 0; N ) and (M 0; N 0), that (N; M ), (N 0; M 0) 62 RA B holds and that C is a formula such that M >C N and M 0 >C N 0 holds, but not M 0 C N .2 Then (M; N ) and (M 0; N 0) survive until (A B) _ C, but (M 0; N ) does not. Proposition 34 The model preference problem is NP-hard for formulas in Conjunctive Form.
Proof. Let A be a propositional formula. Now let x be a new variable not occurring in A. Then let B = ((A ^ :x) x) ^ (x (A ^ :x)). Obvious, B is a formula in Conjunctive Form. We claim that fxg B fxg if and only if A is satis able. First assume A is satis able and M is a model of A. Then M is also a model of A ^ :x. Therefore, M and fxg are models of C = (A ^ :x) x and M C x holds. Similarly, M and fxg are models of D = x (A ^ :x) and x D M holds. Hence x B M B x and by transitivity x B x. Now assume A is not satis able. Then A ^ :x is also not satis able. Therefore, we have MC = fM 2 2V j x 2 M g and RC = ;. Similarly, MD = MC and RD = ;. Hence RB = ;. 7
We presented a new logic for handling hard and soft constraints at once. The logic
has a straightforward semantics that assigns every formula a set of models and a
transitive relation on this set. We have shown that replacement pref-equivalence
and semantic equivalence coincide for our logic and that many desirable
equivalences known from propositional logic hold. Furthermore, we have shown that
every transitive relation on every set of models can be expressed using a formula
without nested preferences. We proved that our logic coincides with qualitative
choice logic [
In the future, we want to pinpoint the complexity of the model preference
problem for arbitrary formulas as well as the complexity of some other, related,
problems like nding a preferred model. Furthermore, we would like to compare
our logic to other formalisms from the literature like Conjunctive Choice Logic
[
This work was funded by the Austrian Science Fund (FWF) under grant number Y698.