% Created 2014-05-18 Sun 21:57
\documentclass[11pt]{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{fixltx2e}
\usepackage{graphicx}
\usepackage{longtable}
\usepackage{float}
\usepackage{wrapfig}
\usepackage{rotating}
\usepackage[normalem]{ulem}
\usepackage{amsmath}
\usepackage{textcomp}
\usepackage{marvosym}
\usepackage{wasysym}
\usepackage{amssymb}
\usepackage{hyperref}
\tolerance=1000
\author{Torsten Schaub\thanks{based on encodings by Roland Kaminski (BIG thanks!)}\\ \url{torsten@cs.uni-potsdam.de}\\ \url{http://potassco.sourceforge.net/videos.html}}
\date{\today}
\title{Basic modeling in ASP and more\\
via the n-Queens puzzle
}
\hypersetup{
  pdfkeywords={},
  pdfsubject={},
  pdfcreator={Emacs 24.3.1 (Org mode 8.2.3c)}}
\begin{document}

\maketitle
\tableofcontents

\section{The problem}
\label{sec-1}

\begin{itemize}
\item Problem statement:

Place n queens on an n x n chess board
such that
no two queens attack one another

\item \url{http://en.wikipedia.org/wiki/Eight_queens_puzzle} (here n=8)

\item Example: n-Queens puzzle, Section 3.2 and 8.1 in \footnote{M. Gebser, R. Kaminski, B. Kaufmann, and T. Schaub: Answer Set Solving in Practice.
Synthesis Lectures on Artificial Intelligence and Machine Learning, Morgan and Claypool
December 2012, 238 pages, \url{10.2200/S00457ED1V01Y201211AIM019}}
\end{itemize}
\section{The systems}
\label{sec-2}

\begin{itemize}
\item Commands

gringo4 --version
clasp3  --version
\end{itemize}
\section{Basic encoding}
\label{sec-3}

\begin{itemize}
\item Example: n-Queens puzzle, Section 3.2 in \footnotemark[1]{}
\begin{itemize}
\item \textbf{Note} \footnotemark[1]{} uses language of gringo 3, while we use the language of gringo 4 (cf \footnote{F. Calimeri, W. Faber, M. Gebser, G. Ianni, R. Kaminski, T. Krennwallner, N. Leone, F. Ricca, and T. Schaub: ASP-Core-2: Input language format. 2012.
Available at \url{https://www.mat.unical.it/aspcomp2013/files/ASP-CORE-2.0.pdf}.}).
\end{itemize}

\item Generate and Test Methodology
okular --presentation methodology.pdf
\end{itemize}

\subsection{Playground}
\label{sec-3-1}

\begin{itemize}
\item Files

view-file \href{queensB.lp4}{queensB.lp4} \footnote{We use extension lp4 to indicate encodings for gringo 4 (along the ASP-Core-2 standard \footnotemark[2]{})}

\begin{itemize}
\item queen(X,Y) indicates a queen on position (X,Y)
\end{itemize}

\item Commands

gringo4 queensB.lp4 -c n=4 | clasp3
gringo4 queensB.lp4 -c n=4 | clasp3 0

gringo4 queensB.lp4 -c n=4 --text
gringo4 queensB.lp4 -c n=4 --text | wc

gringo4 queensB.lp4 -c n=13 | clasp3
gringo4 queensB.lp4 -c n=14 | clasp3
\end{itemize}
\subsection{NB: Keep in mind that programs are normalized}
\label{sec-3-2}

\begin{itemize}
\item Files

view-file \href{queensB.lp4}{queensB.lp4}
view-file \href{queensBB.lp4}{queensBB.lp4}

\item Commands

gringo4 queensB.lp4  -c n=4 | clasp3 --stats
gringo4 queensBB.lp4 -c n=4 | clasp3 --stats

\begin{itemize}
\item Note: Both encodings result in the same constraints!
\end{itemize}
\end{itemize}
\subsection{NB: You may as well want to try gringo 3 for more (grounding) options:}
\label{sec-3-3}

\begin{itemize}
\item Files

view-file \href{queensB.lp}{queensB.lp}

\item Commands

gringo3 queensB.lp -c n=4 --text
gringo4 queensB.lp -c n=4 --text
\end{itemize}
\section{Advanced encoding}
\label{sec-4}

\begin{itemize}
\item Example: n-Queens puzzle, Section 8.1 in \footnotemark[1]{}
\begin{itemize}
\item Note: \footnotemark[1]{} uses language of gringo 3, while we use the language of gringo 4 (cf \footnotemark[2]{}).
\end{itemize}

\item Files

view-file \href{queensB.lp4}{queensB.lp4} \footnotemark[3]{}
view-file \href{queensA.lp4}{queensA.lp4} \footnotemark[3]{}

\item Commands

gringo4 queensB.lp4 -c n=2 --text
gringo4 queensA.lp4 -c n=2 --text

gringo4 queensB.lp4 -c n=14 | clasp3
gringo4 queensA.lp4 -c n=14 | clasp3

gringo4 queensB.lp4 -c n=14 | wc -l
gringo4 queensA.lp4 -c n=14 | wc -l

gringo4 queensB.lp4 -c n=14 | clasp3 --stats
gringo4 queensA.lp4 -c n=14 | clasp3 --stats
\end{itemize}

\subsection{NB: An even more succinct but identical advanced encoding}
\label{sec-4-1}

\begin{itemize}
\item Files

view-file \href{queensA.lp4}{queensA.lp4}
view-file \href{queensAA.lp4}{queensAA.lp4}

\item Commands

gringo4 queensAA.lp4 -c n=14 | clasp3 --stats
gringo4 queensA.lp4  -c n=14 | clasp3 --stats

\item Note: Both encodings result in the same constraints!
\end{itemize}
\subsection{NB: Keep in mind that clasp partly unfolds cardinality constraints}
\label{sec-4-2}

\begin{itemize}
\item Commands

gringo4 queensA.lp4 -c n=14 | wc -l
gringo4 queensA.lp4 -c n=14 | clasp3 --stats | grep Rules

gringo4 queensA.lp4 -c n=14 | clasp3 --stats --trans-ext=dynamic
gringo4 queensA.lp4 -c n=14 | clasp3 --stats --trans-ext=no
gringo4 queensA.lp4 -c n=14 | clasp3 --stats --trans-ext=all
\end{itemize}
\subsection{NB: You may as well want to try gringo 3 for more (grounding) options:}
\label{sec-4-3}

\begin{itemize}
\item Files

view-file \href{queensA.lp}{queensA.lp}

\item Commands

gringo3 queensA.lp -c n=4 --text
gringo4 queensA.lp -c n=4 --text
\end{itemize}
\section{Corrupted encoding}
\label{sec-5}

\begin{itemize}
\item Files

view-file \href{queensX.lp4}{queensX.lp4} \footnotemark[3]{}

\item Commands

gringo4 queensB.lp4 -c n=14 | wc -l
gringo4 queensA.lp4 -c n=14 | wc -l
gringo4 queensX.lp4 -c n=14 | wc -l
\end{itemize}
\section{Declarativity versus Scalability}
\label{sec-6}

\begin{itemize}
\item \textbf{Declarativity}

\begin{itemize}
\item ASP does separate a problem's representation from the algorithms used for solving it
\end{itemize}

\item \textbf{Scalability}

\begin{itemize}
\item \uline{Modeling} ASP does not separate a problem's representation from its induced combinatorics
\item \uline{Solving}  Boolean constraint technology is rather sensitive to search parameters
\end{itemize}

\item \textbf{Challenge}  Source code optimization! \footnote{M. Gebser, R. Kaminski, B. Kaufmann, and T. Schaub: Challenges in Answer Set Solving.
Essays Dedicated to Michael Gelfond on the Occasion of His 65th Birthday: 74--90. Springer, 2011
Available at \url{http://www.cs.uni-potsdam.de/wv/pdfformat/gekakasc11a.pdf}}
\end{itemize}
\section{More advanced encoding}
\label{sec-7}

\begin{itemize}
\item Example: n-Queens puzzle, Section 8.1 in \footnotemark[1]{}
\begin{itemize}
\item Note: \footnotemark[1]{} uses language of gringo 3, while we use the language of gringo 4 (cf \footnotemark[2]{}).
\end{itemize}

\item Files

view-file \href{queensA.lp4}{queensA.lp4} \footnotemark[3]{}
view-file \href{queensApre.lp4}{queensApre.lp4} \footnotemark[3]{}

\item Commands

gringo4 queensA.lp4    -c n=300 | clasp3 --quiet
gringo4 queensApre.lp4 -c n=300 | clasp3 --quiet

gringo4 queensA.lp4    -c n=300 | clasp3 --quiet --stats
gringo4 queensApre.lp4 -c n=300 | clasp3 --quiet --stats

\item Note: Both encodings result in the same constraints!
\end{itemize}
\section{Constraint-based encoding}
\label{sec-8}

\begin{itemize}
\item \textbf{NOTE} This is an experimental feature!

\item Background

\begin{itemize}
\item \uline{feature} 
\begin{itemize}
\item express finite linear constraint satisfaction problems
within ASP's modeling language and
\item solve them with off-the-shelf ASP solvers
\end{itemize}

\item \uline{language}
\begin{itemize}
\item All constraint relations and constraint variables are (currently) 
preceded by a dollar symbol

\item \#disjoint\{ term : value \}
\begin{itemize}
\item Idea: Sets of values labeled with the same term(s) must be disjoint :)
\end{itemize}
\end{itemize}

\item \uline{order encoding} \footnote{N. Tamura, A. Taga, S. Kitagawa, M. Banbara: Compiling finite linear CSP into SAT.
Constraints: 14(2):254-272, 2009.
Available at \url{http://springer.r.delivery.net/r/r?2.1.Ee.2Tp.1gRdFJ.BxsAdG..N.HAQa.38pS.CLWEcC00} (see also \url{http://bach.istc.kobe-u.ac.jp/sugar})}
\begin{itemize}
\item Idea: Introduce a Boolean variable for each statement 'X <= k' 
where X is a variable over integers and k is an integer bound
\end{itemize}
\end{itemize}

\item Files

view-file \href{queensC.clp}{queensC.clp} 
view-file \href{queensB.lp4}{queensB.lp4} \footnotemark[3]{}
view-file \href{queensApre.lp4}{queensApre.lp4} \footnotemark[3]{}

\item Commands

gringo4 queensC.clp -c n=10 | clasp3

gringo4 queensApre.lp4 -c n=300 | clasp3 --quiet
gringo4 queensC.clp    -c n=300 | clasp3 --quiet

gringo4 queensApre.lp4 -c n=300 | clasp3 --stats --quiet
gringo4 queensC.clp    -c n=300 | clasp3 --stats --quiet

gringo4 queensC.clp    -c n=300 | clasp3 --stats --quiet              | grep Constraints
gringo4 queensC.clp    -c n=300 | clasp3 --stats --quiet --sat-prepro | grep Constraints

gringo4 queensC.clp    -c n=300 | clasp3 --quiet             
gringo4 queensC.clp    -c n=300 | clasp3 --quiet --sat-prepro
\end{itemize}
\section{M}
\label{sec-9}

\begin{itemize}
\item Commands

gringo4 queensC.clp    -c n=1000 | clasp3 --stats --quiet
gringo4 queensApre.lp4 -c n=1000 | clasp3 --stats --quiet
gringo4 queensApre.lp4 -c n=1000 | clasp3 --stats --quiet --configuration=jumpy
\end{itemize}
% Emacs 24.3.1 (Org mode 8.2.3c)
\end{document}
