Physical Sciences and Mathematics Commons^™

Constraint answer set programming integrates answer set programming with constraint processing. System Ezsmt+ is a constraint answer set programming tool that utilizes satisfiability modulo theory solvers for search. The truly unique feature of ezsmt+ is its capability to process linear as well as nonlinear constraints simultaneously containing integer and real variables.

Answer set programming  is a  declarative programming paradigm used in formulating combinatorial search problems and implementing distinct knowledge representation and reasoning formalisms. It is common that several related and yet substantially different answer set programs exist for a given problem. Uncovering precise formal links between these programs is often of value. This paper develops a methodology for establishing such links. This methodology relies on the notions of strong equivalence and conservative extensions and a body of earlier theoretical work related to these concepts. We use distinct answer set programming formalizations  of an action language C and a syntactically restricted action …

Many answer set solvers utilize Satisfiability solvers for search. SMT solvers extend Satisfiability solvers. This paper presents the CMODELS-DIFF system that uses SMT 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.