commit 50fe489f9b7e34faf335108afe51a089a152975a Author: Spencer Killen Date: Fri Mar 17 14:30:04 2023 -0600 init diff --git a/.gitattributes b/.gitattributes new file mode 100644 index 0000000..b634d85 --- /dev/null +++ b/.gitattributes @@ -0,0 +1 @@ +*.pdf filter=lfs diff=lfs merge=lfs -text diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..7766db6 --- /dev/null +++ b/.gitignore @@ -0,0 +1,10 @@ +*.aux +*.bbl +*.bcf +*.blg +*.fdb_latexmk +*.fls +*.log +*.out +*.run.xml +*.synctex.gz diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..576ac22 --- /dev/null +++ b/Makefile @@ -0,0 +1,8 @@ +all: document.pdf + +%.pdf: %.tex + latexmk -pdf $< + +clean: + latexmk -C + rm -rf *.bbl *.run.xml diff --git a/document.pdf b/document.pdf new file mode 100644 index 0000000..bb7df38 --- /dev/null +++ b/document.pdf @@ -0,0 +1,3 @@ +version https://git-lfs.github.com/spec/v1 +oid sha256:ebf2beccfa4fbb936dc75ac3c45f2cedb00059ba6a7f4e17dfc3c608f3c1f5da +size 135529 diff --git a/document.tex b/document.tex new file mode 100644 index 0000000..c0a1eec --- /dev/null +++ b/document.tex @@ -0,0 +1,147 @@ +\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} \ No newline at end of file diff --git a/refs.bib b/refs.bib new file mode 100644 index 0000000..27fffaf --- /dev/null +++ b/refs.bib @@ -0,0 +1,159 @@ +@inproceedings{gvn1, +author = {Gargi, Karthik}, +title = {A Sparse Algorithm for Predicated Global Value Numbering}, +year = {2002}, +isbn = {1581134630}, +publisher = {Association for Computing Machinery}, +address = {New York, NY, USA}, +url = {https://doi.org/10.1145/512529.512536}, +doi = {10.1145/512529.512536}, +abstract = {This paper presents a new algorithm for performing global value numbering on a routine in static single assignment form. Our algorithm has all the strengths of the most powerful existing practical methods of global value numbering; it unifies optimistic value numbering with constant folding, algebraic simplification and unreachable code elimination. It goes beyond existing methods by unifying optimistic value numbering with further analyses: it canonicalizes the structure of expressions in order to expose more congruences by performing global reassociation, it exploits the congruences induced by the predicates of conditional jumps (predicate inference and value inference), and it associates the arguments of acyclic \o{} functions with the predicates controlling their arrival (\o{} predication), thus enabling congruence finding on conditional control structures. Finally, it implements an efficient sparse formulation and offers a range of tradeoffs between compilation time and optimization strength. We describe an implementation of the algorithm and present measurements of its strength and efficiency collected when optimizing the SPEC CINT2000 C benchmarks.}, +booktitle = {Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation}, +pages = {45–56}, +numpages = {12}, +keywords = {global value numbering, static single assignment}, +location = {Berlin, Germany}, +series = {PLDI '02} +} + + +@article{gvn2, +author = {Simpson, Taylor and Cooper, Keith and Simpson, L.}, +year = {1997}, +month = {02}, +pages = {}, +title = {SCC-based value numbering} +} + +@article{rice, + title={Classes of recursively enumerable sets and their decision problems}, + author={H. Gordon Rice}, + journal={Transactions of the American Mathematical Society}, + year={1953}, + volume={74}, + pages={358-366} +} + +@inproceedings{alviano_wasp_2013, + title = {{WASP}: A Native {ASP} Solver Based on Constraint Learning}, + volume = {8148}, + url = {https://doi.org/10.1007/978-3-642-40564-8\_6}, + doi = {10.1007/978-3-642-40564-8_6}, + series = {Lecture Notes in Computer Science}, + pages = {54--66}, + booktitle = {Logic Programming and Nonmonotonic Reasoning, 12th International Conference, {LPNMR} 2013, Corunna, Spain, September 15-19, 2013. Proceedings}, + publisher = {Springer}, + author = {Alviano, Mario and Dodaro, Carmine and Faber, Wolfgang and Leone, Nicola and Ricca, Francesco}, + editor = {Cabalar, Pedro and Son, Tran Cao}, + date = {2013}, +} + +@article{cuteri_partial_2019, + title = {Partial Compilation of {ASP} Programs}, + volume = {19}, + url = {https://doi.org/10.1017/S1471068419000231}, + doi = {10.1017/S1471068419000231}, + pages = {857--873}, + number = {5}, + journaltitle = {Theory Pract. Log. Program.}, + author = {Cuteri, Bernardo and Dodaro, Carmine and Ricca, Francesco and Schüller, Peter}, + date = {2019}, +} + +@article{gebser_conflict-driven_2012, + title = {Conflict-driven answer set solving: From theory to practice}, + volume = {187}, + url = {https://doi.org/10.1016/j.artint.2012.04.001}, + doi = {10.1016/j.artint.2012.04.001}, + pages = {52--89}, + journaltitle = {Artif. Intell.}, + author = {Gebser, Martin and Kaufmann, Benjamin and Schaub, Torsten}, + date = {2012}, +} + +@inproceedings{killen_fixpoint_2021, + title = {Fixpoint Characterizations of Disjunctive Hybrid {MKNF} Knowledge Bases}, + volume = {2970}, + url = {http://ceur-ws.org/Vol-2970/aspocppaper3.pdf}, + series = {{CEUR} Workshop Proceedings}, + booktitle = {Proceedings of the International Conference on Logic Programming 2021 Workshops co-located with the 37th International Conference on Logic Programming ({ICLP} 2021), Porto, Portugal (virtual), September 20th-21st, 2021}, + publisher = {{CEUR}-{WS}.org}, + author = {Killen, Spencer and You, Jia-Huai}, + editor = {Arias, Joaquín and D'Asaro, Fabio Aurelio and Dyoub, Abeer and Gupta, Gopal and Hecher, Markus and {LeBlanc}, Emily and Peñaloza, Rafael and Salazar, Elmer and Saptawijaya, Ari and Weitkämper, Felix and Zangari, Jessica}, + date = {2021}, +} + + +@article{przymusinski_stable_1991, + title = {Stable semantics for disjunctive programs}, + volume = {9}, + issn = {0288-3635, 1882-7055}, + url = {http://link.springer.com/10.1007/BF03037171}, + doi = {10.1007/BF03037171}, + abstract = {Machine ({XWAM}) for this semantics 37{\textasciitilde} and developed an elegant interpreter in Prolog. For datalog programs with negation** the computation of well-founded models is quadratic in the size of the program (see Ref. 30) for details).}, + pages = {401--424}, + number = {3}, + journaltitle = {New Generation Computing}, + shortjournal = {New Gener Comput}, + author = {Przymusinski, Teodor C.}, + urldate = {2021-09-29}, + date = {1991-08}, + langid = {english}, + file = {Przymusinski - 1991 - Stable semantics for disjunctive programs.pdf:/home/capybara/Zotero/storage/S7KWDC6J/Przymusinski - 1991 - Stable semantics for disjunctive programs.pdf:application/pdf}, +} + +@incollection{denecker_approximations_2000, + location = {Boston, {MA}}, + title = {Approximations, Stable Operators, Well-Founded Fixpoints and Applications in Nonmonotonic Reasoning}, + isbn = {978-1-4613-5618-9 978-1-4615-1567-8}, + url = {http://link.springer.com/10.1007/978-1-4615-1567-8_6}, + abstract = {In this paper we develop an algebraic framework for studying semantics of nonmonotonic logics. Our approach is formulated in the language of lattices, bilattices, operators and xpoints. The goal is to describe xpoints of an operator O de ned on a lattice. The key intuition is that of an approximation, a pair (x; y) of lattice elements which can be viewed as an approximation to each lattice element z such that x z y. The key notion is that of an approximating operator, a monotone operator on the bilattice of approximations whose xpoints approximate the xpoints of the operator O. The main contribution of the paper is an algebraic construction which assigns a certain operator, called the stable operator, to every approximating operator on a bilattice of approximations. This construction leads to an abstract version of the well-founded semantics. In the paper we show that our theory o ers a uni ed framework for semantic studies of logic programming, default logic and autoepistemic logic.}, + pages = {127--144}, + booktitle = {Logic-Based Artificial Intelligence}, + publisher = {Springer {US}}, + author = {Denecker, Marc and Marek, Victor and Truszczyński, Mirosław}, + editor = {Minker, Jack}, + urldate = {2021-07-21}, + date = {2000}, + doi = {10.1007/978-1-4615-1567-8_6}, +} + +@inproceedings{david_schneider_jitting_2010, + title = {Jitting Prolog for Fun and Profit}, + booktitle = {Proceedings of the 4th Workshop on Dynamic Languages and Applications ({DYLA})}, + author = {David Schneider, Carl Friedrich Bolz, Michael Leuschel}, + date = {2010-06}, +} + +@inproceedings{eiter_eliminating_2004, + title = {On Eliminating Disjunctions in Stable Logic Programming}, + url = {http://www.aaai.org/Library/KR/2004/kr04-047.php}, + pages = {447--458}, + booktitle = {Principles of Knowledge Representation and Reasoning: Proceedings of the Ninth International Conference ({KR}2004), Whistler, Canada, June 2-5, 2004}, + publisher = {{AAAI} Press}, + author = {Eiter, Thomas and Fink, Michael and Tompits, Hans and Woltran, Stefan}, + editor = {Dubois, Didier and Welty, Christopher A. and Williams, Mary-Anne}, + date = {2004}, +} + +@article{gebser_seventh_2020, + title = {The Seventh Answer Set Programming Competition: Design and Results}, + volume = {20}, + url = {https://doi.org/10.1017/S1471068419000061}, + doi = {10.1017/S1471068419000061}, + pages = {176--204}, + number = {2}, + journaltitle = {Theory Pract. Log. Program.}, + author = {Gebser, Martin and Maratea, Marco and Ricca, Francesco}, + date = {2020}, +} + +@book{lifschitz_answer_2019, + title = {Answer Set Programming}, + isbn = {978-3-030-24657-0}, + url = {https://doi.org/10.1007/978-3-030-24658-7}, + publisher = {Springer}, + author = {Lifschitz, Vladimir}, + date = {2019}, + doi = {10.1007/978-3-030-24658-7}, +} \ No newline at end of file