文章基本信息

标题：SMT-Based Answer Set Solver CMODELS(DIFF) (System Description)
本地全文：下载
作者：Da Shen ; Yuliya Lierler
期刊名称：OASIcs : OpenAccess Series in Informatics
电子版ISSN：2190-6807
出版年度：2018
卷号：64
页码：1-15
DOI：10.4230/OASIcs.ICLP.2018.11
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Many answer set solvers utilize Satisfiability solvers for search. Satisfiability Modulo Theory solvers extend Satisfiability solvers. This paper presents the CMODELS(DIFF) system that uses Satisfiability Modulo Theory solvers to find answer sets of a logic program. Its theoretical foundation is based on Niemala's characterization of answer sets of a logic program via so called level rankings. The comparative experimental analysis demonstrates that CMODELS(DIFF) is a viable answer set solver.
关键词：answer set programming; satisfiability modulo theories; constraint satisfaction processing