Potassco - the Potsdam Answer Set Solving Collection

We have moved!

Our new web portal is at potassco.org.

Getting started

Answer Set Programming (ASP) offers a simple and powerful modeling language to solve combinatorial problems. With our tools you can concentrate on an actual problem, rather than a smart way of implementing it. Get started!

To get a quick first impression, you may want to experiment with running clingo in your browser.

Documentation

A comprehensive documentation of our software can be found in the Potassco guide.

Systems

clasp

clasp is an answer set solver for (extended) normal and disjunctive logic programs. It combines the high-level modeling capacities of 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).

Download Resources Article Citation

clasp is also available in Debian, Ubuntu, Arch Linux (AUR), and for Mac OS X in homebrew and macports.

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. Its output can be processed further with clasp, claspar, or claspfolio.

Attention! The languages of Gringo 3 and 4 are not fully compatible because Gringo 4 adheres to the recent ASP language standard. For processing legacy encodings, we recommend downloading the latest version of Gringo 3 in addition to Gringo 4.

Download Article Citation

gringo is also available in Debian, Ubuntu, Arch Linux (AUR), and for Mac OS X in homebrew and macports.

Development: The latest gringo source code is available on github.com/potasso/clingo. There are branches for each of the major releases.

Clingo

Clingo combines both gringo and clasp into a monolithic system. This way it offers more control over the grounding and solving process than gringo and clasp can offer individually - e.g., incremental grounding and solving. Clingo comes with its own version of claspD-2 and hence now supports parallel- and disjunctive solving.

Download Download (legacy version 2.x) Script API Reference Article Citation

clingo is also available in Debian, Ubuntu, Arch Linux (AUR), and for Mac OS X in homebrew and macports as part of gringo.

Development: The latest clingo source code is available on github.com/potasso/clingo. There are branches for each of the major releases.

Aspcud

Aspcud is a solver for package dependencies. A package universe and a request to install, remove, or upgrade packages have to be encoded in the CUDF format. Such a CUDF document can then be passed to aspcud along with an optimization criteria to obtain a solution to the given package problem.

Aspcud is available as a backend solver for apt-get in debian. More information can be found in the blog entry about using external solvers with apt-get. But if you want to get started quickly:

apt-get install apt-cudf
apt-get -s --solver aspcud install totem

aspcud is also available in Debian and Ubuntu.

Download Download (older versions) Mancoosi Homepage Citation

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.

Download Resources Article Citation

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.

Download Resources Article Citation

coala

Coala is a versatile compiler from action languages to answer set programs. It supports different encodings, variables and LTL style queries.

Download Resources Article Citation

Labs

The Labs suite comprises programs related to Answer Set Programming. These are either small utilities or projects in an early or unfinished development phase.

Cemetery

The Cemetery serves as an archive for superseded programs that belonged to the Potassco suite.