147 lines
6.5 KiB
TeX
147 lines
6.5 KiB
TeX
\documentclass{article}
|
||
|
||
|
||
\usepackage[utf8]{inputenc}
|
||
\usepackage{pgfplots}
|
||
\DeclareUnicodeCharacter{2212}{−}
|
||
\usepgfplotslibrary{groupplots,dateplot}
|
||
\usetikzlibrary{patterns,shapes.arrows}
|
||
\pgfplotsset{compat=newest}
|
||
|
||
|
||
\usepackage{hyperref}
|
||
\usepackage{verbatim}
|
||
\usepackage[american]{babel}
|
||
\usepackage{float}
|
||
\usepackage{enumerate}
|
||
\usepackage{graphicx}
|
||
\usepackage{tikz}
|
||
\graphicspath{{./figures/}}
|
||
|
||
|
||
\usepackage[%
|
||
backend=biber,%
|
||
style=ieee,%
|
||
backref=false,%
|
||
sortcites=true,sorting=nyt,%
|
||
mincitenames=1,maxcitenames=2%
|
||
]{biblatex}
|
||
\AtEveryBibitem{\clearfield{note}}
|
||
\AtEveryBibitem{\clearfield{url}}
|
||
\AtEveryBibitem{\clearfield{isbn}}
|
||
\AtEveryBibitem{\clearfield{issn}}
|
||
\AtEveryBibitem{\clearfield{doi}}
|
||
\AtEveryBibitem{\clearfield{urlyear}}
|
||
\AtEveryBibitem{\clearfield{timestamp}}
|
||
|
||
\addbibresource{refs.bib}
|
||
|
||
|
||
\title{Disjunctive Answer Set Programming\\{\small CMPUT 325 LAB Winter 2023}}
|
||
\author{Spencer Killen}
|
||
|
||
\begin{document}
|
||
\raggedbottom
|
||
% \raggedright
|
||
% \pretolerance=10000
|
||
\maketitle
|
||
|
||
An ASP program consists of a series of rules.
|
||
Atoms are globally named symbols that appear within rules.
|
||
Here we describe disjunctive answer set semantics~\cite{przymusinski_stable_1991}.
|
||
|
||
|
||
Example Rule:
|
||
\begin{verbatim}
|
||
foo, blah :- baz, bar, not jam, not can, not bread.
|
||
\end{verbatim}
|
||
|
||
|
||
Each rule has the following parts:
|
||
\begin{enumerate}
|
||
\item the head (``foo, blah'' in above). Can contain 0 or more atoms.
|
||
\item the positive body (``baz, bar'' in above). Can contain 0 or more atoms.
|
||
\item the negative body (``not jam, not can, not bread''). Can contain 0 or more atoms, each preceded by ``not`''
|
||
\end{enumerate}
|
||
Note that Clingo allows you inter interleave atoms in the positive and negative body of rules. E.g.,
|
||
\begin{verbatim}
|
||
:- not a, b, not j.
|
||
\end{verbatim}
|
||
Is a valid rule.
|
||
|
||
Rather than ``running'' an answer set program, we try to find a true/false assignment to all atoms that appear in the program.
|
||
Assignments are treated as sets where the set contains only the atoms that are assigned true.
|
||
Such a truth assignment is called a \textbf{model} of a program if all rules are satisfied by the assignment.
|
||
The following describes rule satisfaction:
|
||
\begin{itemize}
|
||
\item The positive body of a rule is satisfied by an answer set if all atoms in the body are \textbf{true}. If there are no atoms in the positive body, then it is automatically satisfied.
|
||
\item The negative body of a rule is satisfied by an answer set if all of its atoms are \textbf{false}.
|
||
\item A rule is satisfied if either:
|
||
\begin{itemize}
|
||
\item Either the rule's positive or negative body is not satisfied.
|
||
\item The rule's body is satisfied and one or more atoms in the head of the rule is true (Note: if the head has 0 atoms this is not possible)
|
||
\end{itemize}
|
||
\end{itemize}
|
||
|
||
A model of a program is called an \textbf{answer set} if it's minimal, i.e.\ there is no other model of the program that is $\subseteq$ smaller (An assignment is treated as a set containing the atoms assigned true).
|
||
\textbf{NOTE:} a model $X$ may be an answer set even if there exists another model $Y$ with a fewer number of atoms, so long there is some atom that is true in $Y$ that is not true in $X$.
|
||
|
||
Another way of looking at answer sets / minimality: if we can change some of the true atoms in an answer set to be false, then there must be some rule that is no longer satisfied as a result.
|
||
This is the same as saying that every atom must be justified by a rule.
|
||
When performing such a ``minimality check'', negative rule bodies are given special treatment:
|
||
When we change true atoms to be false, negative bodies are only satisfied if they were satisfied before we made the change.
|
||
|
||
|
||
Example:
|
||
\begin{verbatim}
|
||
a.
|
||
a, b :- not c.
|
||
\end{verbatim}
|
||
There are 3 atoms, so there are 8 possible assignments that could be answer sets.
|
||
We go through each possible assignment using pairs $(T, F)$ where $T$ is the set of atoms assigned true, and $F$ is the set of atoms assigned false.
|
||
\begin{enumerate}
|
||
\item $(\{ b \}, \{ a, c \})$, $(\{ c \}, \{ a, b \})$, $(\{ b, c \}, \{ a \})$, and $(\emptyset, \{ a, b, c \})$: All cases where ``a'' is false. The program is not satisfied because the first rule ``a'''s body is satisfied (it is empty), but ``a'' (from the head of the rule) is not true.
|
||
\item $(\{ a \}, \{ b, c \})$: This is an answer set. If we try to make ``a'' false, then the program is not satisfied (See 1).
|
||
\item $(\{ a, b \}, \{ c \})$: This is not an answer set because it is not minimal (See 2, we can make b false).
|
||
\item $(\{ a, b, c \}, \emptyset)$: This is not an answer set: We can make $b$ and $c$ false, and all the rules will be satisfied. Note that when we change ``c'' to be false, the negative body of the rule ``a, b :- not c.'' does not become satisfied.
|
||
\end{enumerate}
|
||
|
||
Another example:
|
||
\begin{verbatim}
|
||
a :- not b.
|
||
b :- not a.
|
||
\end{verbatim}
|
||
\begin{enumerate}
|
||
\item $(\emptyset, \{ a, b \})$: Not an answer set. Both rule bodies are satisfied therefore $a$ and $b$ must be true.
|
||
\item $(\{ a, b \}, \emptyset)$: Not an answer set. We can make both a and b false and all rules are satisfied (Remember that previously unsatisfied negative bodies do not become satisfied during the minimality check)
|
||
\item $(\{ a \}, \{ b \})$: This is an answer set: if we make $a$ false, the negative body of the rule ``a :- not b'' remains satisfied and requires ``a'' to be true.
|
||
\item $(\{ b \}, \{ a \})$: This is an answer set: same reason as above using the rule ``b :- not a'' instead.
|
||
\end{enumerate}
|
||
|
||
Another example:
|
||
\begin{verbatim}
|
||
a, b.
|
||
b :- a.
|
||
\end{verbatim}
|
||
\begin{enumerate}
|
||
\item $(\{ a, b \}, \emptyset)$: Not an answer set. If we change ``b'' to be false, then all rules are satisfied.
|
||
\item $(\emptyset, \{ a, b \})$: Not an answer set. The body of the rule (``a, b.'') is satisfied (because it is empty). So either ``a'' or ``b'' (or both) must be true.
|
||
\item $(\{ a \}, \{ b \})$: Not an answer set, ``b'' must be true because of the rule ``b :- a.''
|
||
\item $(\{ b \}, \{ a \})$: An answer set.
|
||
\end{enumerate}
|
||
|
||
|
||
Last example:
|
||
\begin{verbatim}
|
||
:- a.
|
||
a, b.
|
||
\end{verbatim}
|
||
Here ``a'' cannot be true, because that would satisfy the body of the rule ``:- a.'' and there is no way to satisfy the head of the rule.
|
||
|
||
|
||
\clearpage
|
||
\newpage
|
||
\printbibliography
|
||
|
||
|
||
\end{document} |