Home
Experiments
Downloads

The claspD System

claspD is an answer set programming (ASP) solver for (extended) normal and disjunctive logic programs. Hence, it is able to deal with problems at the second level of the polynomial hierarchy. Conform to this complexity, claspD deploys a generate and test approach, both tasks implemented by way of clasp's core technology. Consequently, claspD incorporates many features that are nowadays standard in state-of-the-art SAT solvers (like chaff, berkmin, minisat, etc.), but which are rather unusual in the context of (disjunctive) ASP solving. Such techniques include:

  • conflict analysis via the First-UIP scheme
  • nogood recording and deletion
  • backjumping
  • restarts
  • conflict-driven decision heuristics
  • unit propagation via watched literals
  • dedicated propagation of binary and ternary nogoods
However, claspD is a genuine ASP solver. Its basic propagation engine includes advanced unfounded set checking based on source pointers. In fact, claspD is the first disjunctive ASP solver whose propagation engine is able (but not guaranteed) to detect non-singleton unfounded sets within non-head-cycle-free strongly connected components of a program's (positive) atom dependency graph. Furthermore, non-polynomial unfounded set checks are only applied if necessary, that is, when an exhaustive test of a non-head-cycle-free strongly connected component is needed.

To get an impression of claspD's performance, visit the benchmarking area.

For the system and a brief user introduction, visit the download area.

Finally, have a lot of fun running claspD!

Last change 2008/04/07