clasp
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) or as a SAT solver (on DIMACS/CNF format).
The following competition results show that clasp is a very versatile solver and suitable for many applications:
- ASP Competition 2009
- 1st in all categories (for problems in the P category, clasp merely printed the unique solution computed by a grounder; unlike with most of the other teams, settings used by the Potassco team were geared towards benchmarks)
- SAT Competition 2009
- 1st in two categories (Crafted SAT+UNSAT and Crafted SAT)
- 2nd in one category (Crafted UNSAT)
- PB Evaluation 2009
- 1st in one category (optimization, small integers, linear constraints: UNSAT answers)
- 3rd in three categories
- ASP System Competition 2007
- 1st in two categories (SCore and SLparse)
- 3rd in one category (MGS)
- PB Evaluation 2007
- 1st in one category (PURE-SAT)
Download Documentation Resources
claspD
claspD is an extension of clasp that allows for solving disjunctive logic programs.
claspar
claspar is a parallelized version of clasp using MPI to distribute search.
Gringo
Current answer set solvers work on variable-free programs. Hence, a grounder is needed that, given an input program with first-order variables, computes an equivalent ground (variable-free) program. Gringo is such a grounder.
Clingo
Clingo stands for clasp on Gringo and combines both systems in a monolithic way. Its input language is that of Gringo and its output corresponds to that of clasp.
iClingo
iClingo is an incremental ASP system implemented on top of Clingo. It is based on the idea that the grounder as well as the solver are implemented in a stateful way. Thus, both keep their previous states while increasing an incremental parameter. As regards grounding, at each incremental step, the goal is to produce only ground rules stemming from the current program slice, without re-producing previous ground rules. The ground program slices are then gradually passed to the solver that accumulates ground rules and computes answer sets for them.
Download Documentation Resources
Clingcon
Clingcon is an answer set solver for constraint logic programs, building upon the answer set solver Clingo and the CSP solver Gecode. It extends the high-level modeling language of ASP with constraint solving capacities. Constraints over finite domain integer variables can be used in logic programs. Clingcon adopts state-of-the-art techniques from the area of SMT, like conflict-driven learning and theory propagation.
claspfolio
claspfolio is a portfolio solver for ASP that makes use of machine-learning techniques for performing algorithm selection, choosing among different configurations of clasp.
Potassco Labs
The Potassco Labs suite comprises programs related to Answer Set Programming. These are either small utilities or projects still under development.
