EZSMTV3发布：基于SMT的约束答案集编程框架迎来重大升级

约束答案集编程（CASP）是一种融合了答案集编程（ASP）、约束处理与可满足性模理论（SMT）的混合推理范式，能够以声明式方式高效编码复杂的组合搜索问题。近日，研究团队正式发布了EZSMTV3，这是一个基于SMT的可扩展CASP框架，标志着该领域翻译式求解方法的重要进展。

EZSMTV3在EZSMT+系统基础上进行了全面升级，引入了更具表现力的输入语言，支持通过弱约束进行优化求解，并为新约束类型的集成提供了标准化基础。该系统创新性地避免自行实现搜索算法，转而集成CVC5、YICES和Z3等前沿SMT求解器进行推理计算，显著提升了求解效率与可靠性。

研究论文展示了EZSMTV3与CLINGCON、CLINGO[DL]、CLINGO[LP]等主流CASP系统的对比测试结果。实验表明，该系统在处理涉及整数与实数混合域的约束问题时表现优异，为复杂约束问题的求解提供了新的技术路径。EZSMTV3的模块化设计为CASP领域的理论探索和功能扩展奠定了坚实基础，有望推动约束编程与自动推理技术的融合发展。