cmput-325-w23-labsheet/document.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}