Answer Set Programming - Comparison of Implementations

Comparison of Implementations

Early systems, such as Smodels, used backtracking to find solutions. As the theory and practice of Boolean SAT solvers evolved, a number of ASP solvers were built on top of SAT solvers, including ASSAT and Cmodels. These converted ASP formula into SAT propositions, applied the SAT solver, and then converted the solutions back to ASP form. More recent systems, such as Clasp, use a hybrid approach, using conflict-driven algorithms inspired by SAT, without full converting into a boolean-logic form. These approaches allow for significant improvements of performance, often by an order of magnitude, over earlier backtracking algorithms.

The Potassco project acts as an umbrella for many of the systems below, including clasp, grounding systems (gringo), incremental systems (iclingo), constraint solvers (clingcon), action language to ASP compilers (coala), distributed MPI implementations (claspar), and many others.

Most systems support variables, but only indirectly, by forcing grounding, by using a grounding system such as Lparse or gringo as a front end. The need for grounding can cause a combinatorial explosion of clauses; thus, systems that perform on-the-fly grounding might have an advantage.

Platform Features Mechanics
Name OS Licence Variables Function symbols Explicit sets Explicit lists Disjunctive (choice rules) support
ASPeRiX Linux GPL Yes No on-the-fly grounding
ASSAT Solaris Freeware SAT-solver based
Clasp Answer Set Solver Linux, Mac OS, Windows GPL yes, in Clingo Yes No No Yes, in ClaspD Incremental, SAT-inspired (nogood, conflict-driven)
Cmodels Linux, Solaris GPL Requires grounding Yes Incremental, SAT-solver inspired (nogood conflict-driven)
DLV Linux, Mac OS, Windows free for academic and non-commercial educational use, and for non-profit organizations Yes Yes No No Yes Not Lparse compatible
DLV-Complex Linux, Mac OS, Windows Freeware Yes Yes Yes Yes Built on top of DLV - Not Lparse compatible
GnT Linux GPL Requires grounding Yes built on top of smodels.
nomore++ Linux GPL combined literal+rule-based
Platypus Linux, Solaris, Windows GPL Distributed, multi-threaded nomore++, smodels
Pbmodels Linux ? Pseudo-boolean solver based
Smodels Linux, Mac OS, Windows GPL Requires grounding No No No No
Smodels-cc Linux ? Requires grounding SAT-solver based; smodels w/conflict clauses.
Sup Linux ? SAT-solver based

Read more about this topic:  Answer Set Programming

Famous quotes containing the word comparison:

    He was a superior man. He did not value his bodily life in comparison with ideal things. He did not recognize unjust human laws, but resisted them as he was bid. For once we are lifted out of the trivialness and dust of politics into the region of truth and manhood.
    Henry David Thoreau (1817–1862)