ASSAT
ASSAT (Answer Sets by SAT solvers) is a system for computing answer sets of a logic program by using SAT solvers. Briefly speaking, given a ground logic program P, ASSAT(X), depending on the SAT solver X used, works as follows: Computes the completion of P and converts it into a set C of clauses. Repeats Calls X on C to get a model M (terminates with failure if no such M exists). If M is an answer set of P, then returns with it. Otherwise, finds some loops in P whose loop formulas are not satisfied by M and adds their corresponding clauses to C.
Keywords for this software
References in zbMATH (referenced in 149 articles , 1 standard article )
Showing results 1 to 20 of 149.
Sorted by year (- Zhang, Heng; Zhang, Yan: Expressiveness of logic programs under the general stable model semantics (2017)
- Zhou, Yi; Zhang, Yan: A progression semantics for first-order logic programs (2017)
- Alliot, Jean-Marc; Diéguez, Martín; Fariñas del Cerro, Luis: Metabolic pathways as temporal logic programs (2016)
- Calimeri, Francesco; Gebser, Martin; Maratea, Marco; Ricca, Francesco: Design and results of the Fifth Answer Set Programming Competition (2016)
- Doherty, Patrick; Kvarnström, Jonas; Szałas, Andrzej: Iteratively-supported formulas and strongly supported models for Kleene answer set programs (extended abstract) (2016)
- Balint, Adrian; Belov, Anton; Järvisalo, Matti; Sinz, Carsten: Overview and analysis of the SAT challenge 2012 solver competition (2015) ioport
- Fichte, Johannes Klaus; Szeider, Stefan: Backdoors to tractable answer set programming (2015)
- Fichte, Johannes K.; Szeider, Stefan: Backdoors to normality for disjunctive logic programs (2015)
- Benhamou, Belaïd: Dynamic and static symmetry breaking in answer set programming (2013)
- Strass, Hannes; Thielscher, Michael: A general first-order solution to the ramification problem with cycles (2013)
- Alviano, Mario; Faber, Wolfgang; Greco, Gianluigi; Leone, Nicola: Magic sets for disjunctive Datalog programs (2012)
- Asuncion, Vernon; Lin, Fangzhen; Zhang, Yan; Zhou, Yi: Ordered completion for first-order logic programs on finite structures (2012)
- Faber, Wolfgang; Leone, Nicola; Perri, Simona: The intelligent grounder of DLV (2012)
- Gebser, Martin; Kaufmann, Benjamin; Schaub, Torsten: Conflict-driven answer set solving: from theory to practice (2012)
- Schockaert, Steven; Janssen, Jeroen; Vermeir, Dirk: Satisfiability checking in \Lukasiewiczlogic as finite constraint satisfaction (2012)
- Wang, Yisong; You, Jia-Huai; Yuan, Li Yan; Shen, Yi-Dong; Zhang, Mingyi: The loop formula based semantics of description logic programs (2012)
- Aguado, Felicidad; Cabalar, Pedro; Pérez, Gilberto; Vidal, Concepción: Loop formulas for splitable temporal logic programs (2011)
- Calimeri, Francesco; Ianni, Giovambattista; Ricca, Francesco; Alviano, Mario; Bria, Annamaria; Catalano, Gelsomina; Cozza, Susanna; Faber, Wolfgang; Febbraro, Onofrio; Leone, Nicola; Manna, Marco; Martello, Alessandra; Panetta, Claudio; Perri, Simona; Reale, Kristian; Santoro, Maria Carmela; Sirianni, Marco; Terracina, Giorgio; Veltri, Pierfrancesco: The third answer set programming competition: preliminary report of the system competition track (2011) ioport
- Chen, Yin; Lin, Fangzhen; Zhang, Yan; Zhou, Yi: Loop-separable programs and their first-order definability (2011)
- Durzinsky, Markus; Marwan, Wolfgang; Ostrowski, Max; Schaub, Torsten; Wagler, Annegret: Automatic network reconstruction using ASP (2011)
Further publications can be found at: http://assat.cs.ust.hk/#publications