AI 中文总结
介绍EZSMTV3这一基于SMT的可扩展CASP框架，它在EZSMT+基础上改进，引入更具表现力的输入语言，利用先进SMT求解器推理，给出与同类工具的基准测试结果，为CASP领域未来扩展和理论探索提供平台。
AI 中文摘要
约束答案集编程（CASP）是一种将答案集编程（ASP）与约束处理和可满足性模理论（SMT）相结合的混合推理范式，能对复杂组合搜索问题进行强大的声明式编码。本文介绍了EZSMTV3的设计与实现，它是一个基于SMT的可扩展CASP框架，改进了CASP求解的转换方法。基于EZSMT+系统，EZSMTV3引入了更具表现力的输入语言，支持通过弱约束进行优化，并为新约束类型的简化集成提供基础。它利用CVC5、YICES和Z3等先进SMT求解器进行推理。文中给出了EZSMTV3与CLINGCON、CLINGO[DL]和CLINGO[LP]等CASP同类工具的基准测试结果，展示了其处理整数和实数混合域约束的能力。该系统为CASP领域的未来扩展和理论探索提供了强大平台。
英文摘要
Constraint Answer Set Programming (CASP) is a hybrid reasoning paradigm that combines Answer Set Programming (ASP) with Constraint Processing and Satisfiability Modulo Theories (SMT), enabling powerful declarative encodings of complex combinatorial search problems. This paper presents the design and implementation of EZSMTV3, an extensible SMT-based CASP framework that advances the translational approach to CASP solving. Building upon the foundation of the EZSMT+ system, EZSMTV3 introduces a more expressive input language, supports optimization via weak constraints, and offers foundations for streamlined integration of new constraint types. Rather than implementing custom search procedures, EZSMTV3 leverages state-of-the-art SMT solvers, such as CVC5, YICES, and Z3 to perform reasoning. The paper provides benchmarking results comparing EZSMTV3 with its CASP peers such as CLINGCON, CLINGO[DL], and CLINGO[LP], while showcasing its ability to handle mixed-domain constraints involving both integers and reals. The system provides a robust platform for future extensions and theoretical exploration within the CASP domain.
CommentsUnder consideration in Theory and Practice of Logic Programming (TPLP)
