Extension of the EZSMT Software System For Non-tight Constraint Answer Set Programs

Answer set programming (ASP) is a programming language that plays a critical role in the development of software applications in areas of science, humanities, and industry. Yet, it is faced with some challenges. Therefore, researchers develop a related paradigm called constraint answer set programming (CASP) to tackle several issues of ASP tools. Recently, a method is proposed to find solutions to CASP programs by using satisfiability modulo theories (SMT) solvers. SMT solvers are high-performance systems stemming from the software verification community. This SMT-based approach is implemented in a system called EZSMT, which often outperforms its peers. Yet, it has several limitations. For instance, it is unable to process a large class of programs called non-tight . This restriction does not allow users to express, for example, reachability relations between cities connected by roads on a map. Solving non-tight programs is important, because they are crucial in many applications. In this work, we extend EZSMT for non-tight input. Our main contribution is designing an extension, which adds additional requirements into non-tight programs so that SMT solvers can be called to compute solutions correctly. We also extend the architecture of original EZSMT, in order to allow computation of multiple solutions. Our experimental analysis shows that the extended EZSMT system is a viable tool when being compared to state-of-the-art CASP solvers CLINGCON and EZCSP. In summary, we believe that, by making clear the translation of arbitrary CASP programs to SMT, our work will boost the cross-fertilization between the two areas