options.tex

\section{Command Line Options}\label{sec:options}

In this section, we briefly describe the meaning of
some selected command line options supported by
\gringo\ (Section~\ref{subsec:opt:gringo}),
\clingo\ (Section~\ref{subsec:opt:clingo}), and
\clasp\ (Section~\ref{subsec:opt:clasp}).
Each of these tools display their available options
when invoked with flag \code{--help} or \code{-h}.%
\footnote{%
  Note that our description of command line options
  is based on \gringo\ and \clingo\ series~4
  as well as \clasp\ series 3.
  While it is rather unlikely that command line options will
  disappear in future versions,
  additional ones might be introduced.
  We will try to keep this document up-to-date,
  but checking the help information shipped
  with a new version is always a good idea.}
The approach of distinguishing long options, starting with `\code{--}',
and short ones of the form `\code{-\textit{l}}',
where \code{\textit{l}} is a letter,
follows the GNU Coding Standards~\cite{GNUcoding}.
For obvious reasons,
short forms are made available only for the most common (long) options.
Some options, also called flags, do not take any argument,
while others require arguments.
An argument \code{\textit{arg}} is provided to a (long) option \code{\textit{opt}}
by writing
`\code{--\textit{opt}=\textit{arg}}' or
`\code{--\textit{opt} \textit{arg}}',
while only
`\code{-\textit{l} \textit{arg}}'
is accepted for a short option \code{\textit{l}}.
For each command line option,
we below indicate whether it requires an argument,
and if so, we also describe its meaning.


\subsection{\gringo\ Options}\label{subsec:opt:gringo}

An abstract invocation of \gringo\ looks as follows:
%
\begin{lstlisting}[numbers=none]
gringo [ options | files ]
\end{lstlisting}
%
Note that options and filenames do not need to be passed to \gringo\
in any particular order.
If neither a filename nor an option that makes \gringo\ exit (see below)
is provided, \gringo\ reads from the standard input.
In the following, we list and describe the options accepted by \gringo\
along with their particular arguments (if required):
%
\begin{description}
\item[\code{--help,-h}]~\\
Print help information and exit.
\item[\code{--version,-v}]~\\
Print version information and exit.
\item[\code{--verbose[=n],-V}]~\\
Print additional (progress) information during computation.
Verbosity level one and two are currently not used by \gringo.
The flag implies level three.
Level three prints internal representations of the logic program.
\item[\code{--const,-c \textit{c}=\textit{t}}]~\\
Replace occurrences (in the input program) of constant~\code{\textit{c}} with term~\code{\textit{t}}.
This overrides constant definitions in a source file without a warning.
\item[\code{--text,-t}]~\\
Output ground program in (human-readable) text format.
\item[\code{--lparse-rewrite}]~\\
Can be used in conjunction with the \code{--text} option to print a program in a (human-readable) similar to the \smodels\ format,
which is otherwise passed to the solver.
\item[\code{--lparse-debug=\{none,plain,lparse,all\}}]~\\
This option enables additional debugging output to the standard error stream.
The available arguments are:
\begin{description}[leftmargin=2cm,style=nextline,align=right,font=\code]
  \item[none]  No additional output is printed.
  \item[plain] Prints rules as with~\code{--text} but prefixed with~\code{\%}.
  \item[lparse] Prints rules as with~\code{--text} and~\code{--lparse-rewrite} but prefixed with~\code{\%\%}.
  \item[all] Combines argument \code{plain} and \code{lparse}.
\end{description}

\item[\code{--warn,-W [no-]w}]
This option can be used to enable and disable warnings.
To disable a warning, the argument has to prefixed with \code{no-}.
To enable or disable multiple warnings, this option can be passed multiple times with different arguments.
By default all warnings are enabled.
The available values for argument \code{w} are:
\begin{description}[leftmargin=6cm,style=nextline,align=right,font=\code]
  \item[file-included]       See Section~\ref{sec:warn:incfile}.
  \item[variable-unbounded]  See Section~\ref{sec:warn:unbound}.
  \item[operation-undefined] See Section~\ref{sec:warn:undefterm}.
  \item[atom-undefined]      See Section~\ref{sec:warn:undefatm}.
  \item[global-variable]     See Section~\ref{sec:warn:global}.
\end{description}
\end{description}
%
When calling \gringo\ without options,
it outputs a ground program in \smodels\ format~\cite{lparseManual},
which is a common input language for propositional ASP solvers.

\subsection{\clingo\ Options}\label{subsec:opt:clingo}
ASP system \clingo\ combines grounder \gringo\ and solver \clasp\
via an internal interface.
An abstract invocation of \clingo\ looks as follows:
%
\begin{lstlisting}[numbers=none]
clingo [ options | files | number ]
\end{lstlisting}
%
The optional numerical argument allows for specifying the maximum number of answer sets to be computed (\code{0}~standing for all answer sets).
As with \gringo,
the number, options, and filenames do not need to be passed to \clingo\ in any particular order.
Given that \clingo\ combines \gringo\ and \clasp,
it accepts all options described in the previous section and in Section~\ref{subsec:opt:clasp}.
In particular,
(long) options \code{--help} and \code{--version} make \clingo\ print the desired information and exit,
while \code{--text} instructs \clingo\ to output a ground program (rather than solving it) like \gringo.
If neither a filename nor an option that makes \clingo\ exit (see Section~\ref{subsec:opt:gringo}) is provided,
\clingo\ reads from the standard input.
Beyond the options described in Section~\ref{subsec:opt:gringo} and~\ref{subsec:opt:clasp},
\clingo\ has a single additional option:
%
\begin{description}
\item[\code{--mode=m}]~\\
Choose the mode in which \clingo\ should run.
Available values for \code{m} are:
\begin{description}[leftmargin=2cm,style=nextline,align=right,font=\code]
  \item[clingo] Explicitly select \clingo\ mode (the default).
  \item[gringo] In this mode \clingo\ behaves like \gringo.
  \item[lparse] In this mode \clingo\ behaves like \clasp.
\end{description}

\end{description}
%
Finally, the default command line when invoking \clingo\
consists of all \clasp\ defaults (cf.\ Section~\ref{subsec:opt:clasp}).

\subsection{\clasp\ Options}\label{subsec:opt:clasp}
Stand-alone \clasp~\cite{gekanesc07b} is an ASP solver for ground logic programs
that can also be used as a SAT, MaxSAT, or PB solver (cf.\ Section~\ref{subsec:lang:clasp}).
An abstract invocation of \clasp\ looks as follows:
%
\begin{lstlisting}[numbers=none]
clasp [ options | files | number ]
\end{lstlisting}
%
As with \clingo\ and \iclingo,
a numerical argument specifies the maximum number of answer sets to be computed,
where \code{0}~stands for all answer sets.
(The number of requested answer sets can likewise be set via long option
 \code{--models} or its short form~\code{-n}.)
If neither a filename nor an option that makes \clasp\ exit (see below) is provided,
\clasp\ reads from the standard input.%
\footnote{%
 In earlier versions of \clasp, filenames had to be given via option \code{--file}
 or its short form~\code{-f}.}
In fact, it is typical to use \clasp\ in a pipe with \gringo\ in the following way:
\begin{lstlisting}[numbers=none]
gringo [ options | files ] | clasp [ options | number ]
\end{lstlisting}
In such a pipe, \gringo\ instantiates an input program and outputs the ground
rules in \smodels\ format,
which is then fed to \clasp\ that computes and outputs answer sets.
Note that \clasp\ offers plenty of options to configure its behavior.
In the following, we present only some important options
and categorize them according to their functionalities.

\subsubsection{General Options}\label{subsec:clasp:general}
We below group some general options of \clasp,
used to configure its global behavior.
\begin{description}
  \item[\code{--help[=\textit{n}],-h}]~\\
    Print help information and exit.\\
    Argument~\code{\textit{n}} determines the level
    of detail that is shown. If~\code{\textit{n}} is not given
    or is equal to $1$, only major options are shown. Level
    \code{\textit{n}=2} also prints advanced search options. Finally,
    \code{\textit{n}=3} prints the full help information.
  \item[\code{--version,-v}]~\\
    Print version information and exit.
    The version information also includes
    whether or not \clasp\ was built with support for
    parallel solving via multithreading.
  \item[\code{--verbose[=\textit{n}],-V}]~\\
    Configure printing of (progress) information during computation.
    Argument \code{\textit{n}}=\code{0} disables progress information, while
    \code{\textit{n}}=\code{1} and \code{\textit{n}}=\code{2} print basic information.
    Extended information is printed for \code{\textit{n}}$\code{>}$\code{2}, where levels \code{4} and \code{5}
    are only relevant when solving disjunctive logic programs.
    Finally, the flag \code{-V} implies the largest available verbosity level.
  \item[\code{--outf=\textit{n}}]~\\
    Configure output format. Available values for \code{\textit{n}} include
    \code{0} for \clasp's default output format, \code{1} for
    solver competition (ASP, SAT, PB) output, and \code{2} for
    output in JSON\footnote{\url{http://json.org/}} format.
  \item[\code{--quiet[=\textit{models}[,\textit{costs}][,\textit{calls}]],-q}]~\\
    Configure printing of computed models, associated costs (in case of optimization), and individual call statistics (for multi-shot solving).
    Arguments are integers in the range \code{0..2},
    where \code{0} means print all, \code{1} means print last, and \code{2} means do not print any models, costs, or individual call statistics.
    If \code{--quiet} or \code{-q} is given as a flag, all arguments are implicitly set to \code{2}.
  \item[\code{--stats[=\{1,2\}],-s}]~\\
    Maintain and print basic (\code{1}) or extended (\code{2}) statistic information.
  \item[\code{--time-limit=\textit{t}}]~\\
    Force termination after \code{\textit{t}} seconds.
  \item[\code{--solve-limit=\textit{n}[,\textit{m}]}]~\\
    Force termination after either \code{\textit{n}} conflicts or \code{\textit{m}} restarts.
  \item[\code{--pre}]~\\
    Run ASP preprocessor then print preprocessed input program and exit.
  \item[\code{--print-portfolio}]~\\
    Print default portfolio and exit (cf. \code{--parallel-mode}).
\end{description}

\subsubsection{Solving Options}\label{subsec:clasp:solving}
The options listed below can be used to configure
the main solving and reasoning strategies of \clasp.
\begin{description}
  \item[\code{--models,-n \textit{n}}]~\\
    Compute at most~\code{\textit{n}} models,
    \code{\textit{n}}=\code{0} standing for compute all models.
  \item[\code{--project}]~\\
    Project answer sets to named atoms and only enumerate unique projected solutions~\cite{gekasc09a}.
  \item[\code{--enum-mode,-e \textit{mode}}]~\\
    Configure enumeration algorithm applied during solving.
    Available values for \code{\textit{mode}} are:
    \begin{description}[leftmargin=2.1cm,style=nextline,align=right,font=\code]
      \item[bt]       Enable backtrack-based enumeration~\cite{gekanesc07c}.
      \item[record]   Enable enumeration based on solution recording. Note that this  mode is prone to blow up
                      in space in view of an exponential number of solutions in the worst case.
      \item[domRec]   Enable subset enumeration via domain-based recording (cf.\ Section~\ref{sec:heuristic}).
      \item[brave]    Compute the brave consequences (union of all answer sets) of a logic program.
      \item[cautious] Compute the cautious consequences (intersection of all answer sets) of a logic program.
      \item[auto]     Use \code{bt} for enumeration and \code{record} for optimization.
    \end{description}
    Note: The option is only meaningful if \code{--models} is not equal to \code{1}. Furthermore,
    modes \code{brave} and \code{cautious} require \code{--models=0}, which is also the default in that case.
  \item[\code{--opt-mode=\textit{mode}}]~\\
    Configure handling of optimization statements.
    Available values for \code{\textit{mode}} are:
    \begin{description}[leftmargin=1.6cm,style=nextline,align=right,font=\code]
      \item[opt]      Compute an optimal model (requires \code{--models=0}).
      \item[enum]     Enumerate models with costs less than or equal to some fixed bound (cf. \code{--opt-bound}).
      \item[optN]     Compute optimum, then enumerate optimal models.
      \item[ignore]   Ignore any optimization statements during computation.
    \end{description}
  \item[\code{--opt-bound=\textit{n1}[,\textit{n2},\textit{n3}...]}]~\\
  Initialize objective function(s) to minimize with \code{\textit{n1}[,\textit{n2},\textit{n3}...]}.
  \item[\code{--opt-sat}]~\\
    Treat input in DIMACS-(w)cnf format as MaxSAT optimization problem.

  \item[\code{--parallel-mode,-t \textit{n}[,\textit{mode}]}]~\\
    Enable parallel solving with \textit{n} threads~\cite{gekasc12b}, where
    \textit{mode} can be either \code{compete} for competition-based (portfolio) search
    or \code{split} for splitting-based search via distribution of guiding paths.
\end{description}

\subsubsection{Fine-Tuning Options}\label{subsec:clasp:tune}

The following incomplete list of options can be used to
fine-tune certain aspects of \clasp.
For a complete list of options,
call \clasp\ with option \code{--help=3}.
\begin{description}
  \item[\code{--configuration=\textit{c}}]~\\
    Use \textit{c} as default configuration, where \textit{c} can be:
    \begin{description}[leftmargin=1.6cm,style=nextline,align=right,font=\code]
      \item[frumpy] Use conservative defaults similar to those used in earlier \clasp\ versions.
      \item[jumpy]  Use more aggressive defaults.
      \item[tweety] Use defaults geared towards typical ASP problems.
      \item[trendy] Use defaults geared towards industrial problems.
      \item[crafty] Use defaults geared towards crafted problems.
      \item[handy]  Use defaults geared towards large problems.
      \item[<file>] Use configuration file to configure solver(s).
    \end{description}
    Note that using a configuration file enables freely configurable
    solver portfolios in parallel solving. For an example of such a portfolio,
    call \clasp\ with option \code{--print-portfolio}.
  \item[\code{--opt-strategy=\{bb,usc\}[,\textit{n}]}]~\
    Configure optimization strategy. Use either
    branch-and-bound-based optimization~\cite{gekakasc11c} (\code{bb}) or
    unsatisfiable-core-based optimization~\cite{ankamasc12a} (\code{usc}).
    The optional argument \textit{n} can be used to fine-tune the selected strategy.
    For example, \code{bb,1} enables hierarchical (multi-criteria) optimization~\cite{gekakasc11c},
    while \code{usc,1} enables some form of preprocessing during unsatisfiable-core-based optimization.
    For further details, call \clasp\ with option \code{--help=2}.
    Finally, note that the optimization strategy can be set on a per-solver basis
    in the context of parallel solving, thus allowing for optimization portfolios.
  \item[\code{--restart-on-model}]~\\
    Restart the search after finding a model.
    This is mainly useful during optimization because
    it often ameliorates the convergence to an optimum.

  \item[\code{--heuristic=\{Berkmin,Vmtf,Vsids,Unit,None,Domain\}}]~\\
    Use \emph{BerkMin}-like decision heuristic~\cite{golnov02a}
    (with argument~\code{Berkmin}),
    \emph{Siege}-like decision heuristic~\cite{ryan04a}
    (with argument~\code{Vmtf}),
    \emph{Chaff}-like decision heuristic~\cite{momazhzhma01a}
    (with argument~\code{Vsids}),
    \emph{Smodels}-like decision heuristic~\cite{siniso02a}
    (with argument~\code{Unit}),
    or (arbitrary) static variable ordering
    (with argument~\code{None}).
    Finally, argument~\code{Domain} enables
    a \emph{domain-specific} decision heuristic as described in Section~\ref{sec:heuristic}.
  \item[\code{--save-progress[=\textit{n}]}]~\\
    Enable alternative sign heuristic based on cached truth values~\cite{pipdar07a} if available.
    Cache truth values on backjumps $>$ \code{\textit{n}}.
  \item[\code{--restarts,-r \textit{sched}}]~\\
    Choose and parameterize a restart policy, where \textit{sched} can be:
    \begin{description}[leftmargin=1.6cm,style=nextline,align=right,font=\code]
      \item[no] Disable restarts.
      \item[F,\textit{n}] Run fixed sequence, restarting every \code{\textit{n}} conflicts.
      \item[*,\textit{n},\textit{f}] Run a geometric sequence~\cite{eensor03a},
                                     restarting every $\code{\textit{n}}*\code{\textit{f}}^i$ conflicts,
                                     where~$i$ is the number of restarts performed so far.
      \item[+,\textit{n},\textit{m}] Run an arithmetic sequence,
                                     restarting every $\code{\textit{n}}+\code{\textit{m}}*i$ conflicts,
                                     where~$i$ is the number of restarts performed so far.
      \item[L,\textit{n}] Restart search after a number of conflicts determined by a universal sequence~\cite{lusizu93a}, where \code{\textit{n}}
                          constitutes the base unit.
      \item[D,\textit{n},\textit{f}] Use a dynamic policy similar to the one of \sysfont{glucose}~\cite{audsim09b}.
      Given the $\code{\textit{n}}$ most recently learned conflict clauses and their average quality $\code{\textit{Qn}}$,
      a restart is triggered if $\code{\textit{Qn}}*\code{\textit{f}} > \code{\textit{Q}}$, where $\code{\textit{Q}}$
      is the global average quality.
    \end{description}
    The geometric and arithmetic sequences take an optional limit $\code{\textit{lim}} > 0$
    to enable a nested policy~\cite{biere08a}. If given,
    the sequence is repeated after $\code{\textit{lim}}+j$ restarts,
    where~$j$ counts how often the sequence has been repeated so far.

  \item[\code{--eq=\textit{n}}]~\\
    Run equivalence reasoning~\cite{gekanesc08a} for \code{\textit{n}} iterations,
    $\code{\textit{n}}=\code{-1}$ and $\code{\textit{n}}=\code{0}$ standing for
    run to fixpoint or do not run equivalence reasoning, respectively.
  \item[\code{--trans-ext=\{choice,card,weight,scc,integ,dynamic,all,no\}}]
    Compile extended rules~\cite{siniso02a} into normal rules (cf.~Section~\ref{subsec:gringo:normal}).
    Arguments \code{choice},  \code{card}, and \code{weight}
    state that all ``choice rules'', ``cardinality rules'' or ``weight rules'', respectively,
    are to be compiled into normal rules,
    while \code{all} means that all extended rules and \code{no} that none of them
    are subject to compilation. If argument \code{dynamic} is given,
    \clasp\ heuristically decides whether or not to compile individual
    ``cardinality'' and ``weight rules''.
    Finally, \code{scc} limits compilation to recursive ``cardinality'' and ``weight rules'',
    while \code{integ} only compiles those ``cardinality rules'' that are integrity constraints.
  \item[\code{--sat-prepro[=\{0,1,2,3\}][,\textit{x1}]...[,\textit{x5}]}]~\\
    Configure \emph{SatElite}-like preprocessing~\cite{eenbie05a}.
    Argument \code{0} (or \code{no}) means that \emph{SatElite}-like preprocessing is not to be run at all,
    while \code{1} enables basic preprocessing and \code{2} and \code{3} successively enable more
    advanced preprocessing including, for example, blocked clause elimination~\cite{jabihe10a}.
    If \code{--sat-prepro} is given as a flag, \code{2} is assumed.
    The optional arguments $\code{\textit{x1}},\ldots,\code{\textit{x5}}$ can be used
    to set fine grained limits, for example, regarding iterations and runtime.
    For further details, call \clasp\ with option \code{--help=2}.

\end{description}

Let us note that switching the above options can have dramatic effects
(both positively and negatively) on the search performance of \clasp.
If performance bottlenecks are observed, it is worthwhile to first
give the different prefabricated default configurations a try (cf.\ \code{--configuration}).
Furthermore, we suggest trying different heuristics and restart sequences.
For a brief overview on manual fine-tuning, see \cite{gekasc09b}.
Automatic configuration methods are described in Section~\ref{sec:configuration}.


%%% Local Variables:
%%% mode: latex
%%% TeX-master: "guide"
%%% End: