Answer set programming: Difference between revisions

Revision as of 06:48, 1 June 2021

Revision as of 12:25, 2 June 2021

Line 257:

==Comparison of implementations==

Early systems, such as Smodels, used [[backtracking]] to find solutions. As the theory and practice of [[Boolean SAT solver]]s 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 booleanBoolean-logic form. These approaches allow for significant improvements of performance, often by an order of magnitude, over earlier backtracking algorithms.

The [https://potassco.org/ 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.