forked from potassco/guide
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathprefopt.tex
1322 lines (1233 loc) · 57.3 KB
/
prefopt.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
\section{Optimization and Preference Handling}
\label{sec:prefopt}
This section shows how quantitative and qualitative preferences can be used for computing optimal answer sets.
While Section~\ref{sec:optimization} summarizes the standard optimization capacities of \clasp, \gringo, and \clingo\
dealing with lexicographic optimization of linear objective functions,
Section~\ref{sec:asprin} provides a tutorial introduction to \asprin's general preference handling framework.
\subsection{Multi-objective Optimization with \clasp\ and \clingo}
\label{sec:optimization}
This subsection is not yet ready for publishing
and will be included in one of the forthcoming editions of this guide.
Some information on multi-objective optimization
can be obtained at the following references.
\begin{itemize}
\item Optimization \cite{gekakasc11b,gekakasc11c,gekasc11b,ankamasc12a}
\item Video series on \clasp's optimization capacities \url{http://potassco.org/doc/videos}
\item Consult Section~\ref{subsec:gringo:optimize} for language constructs expressing multi-criteria optimization.
\item Consult Section~\ref{subsec:clasp:solving} and~\ref{subsec:clasp:tune} for relevant \clasp\ options configurating the optimization process.
\end{itemize}
\subsection{Preference Handling with \asprin}\label{sec:asprin}
\asprin\ provides a general framework for optimizing qualitative and quantitative preferences in ASP.
It allows for computing optimal answer sets of logic programs with preferences.
While \asprin\ comes with a library of predefined preference types
(\code{subset}, \code{pareto}, etc.),
it is readily extensible by new customized preference types.
For a formal description of \asprin, please consult~\cite{brderosc15a}.
The following description conforms with \asprin~3.1, which uses \clingo~5.%1.1.
\subsubsection{Computing optimal answer sets}
Similar to common optimization in ASP,
where objective functions are added to logic programs
via minimize statements or weak constraints,
a preference specification is added to a logic program
to single out the optimal answer sets with respect to the given preferences.
However, as with minimize statements,
such a specification is not part of the program
but rather a meta statement referring to its answer sets.
Hence, preference specifications are directives and thus preceded by \#.
For clarity, we also refer to the underlying program as the \emph{base program}
(also in view of distinguishing it from the \emph{preference program},
implementing the preference specification; see below).
To begin with,
let us consider a simple example providing a holistic view on preference handling with \asprin.
%
\begin{example}\label{asprin:example1}
Consider the following base program.
\marginlabel{%
To inspect the output, invoke:\\
\code{\mbox{~}clingo \attach{examples/base.lp}{base.lp} 0}\\
or alternatively:\\
\code{\mbox{~}gringo \attach{examples/base.lp}{base.lp} \textbackslash \\\mbox{~}| clasp 0}\\
}
% \attach{examples/base.lp}{\code{base.lp}}
%
\lstinputlisting[numbers=none]{examples/base.lp}
%
% The output of the solver looks as follows:
% \begin{lstlisting}[numbers=none]
% ...
% Answer: 1
% m(2) a(1) a(2) b(1)
% Answer: 2
% m(3) a(5) b(2) b(3) b(4) b(5)
% Answer: 3
% m(1) a(1) b(1) b(2) b(3) b(4) b(5)
% ...
% \end{lstlisting}
We obtain three answer sets, one with \code{m(1)}, \code{m(2)}, and \code{m(3)}, respectively,
and refer to them as $X_1$, $X_2$, and $X_3$.
\begin{note}
Base programs are \gringo\ and \clingo\ programs as specified in Section \ref{subsec:lang:gringo},
except that %atoms names may not start with the underscore symbol `\code{\char`\_}'
%and
weak constraint and minimize and maximize statements are not allowed.
\end{note}
For a first example,
we can use \asprin\ to compute the answer sets of the base program that are subset minimal with respect to atoms of predicate $a/1$.
This can be done with the following preference specification
(available in \attach{examples/preference1.lp}{\code{preference1.lp}}):
%
\lstinputlisting{examples/preference1.lp}
%
Line~1 contains a preference statement of name \code{p1} and type \code{subset} that contains a single (non-ground) preference element.
%The body of the preference element has to be formed by domain predicates, here \code{dom(X)}.
Intuitively, the preference statement \code{p1} defines a preference of type \code{subset} over atoms of predicate \code{a/1}.
Line~2 contains an optimization directive that instructs \asprin\ to compute answer sets that are optimal with respect to \code{p1}.
\begin{note}\label{asprin:note}
Unlike \gringo's native optimization statements and weak constraints (cf.\ Section~\ref{subsec:gringo:optimize}),
\asprin\ separates the declaration of preferences from the actual optimization directive.
\end{note}
To compute an answer set of the base program that is optimal with respect to \code{p1},
an implementation of the preference type \code{subset} must be provided.
This is comprised in \asprin's preference library,
contained in the file \code{asprin\_lib.lp},
which is automatically loaded by the system unless option \code{--no-asprin-lib} is issued.
The computation can then be performed by the following command:
%
%\marginlabel{\clingo, \asprin\ and the related files \code{asprin.parser}, \code{asprin.py} and \code{asprin.lib}
% ought to be located in some directory
% in the system path.}%
%\marginlabel{\clingo\ Python module must be importable via the environment variable \code{PYTHONPATH},
% and the related file \code{asprin}
% ought to be located in some directory in the system path.
% The file \code{asprin\_lib.lp} is first looked up in the current directory.
% If it is not found there, then it is looked up in the root directory of the distribution,
% i.e., in the directory of the main file \code{asprin.py}.}%
\begin{lstlisting}[numbers=none,escapechar=\%]
asprin %\attach{examples/base.lp}{base.lp}% %\attach{examples/preference1.lp}{preference1.lp}%
\end{lstlisting}
%
The output should look like this:
%This command produces the following output:
%
\begin{lstlisting}[numbers=none]
asprin version 3.1.0
Reading from base.lp ...
Solving...
Answer: 1
m(2) a(1) a(2) b(1)
Answer: 2
m(1) a(1) b(1) b(2) b(3)
OPTIMUM FOUND
Models : 2+
Optimum : yes
...
\end{lstlisting}
%
At first, \asprin\ finds the answer set $X_2$ of the base program.
Then, it looks for an answer set that is preferred to $X_2$ and it finds $X_1$.
In the last step, \asprin\ looks for an answer set that is preferred to $X_1$,
and given that none is found the optimality of $X_1$ is established.
In total, two answer sets were enumerated in the computation of an optimal solution.
Alternatively,
we can minimize the extension of predicates \code{a/1} and \code{b/1} with the following preference specification.
%\attach{examples/preference2.lp}{\code{preference2.lp}}:
%
\lstinputlisting[numbers=none]{examples/preference2.lp}
%
Now, we obtain that $X_2$ is already an optimal answer set:
\marginlabel{%
To inspect the output, invoke:\\
\code{\mbox{~}asprin \attach{examples/base.lp}{base.lp} \mbox{~~~~}\textbackslash \
\mbox{~~~}\attach{examples/preference2.lp}{preference2.lp}}}
\begin{lstlisting}[numbers=none]
Answer: 1
m(2) a(2) a(1) b(1)
OPTIMUM FOUND
\end{lstlisting}
\end{example}
\subsubsection{Computing multiple optimal answer sets}
In analogy to \clasp\ and \clingo,
\asprin\ allows for computing $n$ optimal answer sets by adding the number $n$ to the command line;
as well, $0$ is used to compute all optimal answer sets.
\begin{example}
For instance, the command
%
\begin{lstlisting}[numbers=none,escapechar=\%]
asprin %\attach{examples/base.lp}{base.lp}% %\attach{examples/preference1.lp}{preference1.lp}% 0
\end{lstlisting}
%
results in the output:
%
\begin{lstlisting}[numbers=none]
Answer: 1
m(2) a(2) a(1) b(1)
Answer: 2
m(1) a(1) b(3) b(2) b(1)
OPTIMUM FOUND
Answer: 3
m(3) a(3) b(3) b(2)
OPTIMUM FOUND
\end{lstlisting}
%
The computation of the first optimal answer set, $X_1$, is the same as above.
Then, \asprin\ searches for an answer set of the base program that is not worse than $X_1$,
finds $X_3$, and proves that it is optimal.
In the last step, \asprin\ looks for some answer set that is not worse than $X_1$ and $X_3$,
and given that there is none, it terminates.
Adding the following choice rule
(via file \attach{examples/c1.lp}{\code{c1.lp}})
to the above optimization process
%
\lstinputlisting[numbers=none]{examples/c1.lp}
%
yields two additional optimal answer sets, both containing \code{c(1)}:
%
\marginlabel{%
To inspect the output, invoke:\\
\code{\mbox{~}asprin \attach{examples/base.lp}{base.lp} \mbox{~~~~}\textbackslash \
\mbox{~~~}\attach{examples/preference1.lp}{preference1.lp}\mbox{~~~}\textbackslash \
\mbox{~~~}\attach{examples/c1.lp}{c1.lp} 0}} %\mbox{~~~~~~~~~~~~}\textbackslash \
% \mbox{~~~}asprin.lib 0}}
%
\begin{lstlisting}[numbers=none]
Answer: 1
m(2) a(2) a(1) b(1)
Answer: 2
m(1) a(1) b(3) b(2) b(1)
OPTIMUM FOUND
Answer: 3
m(1) a(1) b(3) b(2) b(1) c(1)
OPTIMUM FOUND *
Answer: 4
m(3) a(3) b(3) b(2)
OPTIMUM FOUND
Answer: 5
m(3) a(3) b(3) b(2) c(1)
OPTIMUM FOUND *
\end{lstlisting}
%
When \asprin\ looks for an answer set that is not worse than $X_1$,
it first looks for answer sets that interpret atoms appearing in the preference statements
in the same way as $X_1$.
In this way,
it finds the second optimal model, that contains \code{c(1)},
and prints it followed by the line `\lstinline{OPTIMUM FOUND *}'.
Then, it continues searching, finds $X_3$ and the process continues.
Finally,
we can project optimal answer sets on the formulas of the preference statements
by \asprin's option \lstinline{--project}.
\marginlabel{%
To inspect the output, invoke:\\
\code{\mbox{~}asprin \attach{examples/base.lp}{base.lp} \mbox{~~~~}\textbackslash \
\mbox{~~~}\attach{examples/preference1.lp}{preference1.lp}\mbox{~~~}\textbackslash \
\mbox{~~~}\attach{examples/c1.lp}{c1.lp} 0 --project}}%\mbox{~~~~~~~~~~~~}\textbackslash \
% \mbox{~~~}asprin.lib 0\mbox{~~~~~}\textbackslash \
% \mbox{~~~}--project}\\
%}
This yields only the three optimal answer sets not containing \code{c(1)}.
% \attach{examples/c1.lp}{\code{c1.lp}}:
%
% \begin{lstlisting}[numbers=none]
% Answer: 1
% m(2) a(2) a(1) b(1)
% Answer: 2
% m(1) a(1) b(4) b(3) b(5) b(2) b(1)
% OPTIMUM FOUND
% Answer: 3
% m(3) a(5) b(4) b(3) b(5) b(2)
% OPTIMUM FOUND
% \end{lstlisting}
\end{example}
\subsubsection{Input language of \asprin}
\index{optimization!preference specification}%
\index{optimization!preference specification!preference statement}%
\index{optimization!preference specification!weighted formula}%
\index{optimization!preference specification!preference element}%
\index{optimization!optimization directive}%
\asprin's input language extends the one described in Section~\ref{sec:language} by constructs for expressing qualitative and quantitative preferences.
A \emph{weighted formula} is of the form
\[\boldsymbol{t}\code{::}F\]
where $\boldsymbol{t}$ is a term tuple,
and $F$ is a either a Boolean formula
or a naming atom.
We may drop \code{::} and simply write $F$ whenever $\boldsymbol{t}$ is empty.
If $F$ is missing\footnote{Note that empty weighted formulas are not allowed.},
we interpret is as the Boolean constant \code{\#true}.
Boolean formulas are formed from atoms, possibly preceded by classical negation (`\code{-}'),
using the connectives \code{not} (default negation), \code{\&} (conjunction) and \code{|} (disjunction).
Parentheses can be written as usual\footnote{Except that they are not allowed around atoms.},
and when omitted, negation has precedence over conjunction, and conjunction over disjunction.
%
Furthermore, if $F$ is a conjunction of the form $F_1 \code{\&} \ldots \code{\&} F_n$,
it can also we written using the body notation $F_1\code{,} \ldots\code{,} F_n$.
%
Naming atoms of form \code{**s}, where \code{s} is a term,
refer to the preference associated with preference statement \code{s} (see below).
%
Examples of weighted formulas are
`\code{42::a}',
`\code{a(X) \& b(X)}',
`\code{C::edge(X,Y), cost(X,Y,C)}',
`\code{W,(X,Y)::not a(W,X) | b(Y)}', and
`\code{X::**p(X)}'.
If $F_1$, \ldots, $F_n$ are weighted formulas, then
\[
\code{\{}F_1\code{;}\dots\code{;}F_m\code{\}}
\]
is a set of weighted formulas.
We may drop the curly braces if $m=1$.
A \emph{preference element} is of the form
%\[\boldsymbol{B}_1\; \gg \,\dots\, \gg \;\boldsymbol{B}_m\code{ || }\boldsymbol{B}\code{ : }\!\!\!\! B\]
\[\boldsymbol{F}_1\; >> \,\dots\, >> \;\boldsymbol{F}_m\code{ || }\boldsymbol{F}\code{ : }\!\!\!\! B\]
where each $\boldsymbol{F}_r$ and $\boldsymbol{F}$ is a set of weighted bodies,
and $B$ is a rule body where all literals belong to domain predicates
(see Page~\pageref{pg:domain}) or built-ins.
%
We may drop `\code{>>}' if $m=1$,
and `\code{||$\, \boldsymbol{F}$}' and `\code{:$\,B$}' whenever $\boldsymbol{F}$ and/or $B$ are empty, respectively.
%
Intuitively, $r$ gives the rank of the respective set of weighted bodies.
This can be made subject to condition $\boldsymbol{F}$ by using the conditional `\code{||}'.
Preference elements provide a (possible) structure to a set of weighted bodies
by giving a means of conditionalization and a symbolic way of defining pre-orders (in addition to using weights).
%
%Hence
%\code{\{a(X);b(X) \& c(X))\}>d(X)} stands for
%\code{\{a;neg(b)\}>\{c\} || and(d,neg(d))}.
%
Examples of preference elements are
`\code{42::a}',
`\code{a(X), b(X):c(X)}',
`\code{X::**p(X)}',
`\code{\{a(X);b(X)\} >> \{c(X);d(X)\}}', and
`\code{a(X) >> b(X) || c(X) : dom(X)}'.
\begin{note}
Here and below,
the rule body $B$ is intended \emph{exclusively} to provide instantiations for the variables appearing in the expressions to its left.
Accordingly, the literals in $B$ must be built-ins or belong to domain predicates of the accompanying logic program.
This ensures that $B$ can be fully evaluated during grounding.
\end{note}
\begin{note}\label{asprin:nobody}
If the body $B$ of a preference element $e$ is empty,
\asprin\ automatically replaces it with a body
providing the domains of the atoms appearing in $e$,
consisting of new atoms $\code{dom(}a\code{)}$
for every atom with variables $a$ in $e$,
and new atoms $\code{pref\_dom(}s\code{)}$
for every naming atom with variables $\code{**}s$ in $e$.
%
For example,
`\code{X::**p(X)}' becomes
`\code{X::**p(X) : pref\_dom(p(X))}', and
`\code{\{a(X);b(X)\} >> \{c(X);d(X)\}}' becomes
`\code{\{a(X);b(X)\} >> \{c(X);d(X)\}:dom(a(X)),dom(b(X)),dom(c(X)),dom(d(X))}'.
%
For defining those atoms,
\asprin\ extends the base program with facts
$\code{dom(}a_{gr}\code{).}$ for every ground instace $a_{gr}$ of $a$ obtained by \clingo\
after grounding the base program.
%
Similarly, \asprin\ adds facts
$\code{pref\_dom(}s_{gr}\code{).}$
for every ground instance $s_{gr}$ of $s$ obtained by \clingo\
while grounding the preference specification.
\end{note}
\index{safety!preference statement}
\begin{note}
Preference elements are required to be \emph{safe},
i.e., all variables in a preference element must occur in some positive literal
in its body or in the body of the preference statement containing it (see below).
%
Note that preference elements whose body is missing are always safe,
due to the new body automatically added by \asprin\
(see previous Remark \ref{asprin:nobody}).
\end{note}
A \emph{preference statement} is of the form %
\[\code{\#preference(s,t)\{}e_1\code{;}\dots\code{;}e_n\code{\} : }\!\!\!\!B\code{.}\]
%
where \code{s} is a term giving the preference name,
\code{t} is a term providing the preference type,
and each $e_j$ is a preference element.
The rule body $B$ has the same form and purpose as above.
%
%\begin{note}
That is, the body $B$ of a preference statement is used to instantiate the variables of $s$, $t$ and each $e_i$.
For safety, all variables appearing in \code{s} and \code{t} must also appear in a positive literal in $B$.
\begin{example}
\label{asprin:example2}
Given the logic program
\begin{lstlisting}[numbers=none]
dom(1..2).
{ a(X,Y) : dom(X), dom(Y)}.
\end{lstlisting}
the preference statement
\begin{lstlisting}[numbers=none]
#preference(p(X),subset){ a(X,Y) : dom(Y) } : dom(X).
\end{lstlisting}
stands for the following two ground preference statements:
\begin{lstlisting}[numbers=none]
#preference(p(1),subset){ a(1,1) ; a(1,2) }.
#preference(p(2),subset){ a(2,1) ; a(2,2) }.
\end{lstlisting}
\end{example}
%\end{note}
Preference statements are accompanied by
\emph{optimization directives} such as
\[\code{\#optimize(s) : }\!\!\!\!B\code{.}\]
where $B$ is as above,
telling \asprin\ to restrict its reasoning mode to the preference relation declared by \code{s}.
%
A \emph{preference specification} is a set of preference statements along with an optimization directive.
It is valid, if grounding results in acyclic and closed naming dependencies
along with a single optimization directive
(see \cite{brderosc15a} for details).
% A non ground preference specification is valid
% if after grounding it (using the accompanying logic program)
% the resulting ground specification is valid.
If a preference specification is not valid, \asprin\ reports an error and exits.
%
As mentioned before,
the purpose of such a specification is to define the optimal answer sets of an underlying base logic program.
%
\begin{note}\label{asprin:noopt}
When grounding results in no optimization directive,
\asprin\ prints a warning and computes (possibly non optimal) answer sets of the base program.
%
%Additionally, \asprin\ allows \clingo\ minimize and maximize statements
%(cf. Section \ref{subsec:gringo:optimize}) instead of a preference specification.
%%
%In this case, using \asprin's library, the system computes optimal stable models
%following the semantics of \clingo.%
%\footnote{%
%The minimize and maximize statements
%are translated into preference statements of type \code{clingo\_minimize}.
%wihch is implemented in \asprin's library according to the semantics of \clingo.
%%
%Hence, using the library, the system computes \clingo\ optimal stable models.
%%
%However, it is possible to provide a different implementation of the type \code{clingo\_minimize}
%(see Section \ref{asprin:implement}),
%thereby providing new semantics to minimize and maximize statements.}
\end{note}
\begin{example}\label{asprin:example3}
Consider a preference specification about leisure activities (without base program).
\begin{lstlisting}[escapechar=?]
#preference(costs,less(weight)){
C :: sauna : cost(sauna,C);
C :: dive : cost(dive,C)
}.
#preference(fun,superset){ sauna; dive; hike; not bunji }.
#preference(temps,aso){
dive >> sauna || hot;
sauna >> dive || not hot
}.
#preference(all,pareto){**costs; **fun; **temps}.
#optimize(all).
\end{lstlisting}
Intuitively, the relation expressed by the preference statement \code{costs} in Line~1 aims at optimizing the sum of weights of its preference elements,
viz.\ \code{C::sauna:cost(sauna,C)} and \code{C::dive:cost(dive,C)}.
The preference type \code{less(weight)} is very similar to the one used by native minimization directives (cf.\ Section~\ref{subsec:gringo:optimize}).
The preference type \code{superset} provides a set inclusion based relation and the one refereed to as \code{aso}
amounts to answer set optimization as put forward in~\cite{brnitr03a}.
These three basic preference relations are combined according to the \code{pareto} principle in Line~10.
And this combined preference relation is declared subject to optimization in Line~12.
\end{example}
%
\begin{note}
All four preference types in Example~\ref{asprin:example3} are predefined in \asprin's preference library and take different syntactic restrictions of preference elements as arguments.
\end{note}
\subsubsection{Preference relations and preference types}
\index{preference type}
\index{optimization!preference type@\gobblecomma|see{preference type}}
A ground preference statement declares a
strict partial order over answer sets.\footnote{A strict partial order is a transitive and irreflexive relation.}
This order is called a \emph{preference relation}.
\begin{example}
The preference statement of Example \ref{asprin:example1} stands for the following ground preference statement:
\begin{lstlisting}[numbers=none]
#preference(p1,subset){ a(1); a(2); a(3) }.
\end{lstlisting}
It declares the following preference relation:
\[
\begin{array}{cccl}
X \succ_{\code{p1}} Y & \text{ iff } & & \{e\in \{\code{a(1)},\code{a(2)},\code{a(3)}\} \mid X\models e\} \\
& & \subset & \{e\in \{\code{a(1)},\code{a(2)},\code{a(3)}\} \mid Y\models e\}
\end{array}
\]
In Example \ref{asprin:example1},
we get
$X_1\succ_{\code{p1}}X_2$ because \code{\{a(1)\}$\;\subset\;$\{a(1),a(2),a(3)\}}
and $X_3\succ_{\code{p1}}X_2$ given that \code{\{a(2),a(3)\}$\;\subset\;$\{a(1),a(2),a(3)\}};
however, we have $X_1\not\succ_{\code{p1}}X_3$ since \code{\{a(1)\}$\;\not\subset\;$\{a(2),a(3)\}}.
\end{example}
An answer set $X$ of a base program $P$ is \emph{optimal} with respect to a preference relation $\succ$
if there is no other answer set $Y$ of $P$ such that $Y \succ X$.
In Example \ref{asprin:example1},
%with preference statement \code{p1},
$X_1$ and $X_3$ are optimal,
whereas $X_2$ is not because $X_1 \succ_{\code{p1}} X_2$ (and $X_3 \succ_{\code{p1}} X_2$).
%Given a valid preference specification where all preference statements are admissible,
\asprin\ computes answer sets of the base program
that are optimal with respect to the preference relation
defined by the preference statement selected for optimization.
Hence, in the example it produces $X_1$ and $X_3$.
But how does a preference statement declare a preference relation?
This is accomplished by the \emph{preference type}
that maps a set $E$ of ground preference elements into a preference relation.
For example, the type \code{subset} maps $E$ into
\[
X \succ Y \text{ iff } \{e\in E\mid X\models e\}\subset\{e\in E\mid Y\models e\}
\]
And when applied to the preference elements of \code{p1} in Example \ref{asprin:example1}, we obtain $\succ_{\code{p1}}$.
The full generality of preference elements is not always needed.
%
For example, for \code{subset} we are only interested in preference elements that are Boolean formulas.
For this reason, we specify for each preference type its \emph{domain},
i.e., the ground preference elements for which the preference type is well defined.
Hence, the domain of \code{subset} consists of Boolean formulas.
Furthermore, a ground preference statement
\[\code{\#preference(s,t)\{}e_1\code{;}\dots\code{;}e_n\code{\}.}\]
is \emph{admissible} if every ${e}_i$ belongs to the domain of \code{t}.
If a ground preference statement is not admissible, \asprin\ reports an error and exits.
\begin{example}
In Example \ref{asprin:example1}, the preference statement \code{p1}
is admissible because \code{a(1)}, \code{a(2)}, and \code{a(3)} are Boolean formulas
and thus belong to the domain of \code{subset}.
If we added the preference elements \code{1::a(1)} or \code{**p2},
the statement would not be admissible any more.
\end{example}
\subsubsection{\asprin\ library}
\index{preference type!\code{subset}}
\index{preference type!\code{superset}}
\index{preference type!\code{less(cardinality)}}
\index{preference type!\code{more(cardinality)}}
\index{preference type!\code{less(weight)}}
\index{preference type!\code{more(weight)}}
\index{preference type!\code{minmax}}
\index{preference type!\code{maxmin}}
\index{preference type!\code{aso}}
\index{preference type!\code{poset}}
\index{preference type!\code{cp}}
\asprin's preference library implements the following basic preference types:
\begin{itemize}
\item \code{subset} and \code{superset}
\item \code{less(cardinality)} and \code{more(cardinality)}
\item \code{less(weight)} and \code{more(weight)}
\item \code{minmax} and \code{maxmin}
\item \code{aso} (Answer Set Optimization, \cite{brnitr03a})
\item \code{poset} (Qualitative Preferences, \cite{rogima10a})
\item \code{cp} (CP nets, \cite{bobrdohopo04a})
\end{itemize}
We have already given the definition of \code{subset}.
The preference types \code{superset}, \code{less(cardinality)}, and \code{more(cardinality)} share the domain of \code{subset}.
Given a set of ground preference elements \code{$E$},
their semantics is defined as follows:
\begin{itemize}
\item
\code{superset} maps $E$ to the preference relation
\[
X \succ Y \text{ iff } \{e\in E\mid X\models e\}\supset\{e\in E\mid Y\models e\}
\]
\item
\code{less(cardinality)} maps $E$ to the preference relation
\[
X \succ Y \text{ iff } \{e\in E\mid X\models e\}<\{e\in E\mid Y\models e\}
\]
\item
\code{more(cardinality)} maps $E$ to the preference relation
\[
X \succ Y \text{ iff } \{e\in E\mid X\models e\}>\{e\in E\mid Y\models e\}
\]
\end{itemize}
An example of preference type \code{superset} is given in Line~5 of Example~\ref{asprin:example3}.
%
\begin{example}
%
\marginlabel{%
To inspect the output, invoke:\\
\code{\mbox{~}asprin \attach{examples/base.lp}{base.lp} \mbox{~~~~}\textbackslash \
\mbox{~~~}\attach{examples/preference3.lp}{preference3.lp}}}
%
We can use the type \code{less(cardinality)} to minimize the cardinality of the atoms of predicate \code{b/1}
in Example~\ref{asprin:example1} as follows:
%
\lstinputlisting[numbers=none]{examples/preference3.lp}
%
This yields the unique optimal answer set $X_2$.
\end{example}
Preference types \code{less(weight)} and \code{more(weight)}
are similar to \code{\#minimize} and \code{\#maximize} statements.
However, they do not comprise priorities but apply to general Boolean formulas.
Their common domain consists of sets of ground preference elements of the form:
\[w\code{,}\boldsymbol{t}\code{::}F\]
Here, ${w}$ is an integer, $\boldsymbol{t}$ a term tuple, and $F$ a Boolean formula.
%
We may drop `\code{,}' when $\boldsymbol{t}$ is empty.
%
Their meaning is defined with respect to a set $E$ of ground preference elements:
\begin{itemize}
\item
\code{less(weight)} maps $E$ to the preference relation
\[
X \succ Y
\text{ iff }
\sum_{(w,\boldsymbol{t})\in\{w,\boldsymbol{t}\mid w,\boldsymbol{t}\mathtt{::}F\in E, X\models F\}}w
<
\sum_{(w,\boldsymbol{t})\in\{w,\boldsymbol{t}\mid w,\boldsymbol{t}\mathtt{::}F\in E, Y\models F\}}w
\]
\item
\code{more(weight)} maps $E$ to the preference relation
\[
X \succ Y
\text{ iff }
\sum_{(w,\boldsymbol{t})\in\{w,\boldsymbol{t}\mid w,\boldsymbol{t}\mathtt{::}F\in E, X\models F\}}w
>
\sum_{(w,\boldsymbol{t})\in\{w,\boldsymbol{t}\mid w,\boldsymbol{t}\mathtt{::}F\in E, Y\models F\}}w
\]
\end{itemize}
For illustrating the similarity to optimization statements,
consider the following \code{\#minimize} statement from Section~\ref{subsec:tsp:encoding}.
%
\lstinputlisting[numbers=none,firstline=2]{examples/min.lp}
%
With preference type \code{less(weight)},
this can be expressed as follows.
\begin{lstlisting}[numbers=none]
#preference(myminimize,less(weight))
{ C,X,Y :: cycle(X,Y), cost(X,Y,C) }.
#optimize(myminimize).
\end{lstlisting}
The similarity between preference type \code{more(weight)} and \code{\#maximize} statements is analogous.
Recall also Remarks~\ref{asprin:note} and \ref{asprin:noopt} from above.
%
Another example of preference type \code{\code{less(weight)}} is given in Lines~1-4 of Example~\ref{asprin:example3}.
Preference types \code{minmax} and \code{maxmin} are
closely related to \code{less(weight)} and \code{more(weight)},
respectively.
%
The idea is to have a set of sums,
and to minimize the maximum value of all sums with \code{minmax},
or to maximize their minimum value with \code{maxmin}.
%
Their common domain consists of sets of ground preference elements of the form:
\[s\code{,}w\code{,}\boldsymbol{t}\code{::}F\]
where $s$ is a term, ${w}$ an integer,
$\boldsymbol{t}$ a term tuple, and $F$ a Boolean formula.
%
As before, we may drop `\code{,}' when $\boldsymbol{t}$ is empty.
%
The terms $s$ name different sums,
whose value is specified by the rest of the element
`$w\code{,}\boldsymbol{t}\code{::}F$'
(similar to \code{less(weight)} and \code{more(weight)}).
%
For a set $E$ of ground preference elements,
the value of sum $s$ in $X$ is:
\[
v(s,X)=\sum_{(w,\boldsymbol{t})\in
\{w,\boldsymbol{t}\mid s,w,\boldsymbol{t}\mathtt{::}F\in E, X\models F\}}w
\]
Then:
\begin{itemize}
\item
\code{minmax} maps $E$ to the preference relation%
\[
X \succ Y \text{ if }
\max \{ v(s,X) \mid s \ \text{is a sum of } E \} <
\max \{ v(s,Y) \mid s \ \text{is a sum of } E \}
\]
\item
\code{maxmin} maps $E$ to the preference relation%
\[
X \succ Y \text{ if }
\min \{ v(s,X) \mid s \ \text{is a sum of } E \} >
\min \{ v(s,Y) \mid s \ \text{is a sum of } E \}
\]
\end{itemize}
\begin{example}\label{asprin:minmaxexample}
%
\marginlabel{%
To inspect the output, invoke:\\
\code{\mbox{~}asprin \attach{examples/base.lp}{base.lp} \mbox{~~~~}\textbackslash \
\mbox{~~~}\attach{examples/preference4.lp}{preference4.lp}}}
%
The following preference statement
expresses a preference for
minimizing the maximum number of atoms of the predicates \code{a/1} and \code{b/1}:
%
\lstinputlisting[numbers=none]{examples/preference4.lp}
%
%The statement says that
%for every \code{X} of \code{dom/1},
%if \code{a(X)} is true or \code{b(X)} is false,
%this is preferred to the conjunction of \code{a(X)} being false and \code{b(X)} being true.
Together with the base program in Example~\ref{asprin:example1}, this yields optimal answer sets $X_2$ and $X_3$.
%
Using \code{maxmin} (simply adding \code{-c minmax=maxmin} to the command line) we obtain also $X_1$.
\end{example} %
The preference type~\code{aso} implements answer set optimization~\cite{brnitr03a} and relies upon
ground preference elements of the form:
\[ F_1 \, \code{>>} \, \dots \, \code{>>} \, F_m \code{ || }F\]
where each $F_i$ and $F$ are Boolean formulas.
Preference elements of this form are called \code{aso} rules.
The semantics of \code{aso} is based on satisfaction degrees.
In a nutshell,
the satisfaction degree of an \code{aso} rule $r$ in an answer set $X$,
written $v_X(r)$, is
$1$ if $X$ does not satisfy the body $B$, % $X \not\models b$ for some $b\in B$, %\cap\mathcal{A}$ or if $X \models b$ for some $\naf{b}\in B$,
or if $X$ does not satisfy any $F_i$,
and it is $\min\{k \mid X \models F_k, 1\leq k\leq n\}$ otherwise.
Then, a set of \code{aso} rules $E$ is mapped to the preference relation defined as follows:
$X \succeq Y$ if for all rules $r \in E$, $v_X(r) \leq v_Y(r)$,
and $X \succ Y$ if $X \succeq Y$ but $Y \not\succeq X$.
See~\cite{brnitr03a} for a more detailed introduction.
%An example of preference type \code{aso} is given in Lines~6-9 of Example~\ref{asprin:example3}.
%
\begin{example}\label{asprin:asoexample}
%
\marginlabel{%
To inspect the output, invoke:\\
\code{\mbox{~}asprin \attach{examples/base.lp}{base.lp} \mbox{~~~~}\textbackslash \
\mbox{~~~}\attach{examples/preference5.lp}{preference5.lp}}}
%
The following preference statement of type \code{aso} expresses a preference
for atoms of predicate \code{a/1} over atoms of predicate \code{b/1}.
%
\lstinputlisting[numbers=none]{examples/preference5.lp}
%
%The statement says that
%for every \code{X} of \code{dom/1},
%if \code{a(X)} is true or \code{b(X)} is false,
%this is preferred to the conjunction of \code{a(X)} being false and \code{b(X)} being true.
Together with the base program in Example~\ref{asprin:example1}, this yields the unique optimal answer set $X_2$.
\end{example} %
Another example of preference type \code{aso} is given in Lines~6-9 of Example~\ref{asprin:example3}.
The preference type \code{poset} implements the approach to qualitative preferences put forward in~\cite{giumar12a}.
Such preferences are modeled as a strict partially ordered set
\(
(S,>)
\)
of literals.
The literals in $S$ represent propositions that are preferably satisfied
and the strict partial order $>$ on $S$ gives their relative importance.
%
The \asprin\ implementation of \code{poset} extends the original approach by allowing preferences over Boolean formulas.
The domain of \code{poset} consists of the sets $E$ of ground preference elements of the form
\[F\code{.}\]
or
\[F \, \code{>>} \, F'\code{.}\]
where $F$ and $F'$ are Boolean formulas.
%
To give a glimpse of the formal underpinnings,
consider a set $E$ of such ground preference elements.
The set $S_E$ consists of all Boolean formulas appearing in $E$
and the partial order $>_E$ is the transitive closure of the order
specified by the preference elements of the second type.
Then, $X \succ Y$ holds if
there is some formula $F \in S_E$ such that $X \models F$ and $Y \not\models F$,
and for every formula $F \in S_E$ such that $Y \models F$ and $X \not\models F$,
there is a formula
$F'\in S$ such that $F'>_{E}F$ and $X \models F'$ but $Y \not\models F'$. The interested reader is referred to~\cite{giumar12a} for full details. %
\begin{example}
%
\marginlabel{%
To inspect the output, invoke:\\
\code{\mbox{~}asprin \attach{examples/base.lp}{base.lp} \mbox{~~~~}\textbackslash \
\mbox{~~~}\attach{examples/preference6.lp}{preference6.lp}}}
%
We apply the preference type \code{poset} to the preference statement of Example \ref{asprin:asoexample}:
%
\lstinputlisting[numbers=none]{examples/preference6.lp}
%
This expresses a preference for the truth of both \code{a/1} and \code{b/1},
preferring \code{a/1} over \code{b/1}.
With the base program in Example~\ref{asprin:example1},
we obtain three optimal answer sets $X_1$, $X_2$ and $X_3$.
\end{example} %
\label{asprin:cp}
The preference type \code{cp} implements CP-nets (\cite{bobrdohopo04a}) by means of
preference elements of the following form:
\[ L_1 \ \code{>>} \ L_2 \code{ || } \boldsymbol{L}\]
where $\boldsymbol{L}$ is a set of literals,
and $L_1$ and $L_2$ are contrary literals,
i.e., for some atom $A$, either $L_1$ is $A$ and $L_2$ is $\code{not}~A$, or vice versa.
The semantics of CP-nets rely on the notion of \emph{improving flips}.
%
Consider a set $E$ of ground preference elements,
and two sets of atoms $X$ and $Y$.
%
There is an improving flip from $X$ to $Y$ if there is some preference element in $E$ such that
all literals in $\boldsymbol{L}$ are satisfied by $X$ and $Y$, and
either $L_1$ is $A$ and $Y$ is $X\cup\{A\}$, or
$L_1$ is $\code{not}~A$ and $Y$ is $X\setminus\{A\}$.
%
Then, $W \succ Z$ holds if there is a sequence of improving flips from $Z$ to $W$.
%
A preference statement is said to be consistent if there is no set of atoms $X$
such that $X \succ X$.
%
\asprin\ assumes that the input \code{cp} preference statements are always consistent.
\begin{example}
%
\marginlabel{%
To inspect the output, invoke:\\
\code{\mbox{~}asprin \attach{examples/base.lp}{base.lp} \mbox{~~~~}\textbackslash \
\mbox{~~~}\attach{examples/preference7.lp}{preference7.lp}\mbox{~~~}\textbackslash \
\mbox{~~~}--meta=simple}}
%
The following preference statement expresses a preference for atoms of predicate \code{a/1} being true,
and atoms of predicate \code{b/1} having the same value as the corresponding ones of \code{a/1}:
%
\lstinputlisting[numbers=none]{examples/preference7.lp}
%
With the base program in Example~\ref{asprin:example1},
we obtain two optimal answer sets $X_2$ and $X_3$.
%
$X_1$ is not optimal because $X_2$ is better than it.
\end{example} %
\begin{note}
For CP-nets whose structure corresponds to a set of trees,
we can use options \code{--const-nb cp\_tree=1 --meta=no},
and optionally \code{--approximation=weak} or \code{--approximation=heuristic}.
%
For CP-nets with acyclic structure,
we can use options \code{--approximation=weak} or \code{--approximation=heuristic},
that should be combined with \code{--meta=combine} when computing more than one optimal models.
%
Options \code{--meta=simple} or \code{--meta=combine} can always be used for any CP net.
Their performance can be improved providing the diameter $n$%
\footnote{The diameter of a CP net is the longest loop-free sequence of improving flips
between any two sets of atoms.}
of the CP net whenever it is known,
using $\code{--const-nb cp\_nontree\_diameter=}n$.
%
In general, one of the previous options has to be issued,
otherwise \code{asprin} will generate an error.
%
The reason for this is that the preference programs for \code{cp} contain some choice rules,
and this requires a dedicated treatment by the system (see also Remark~\ref{asprin:note:meta}).
%
As a rule of thumb,
we recommend to use the most specific options for the CP net at hand.
\end{note}
% TODO: Fix later programs
% TODO: Fix later remark
\index{preference type!\code{neg}}
\index{preference type!\code{and}}
\index{preference type!\code{pareto}}
\index{preference type!\code{lexico}}
The library of \asprin\ implements furthermore the following composite preference types,
which amount to the ones defined in~\cite{sonpon06a}:
\begin{itemize}
\item \code{neg}
\item \code{and}
\item \code{pareto}
\item \code{lexico}
\end{itemize}
Preference types \code{and} and \code{pareto} deal with sets of ground naming atoms
\[\code{**s}\]
For \code{neg}, these sets must be singleton.
And for \code{lexico}, each naming atom has an attached tuple $\code{$w$}$:
\[w\code{::**s}\]
Given a naming atom \code{**s},
let $\succ_{\code{s}}$, $\succeq_{\code{s}}$, $=_{\code{s}}$, $\preceq_{\code{s}}$, $\prec_{\code{s}}$ be the
strict, non-strict, equal, and inverse preference relations associated with preference statement $\code{s}$.
Then, the semantics of each composite preference type is defined as follows:
\begin{itemize}
\item
\code{neg} maps $E=\code{\{**s\}}$ to the preference relation
\[
X \succ Y \text{ iff } Y \prec_s X
\]
\item
\code{and} maps \code{$E=$\{**$s_1$;$\ldots$;**$s_n$\}} to the preference relation
\[
X \succ Y \text{ iff } \bigwedge_{\code{**s}\in E}(X\succ_\code{s} Y)
\]
\item
\code{pareto} maps \code{$E=$\{**$s_1$;$\ldots$;**$s_n$\}} to the preference relation
\[
X \succ Y \text{ iff } \bigwedge_{\code{**s}\in E} (X\succeq_\code{s} Y)\wedge\bigvee_{\code{**s}\in E} (X\succ_\code{s} Y)
\]
\item
\code{lexico} maps \code{$E=$\{$w_1$::**$s_1$;$\ldots$;$w_n$::**$s_n$\}} to the preference relation
\[
X \succ Y \text{ iff } \bigvee_{\code{w::**s}\in E}\!((X\!\succ_\code{s} \!Y)\!\wedge\!\bigwedge_{\code{v::**s'}\in E,\code{v}>\code{w}}(X =_{\code{s'}} Y)\!)
\]
\end{itemize}
\begin{example}\label{asprin:composite}
Consider the following preference specification, where \code{p1} and \code{p3} are defined as before:
%
\lstinputlisting[numbers=none]{examples/preference8.lp}
\marginlabel{%
To inspect the output, invoke:\\
\code{\mbox{~}asprin \attach{examples/base.lp}{base.lp} \mbox{~~}\textbackslash \
\mbox{~~~}\attach{examples/preference8.lp}{preference8.lp}\mbox{~}\textbackslash\
\mbox{~~~}\attach{examples/optimize_p8.lp}{optimize\_p8.lp}\mbox{~}0}}
%
Along with the base program of Example \ref{asprin:example1} and adding the fact \code{\#optimize(p8)},
\asprin\ produces answer sets $X_2$ and $X_3$.
If instead we optimize over \code{p9} or \code{p10}, we obtain the three answer sets $X_1$, $X_2$ and $X_3$,
while optimizing on \code{p11} we get only $X_2$.
\end{example}
\subsubsection{Implementing preference types}\label{asprin:implement}
\index{optimization!preference program}
In \asprin, preference types are implemented by logic programs called \emph{preference programs}.
In a nutshell, a preference type decides if,
given a preference statement \code{s},
an answer set $X$ is better than another answer set $Y$.
To represent that decision by a preference program,
the three involved elements \code{s}, $X$, and $Y$ are translated into facts and rules.
Let us first look at some simple translations of preference statements.
%In \asprin, preference statements are translated into rules.
%Let's see first some simple examples.
\begin{example}
\label{asprin:example1translated}
Recall the preference statement \code{p1} of Example \ref{asprin:example1}:
%\begin{lstlisting}[numbers=none]
\lstinputlisting[numbers=none,firstline=1,lastline=1]{examples/preference1.lp}
%#preference(p1,subset){ a(X) : dom(X) }.
%\end{lstlisting}
This is translated into:\footnote{% %the rules $F_\code{p1}$:
Using option \code{--print-programs}, \asprin\ prints the result of the translation.}
\begin{lstlisting}
preference(p1,subset).
preference(p1,(1,1,(X)),1,for(atom(a(X))),()) :- dom(X).
\end{lstlisting}
Line~1 states the name and the type of the preference statement.
Line~2 can be read as follows:
the preference statement \code{p1},
appearing as the first preference statement of the program,
in the first element has variables $\{\code{X}\}$,
and in the first position of the element there is a Boolean formula \code{a(X)} that has an empty list of associated weights.
%The reification $F_\code{p2}$ of
The translation of
\lstinputlisting[numbers=none,firstline=1,lastline=1]{examples/preference2.lp}
replaces \code{p1} with \code{p2} in Line~1 and~2, and adds:
\begin{lstlisting}[numbers=none]
preference(p2,(1,2,(X)),1,for(atom(b(X))),()) :- dom(X).
\end{lstlisting}
Number \code{2} in \code{(1,2,(X))} tells us that this is the second preference element.
\end{example}
\begin{example}
The preference statement of Example \ref{asprin:example2}:
\begin{lstlisting}[numbers=none]
#preference(p(X),subset){ a(X,Y) : dom(Y) } : dom(X).
\end{lstlisting}
is translated into the rules:
\begin{lstlisting}[numbers=none]
preference(p(X),subset) :- dom(X).
preference(p(X),(1,1,(Y,X)),1,for(atom(a(X,Y))),()) :-
dom(Y), dom(X).
\end{lstlisting}
Observe how \code{dom(X)} is appended to both rules.
\end{example}
In general, a weighted formula \code{$\boldsymbol{t}$::$F$}
occurs in some set
\[\boldsymbol{F}_i=\code{\{}F_1\code{;}\dots\code{;}F_m\code{\}}\]
of a preference element $e_j$ of the form
\[\boldsymbol{F}_1\;>\,\dots\,>\;\boldsymbol{F}_n\code{ || }\boldsymbol{F_0}\code{ : }\!\!\!\! B_j\]
that belongs itself to a preference statement \code{s} of the form
\[\code{\#preference(s,t)\{}e_1\code{;}\dots\code{;}e_o\code{\} : }\!\!\!\!B\code{.}\]
appearing as the $k$-th preference statement of the program.
Accordingly, the weighted formula is translated into a rule of the form
\[\code{preference(s,(}k\code{,}j\code{,}\boldsymbol{v}\code{),}i\code{,for(}t_F\code{),}\boldsymbol{t}\code{) :- }B_j\code{, }B\code{.}\]
where $i$ and $j$ are the indexes of $\boldsymbol{F}_i$ and $e_j$, respectively,
$\boldsymbol{v}$ is a term tuple containing all variables appearing in the rule,
and ${t}_F$ is a term representing the Boolean formula $F$
by using function symbols \code{atom/1}, \code{neg/1}, \code{and/2}, and \code{or/2} in prefix notation.
For example,