NAME

       clasp - a conflict-driven nogood learning answer set solver

SYNOPSIS

       clasp [number][options]

DESCRIPTION

       This manual page documents briefly the clasp command.

       clasp  is an answer set solver for (extended) normal logic programs. It combines the high-
       level modeling capacities of answer set programming (ASP) with state-of-the-art techniques
       from  the  area  of  Boolean  constraint  solving.  The  primary clasp algorithm relies on
       conflict-driven  nogood  learning,  a  technique   that   proved   very   successful   for
       satisfiability  checking  (SAT). Unlike other learning ASP solvers, clasp does not rely on
       legacy software, such as a SAT solver or any other existing ASP solver. Rather, clasp  has
       been  genuinely developed for answer set solving based on conflict-driven nogood learning.
       clasp can be applied as an ASP solver (on LPARSE output  format),  as  a  SAT  solver  (on
       simplified DIMACS/CNF format), or as a PB solver (on OPB format).

OPTIONS

       These  programs  follow the usual GNU command line syntax, with long options starting with
       two dashes (`-').  A summary of options is included below.  For  a  complete  description,
       see <http://www.cs.uni-potsdam.de/clasp/>.

       -h, --help
              Show summary of options.

       -v, --version
              Show version of program.

SEE ALSO

       gringo(1).

AUTHOR

       clasp was written by Benjamin Kaufmann <kaufmann@cs.uni-potsdam.de>.

       This  manual  page  was  written  by  Thomas Krennwallner <tkren@kr.tuwien.ac.at>, for the
       Debian project (and may be used by others).

                                          March  4, 2010                                 CLASP(1)