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 words comparison of and/or comparison:
“When we reflect on our past sentiments and affections, our thought is a faithful mirror, and copies its objects truly; but the colours which it employs are faint and dull, in comparison of those in which our original perceptions were clothed.”
—David Hume (1711–1776)
“But the best read naturalist who lends an entire and devout attention to truth, will see that there remains much to learn of his relation to the world, and that it is not to be learned by any addition or subtraction or other comparison of known quantities, but is arrived at by untaught sallies of the spirit, by a continual self-recovery, and by entire humility.”
—Ralph Waldo Emerson (1803–1882)