Bug#605877: ITP: clasp -- A conflict-driven nogood learning answer set solver

[Thomas Krennwallner <tkren@kr.tuwien.ac.at>]

Package: wnpp
Severity: wishlist
Owner: Thomas Krennwallner <tkren@kr.tuwien.ac.at>


* Package name    : clasp
  Version         : 1.3.6
  Upstream Author : Benjamin Kaufmann <kaufmann@cs.uni-potsdam.de>
* URL             : http://www.cs.uni-potsdam.de/clasp/
* License         : GPL
  Programming Lang: C++
  Description     : A conflict-driven nogood learning answer set solver

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 SMODELS format, as output by Gringo), as a SAT
solver (on a simplified version of DIMACS/CNF format), or as a PB
solver (on OPB format).