clasp - a conflict-driven nogood learning answer set solver
clasp [
number] [
options]
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).
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.potassco.org/clasp/>.
- -h, --help
- Show summary of options.
- -v, --version
- Show version of program.
gringo(1).
clasp was written by Benjamin Kaufmann <
[email protected]>.
This manual page was written by Thomas Krennwallner
<
[email protected]>, for the Debian project (and may be used by
others).