SMT-Based Constraint Answer Set Solver EZSMT (System Description)

Citations Over TimeTop 10% of 2016 papers

Abstract

Constraint answer set programming is a promising research direction that integrates answer set programming with constraint processing. Recently, the formal link between this research area and satisfiability modulo theories (or SMT) was established. This link allows the cross-fertilization between traditionally different solving technologies. The paper presents the system ezsmt, one of the first SMT-based solvers for constraint answer set programming. It also presents the comparative analysis of the performance of ezsmt in relation to its peers including solvers EZCSP, CLINGCON, and MINGO. Experimental results demonstrate that SMT is a viable technology for constraint answer set programming.

Related Papers

• → Classical negation in logic programs and disjunctive databases(1991)2,289 cited
• → Answer set programming at a glance(2011)905 cited
• → Theory Solving Made Easy with Clingo 5(2016)146 cited
• → Integrating answer set programming and constraint logic programming(2008)122 cited