% Created 2014-06-22 Sun 10:58
\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\\ \url{torsten@cs.uni-potsdam.de}\\ \url{http://potassco.sourceforge.net/videos.html}}
\date{\today}
\title{Optimization in clasp 3\thanks{BIG thanks to Martin Gebser for pimping the encodings!}}
\hypersetup{
  pdfkeywords={},
  pdfsubject={},
  pdfcreator={Emacs 24.3.1 (Org mode 8.2.3c)}}
\begin{document}

\maketitle
\tableofcontents

\section{Encoding}
\label{sec-1}
\subsection{Systems}
\label{sec-1-1}

\begin{itemize}
\item \uline{commands}
gringo4 --version
clasp3  --version
\end{itemize}
\subsection{Basic encoding}
\label{sec-1-2}

\begin{itemize}
\item Example: Traveling Sales Person, Section 3.3 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}}
\begin{itemize}
\item \textbf{Note} \footnotemark[1]{} uses language of gringo 3
\item See also \url{http://en.wikipedia.org/wiki/Travelling_salesman_problem}
\end{itemize}

\item \uline{commands}

\begin{itemize}
\item problem instance
view-file \href{graph.lp}{graph.lp} 
view-file \href{costs.lp}{costs.lp}

\item problem encoding
view-file \href{tsp.lp4}{tsp.lp4} \footnote{We use extension lp4 to indicate encodings for gringo 4 (along the ASP-Core-2 standard \footnotemark)}\footnotetext[3]{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}.}

\item problem solving
gringo4 tsp.lp4 graph.lp costs.lp | clasp3
\end{itemize}
\end{itemize}
\subsection{Optimization phases}
\label{sec-1-3}

\begin{itemize}
\item Branch and bound (top-down)
\begin{enumerate}
\item converging to optimum (SAT \ldots{} SAT)
\item prove optimiality  (UNSAT)
\end{enumerate}

\item Unsatisfiable core driven (bottom-up; cf \footnote{B. Andres, B. Kaufmann, O. Mattheis and T. Schaub: Unsatisfiability-based optimization in clasp. 
ICLP: 212-221, 2012.
Available at \url{http://www.cs.uni-potsdam.de/wv/pdfformat/ankamasc12a.pdf}})
\begin{enumerate}
\item identify and relax cores (UNSAT \ldots{} UNSAT)
\item until consistency (SAT)
\end{enumerate}
\end{itemize}
\subsection{clasp output}
\label{sec-1-4}

\begin{itemize}
\item option 

--quiet[=<m>,<o>],-q    : Configure printing of models and optimize values
   <m>: print \{0=all|1=last|2=no\} models
   <o>: print \{0=all|1=last|2=no\} optimize values [<m>]

\begin{itemize}
\item \uline{commands}

gringo4 tsp.lp4 graph.lp costs.lp | clasp3 --quiet=0,0
gringo4 tsp.lp4 graph.lp costs.lp | clasp3 --quiet=1,0
gringo4 tsp.lp4 graph.lp costs.lp | clasp3 --quiet=2,0
\end{itemize}
\end{itemize}
\subsection{More demanding instance}
\label{sec-1-5}

\begin{itemize}
\item Example: Clumpy graphs \footnote{J. Ward, J. Schlipf: Answer Set Programming with Clause Learning. 
LPNMR: 302-313, 2004.}

\item \uline{commands}
gringo4 clumpy-08x08$_{\text{06}}$.lp tsp.lp4 | clasp3 --quiet=2,0
\end{itemize}
\subsection{Advanced encoding}
\label{sec-1-6}

\begin{itemize}
\item Example: Traveling Sales Person, Section 8.3 in \footnotemark[1]{}
\begin{itemize}
\item \textbf{Note} \footnotemark[1]{} uses language of gringo 3
\end{itemize}
\end{itemize}

\subsubsection{Encodings}
\label{sec-1-6-1}

\begin{itemize}
\item \uline{commands}
view-file \href{tsp.lp4}{tsp.lp4} \footnotemark[2]{}
view-file \href{tspA.lp4}{tspA.lp4} \footnotemark[2]{}
\begin{itemize}
\item \textbf{ATTENTION} Objective value is different (though optimum models remain the same)!
\end{itemize}
\end{itemize}
\subsubsection{Explanation}
\label{sec-1-6-2}

Consider node 1:
\begin{verbatim}

edge(1,4). cost(1,4,1).            % <<< lowest cost edge
edge(1,2). cost(1,2,2).
edge(1,3). cost(1,3,3).

order(1,1,2).
order(1,2,3).

               %  cycle(1,4)         no penalty     
penalty(1,1,1) :- cycle(1,2).      %    penalty of one
penalty(1,2,1) :- cycle(1,3).      %    penalty of one ...
penalty(1,1,1) :- penalty(1,2,1).  %      ... plus one

#minimize{ 1,.. : penalty(1,1,1), 1,.. : penalty(1,2,1), ... }.

\end{verbatim}
\subsubsection{Solving}
\label{sec-1-6-3}

gringo4 tsp.lp4  graph.lp costs.lp  | clasp3 
gringo4 tspA.lp4 graph.lp costs.lp  | clasp3 

gringo4 tsp.lp4  clumpy-08x08$_{\text{06}}$.lp | clasp3 --quiet=2,0
gringo4 tspA.lp4 clumpy-08x08$_{\text{06}}$.lp | clasp3 --quiet=2,0

gringo4 tsp.lp4  clumpy-08x08$_{\text{10}}$.lp | clasp3 --quiet=2,0
gringo4 tspA.lp4 clumpy-08x08$_{\text{10}}$.lp | clasp3 --quiet=2,0
\subsubsection{Important note}
\label{sec-1-6-4}

ALWAYS GET THE ENCODING RIGHT AT FIRST!
YOU CAN NEVER RECOVER FROM A BAD ENCODING!
\subsection{More demanding instance, continued}
\label{sec-1-7}

\begin{itemize}
\item \uline{commands}  
gringo4 clumpy-08x08$_{\text{10}}$.lp tspA.lp4 $>$ tspA10
clasp3 tspA10 --quiet=2,0
\end{itemize}
\section{Solving}
\label{sec-2}
\subsection{Options for optimization}
\label{sec-2-1}

\begin{itemize}
\item \uline{commands} (use less on shell ;)
clasp3 --help=3 > helper

\item view-file \href{helper}{helper}
\end{itemize}
\subsection{Progress saving}
\label{sec-2-2}

\begin{itemize}
\item See \footnote{K. Pipatsrisawat, A. Darwiche: A lightweight component caching scheme for satisfiability solvers.
SAT: 294-299, 2007.}

\item view-file \href{helper}{helper}

\item \uline{commands}

clasp3 tspA10 --quiet=2,0 --save-progress=0
clasp3 tspA10 --quiet=2,0 --save-progress=1

\item view-file \href{ham.lp4}{ham.lp4}
\item view-file \href{hamO.lp4}{hamO.lp4}

\item \uline{commands}  

gringo4 hamO.lp4 clumpy-08x08$_{\text{10}}$.lp | clasp3 --quiet=2,0 --save-progress=1
gringo4 hamO.lp4 clumpy-08x08$_{\text{10}}$.lp | clasp3 --quiet=2,0 --save-progress=0
gringo4 hamO.lp4 clumpy-08x08$_{\text{10}}$.lp | clasp3 --quiet=2,0 --save-progress=0 --restart-on-model
\end{itemize}
\subsection{Optimization strategies}
\label{sec-2-3}

\begin{itemize}
\item view-file \href{helper}{helper}

\item \uline{commands}  

clasp3 tspA10 --quiet=2,0 --opt-strategy=0 
clasp3 tspA10 --quiet=2,0 --opt-strategy=2
clasp3 tspA10 --quiet=2,0 --opt-strategy=3
clasp3 tspA10 --quiet=2,0 --opt-strategy=4 \footnotemark[4]{}
clasp3 tspA10 --quiet=2,0 --opt-strategy=5

\item \uline{commands}  

gringo4 ham.lp4  clumpy-08x08$_{\text{10}}$.lp | clasp3 --quiet=2,0

gringo4 hamO.lp4 clumpy-08x08$_{\text{10}}$.lp | clasp3 --quiet=2,0 --opt-strategy=0 
gringo4 hamO.lp4 clumpy-08x08$_{\text{10}}$.lp | clasp3 --quiet=2,0 --opt-strategy=2 
gringo4 hamO.lp4 clumpy-08x08$_{\text{10}}$.lp | clasp3 --quiet=2,0 --opt-strategy=3 
gringo4 hamO.lp4 clumpy-08x08$_{\text{10}}$.lp | clasp3 --quiet=2,0 --opt-strategy=4 

gringo4 hamO.lp4 clumpy-16x16$_{\text{10}}$.lp | clasp3 --quiet=2,0 --opt-strategy=0 
gringo4 hamO.lp4 clumpy-16x16$_{\text{10}}$.lp | clasp3 --quiet=2,0 --opt-strategy=4
\end{itemize}

\subsubsection{Multi-criteria optimization}
\label{sec-2-3-1}

\begin{itemize}
\item view-file \href{tspMO.lp4}{tspMO.lp4} (see \href{hamO.lp4}{hamO.lp4})

\item \uline{commands}  

gringo4 tspMO.lp4 clumpy-08x08$_{\text{10}}$.lp | clasp3 --quiet=2,0 --opt-strategy=0
gringo4 tspMO.lp4 clumpy-08x08$_{\text{10}}$.lp | clasp3 --quiet=2,0 --opt-strategy=1
\end{itemize}
\subsection{Optimization heuristics}
\label{sec-2-4}

\begin{itemize}
\item view-file \href{helper}{helper}

\item \uline{commands}  
clasp3 tspA10 --quiet=2,0 --opt-heuristic=1
clasp3 tspA10 --quiet=2,0 --opt-heuristic=2
clasp3 tspA10 --quiet=2,0 --opt-heuristic=3
\end{itemize}
\subsection{Structure-specific heuristics}
\label{sec-2-5}

\begin{itemize}
\item See \footnote{M. Gebser, B. Kaufmann, R. Otero, J. Romero, T. Schaub and P. Wanko: Domain-specific Heuristics in Answer Set Programming. 
AAAI: 350-356, 2013.
Available at \url{http://www.cs.uni-potsdam.de/wv/pdfformat/gekaotroscwa13a.pdf}}

\item view-file \href{helper}{helper}

\item \uline{commands}  
clasp3 tspA10 --quiet=2,0 --heuristic=domain --dom-pref=16 --dom-mod=4
clasp3 tspA10 --quiet=2,0 --heuristic=domain --dom-pref=16 --dom-mod=5
\end{itemize}
\subsection{Domain-specific heuristics}
\label{sec-2-6}

\begin{itemize}
\item See \footnotemark[7]{}

\item \uline{commands} 
gringo4  clumpy-08x08$_{\text{10}}$.lp tspA.lp4          | clasp3 --heuristic=domain --quiet=2,0
gringo4  clumpy-08x08$_{\text{10}}$.lp tspA.lp4 tspH.lp4 | clasp3 --heuristic=domain --quiet=2,0
\end{itemize}
\subsection{Parallel optimization}
\label{sec-2-7}

\begin{itemize}
\item view-file \href{helper}{helper}

\item \uline{commands}
\begin{itemize}
\item auto configuration
clasp3 --print-portfolio
clasp3 tspA10 --quiet=2,0                                         --parallel-mode=4,compete

\item homogeneous configuration
clasp3 tspA10 --quiet=2,0 --configuration=tweety --opt-strategy=0 --parallel-mode=4,compete

\item customized configuration
view-file \href{optfolio-heterogeneous}{optfolio-heterogeneous}
clasp3 tspA10 --quiet=2,0 --configuration=optfolio-heterogeneous  --parallel-mode=4,compete
\end{itemize}
\end{itemize}
\subsection{Another example}
\label{sec-2-8}

\begin{itemize}
\item Example: Ricochet Robots \footnote{M. Gebser, H. Jost, R. Kaminski, P. Obermeier, O. Sabuncu, T. Schaub and M. Schneider: Ricochet Robots: A transverse ASP benchmark. 
LPNMR: 348-360, 2013.
Available at \url{http://www.cs.uni-potsdam.de/wv/pdfformat/gejokaobsascsc13a.pdf}}
See also \url{http://en.wikipedia.org/wiki/Ricochet_Robot}
Fix horizon to 15 and try to find a minimum number of moves to reach target position (viz -c goal=4)

\item \uline{commands}
view-file \href{RR/robotsN.lp4}{RR/robotsN.lp4} \footnotemark[2]{}

gringo4 RR/board16-1.lp RR/robots.lp RR/goals16-1.lp RR/robotsN.lp4 -c horizon=15 -c goal=4 > rico16hor15goal4
clasp3 rico16hor15goal4 --quiet=2,0 --opt-strategy=0
clasp3 rico16hor15goal4 --quiet=2,0 --opt-strategy=2
clasp3 rico16hor15goal4 --quiet=2,0 --opt-strategy=3
clasp3 rico16hor15goal4 --quiet=2,0 --opt-strategy=4
clasp3 rico16hor15goal4 --quiet=2,0 --opt-strategy=5
\end{itemize}
% Emacs 24.3.1 (Org mode 8.2.3c)
\end{document}
