Reducing FASP to Fuzzy SAT
Jeroen Janssen, Steven Schockaert, Dirk Vermeir, Martine De Cock · Atlantis computational intelligence systems · 2012
In recent years, efficient solvers for classical ASP have been developed. Some of these are based on the DPLL algorithm (Davis and Putnam 1960) such as Smodels (Simons and Niemelä 2000) and DLV (Faber and Pfeifer 2005), others use ideas from SAT solving such as clasp (Gebser et al. 2009), while still others directly use SAT solvers to find answer sets, e.g. ASSAT (Lin and Zhao 2004), cmodels (Giunchiglia et al. 2004), and pbmodels (Liu and Truszczynski 2005). The SAT based approaches have been shown to be fast, and have the advantage that they can use the high number of efficient SAT solvers that have been released in recent years. The DPLL based solvers have the advantage that they allow a flexible modeling language, since they are not restricted to what can directly and efficiently be translated to SAT, and that they can be optimized for specific types of programs.