SUP is a native Answer Set Programming (ASP) solver that can be seen as a combination of computational ideas behind two ASP solvers: Cmodels and Smodels. Answer set solver Cmodels operates by computing a supported model M of the given logic program P, and then continuing this process, if necessary, in the presence of additional constraints expressed by loop formulas. Computing M is accomplished by forming the completion of P, clausifying it (at this step additional atoms can be introduced) and then invoking a SAT solver. Solver SUP operates in a similar way, by computing a sequence of supported models of P, but it does not form the completion of P. Instead, SUP applies Minisat (v1.12b) to P itself (with each rule written as a clause), and the "nonclausal constraint" mechanism of Minisat is employed for expressing the supportedness restriction. The new solver can be described as "Cmodels without completion." Computing a supported model of P without forming the completion formula can be also accomplished by running the Atleast algorithm of Smodels. Computing supported models using Minisat with nonclausal constraints can be thought of as an alternative implementation of Atleast (enhanced by learning). In this sense, SUP combines Smodels and Cmodels algorithms.

http://www.cs.utexas.edu/users/tag/sup/