EZSMT Version 3, Matured

背景

Constraint Answer Set Programming (CASP) 是一种混合推理范式，它将 Answer Set Programming (ASP) 与 Constraint Processing 以及 Satisfiability Modulo Theories (SMT) 相结合，能够对复杂的组合搜索问题实现强大的声明式编码。随着实际应用中问题规模的扩大和约束类型的增多，CASP 系统需要更灵活的框架来支持表达力更强、优化能力更完善、新约束类型集成更便捷的求解方案。在此背景下，EZSMT 系列应运而生。本文介绍的是 EZSMT 的第三个主要版本——EZSMTV3，该版本在先前 EZSMT+ 系统的基础上进一步成熟，旨在通过基于 SMT 的翻译方法，提供一个可扩展的 CASP 求解框架。

核心内容

EZSMTV3 是一个基于 SMT 的可扩展 CASP 框架，它延续并深化了将 CASP 问题翻译为 SMT 问题求解的路线。论文详细介绍了该系统的设计与实现。与传统的为 CASP 编写自定义搜索程序不同，EZSMTV3 直接利用最先进的 SMT 求解器（如 CVC5、YICES 和 Z3）来执行推理任务。这种架构使得系统能够快速适配不同求解器的最新进展，而不需要重复实现搜索逻辑。

EZSMTV3 引入了更富表达力的输入语言，允许用户以更自然的方式描述约束。系统支持通过弱约束（weak constraints）进行优化，这是许多实际优化问题所必需的特性。此外，框架提供了简洁的基础设施，以便于集成新的约束类型——开发者只需定义新约束的语义并将其映射为 SMT 公式，即可实现扩展。

论文通过基准测试，将 EZSMTV3 与同类 CASP 系统进行了比较，包括 CLINGCON、CLINGO[DL] 和 CLINGO[LP]。测试结果展示了 EZSMTV3 在包含整数和实数混合域约束的问题上的处理能力，证明了其在表达力和性能上的竞争力。该框架为未来在 CASP 领域的扩展和理论探索提供了一个稳健的平台。

关键要点

• EZSMTV3 是一个基于 SMT 的可扩展 CASP 框架，采用翻译方法将 CASP 问题转化为 SMT 实例。
• 系统不实现自定义搜索过程，而是直接调用外部 SMT 求解器（CVC5、YICES、Z3）进行推理，从而利用求解器的最新技术。
• 引入了更富表达力的输入语言，支持弱约束优化，便于描述和求解优化问题。
• 提供简洁的扩展机制，允许集成新的约束类型，只需将其映射为 SMT 公式即可。
• 基准测试结果显示，EZSMTV3 在与其他 CASP 系统（CLINGCON、CLINGO[DL]、CLINGO[LP]）的比较中，能够有效处理整数与实数混合域的约束问题。
• 系统设计注重未来可扩展性，为 CASP 领域的后续研究和应用提供了基础平台。

意义与影响

EZSMTV3 的成熟版本发布，对 CASP 领域具有多重意义。首先，它验证了“翻译到 SMT”这一技术路线的可行性，表明无需为每一种约束类型定制搜索算法，只需借助通用 SMT 求解器即可有效求解 CASP 问题。这降低了 CASP 系统开发的维护成本，并使得新约束的集成变得高效。其次，通过引入弱约束支持，系统能够直接处理优化目标，扩展了 CASP 在工程优化、调度、资源分配等领域的应用场景。最后，EZSMTV3 提供了一个开放的实验平台，研究人员可以基于此框架探索更复杂的理论（如结合非线性算术、量词等），并轻松与新兴 SMT 求解器对接。整体而言，该工作推动了 CASP 从理论研究走向实际部署，并为后续基于 SMT 的混合推理系统树立了范例。