EZSMTV3提升复杂约束求解能力，支持混合域变量与优化。
EZSMT Version 3, Matured
- 基于SMT求解器构建，支持整数与实数混合约束
- 引入弱约束实现优化求解，输入语言更灵活表达复杂问题
- 适合需要高效处理多类型约束的逻辑推理研究者
约束答案集编程（CASP）是将答案集编程（ASP）与约束求解、满足模理论（SMT）结合的混合推理范式，可对复杂的组合搜索问题进行强大且声明式的建模。本文介绍EZSMTV3的设计与实现，这是一个基于SMT的可扩展CASP框架，推进了CASP求解的翻译方法。在EZSMT+基础上，EZSMTV3引入更丰富的输入语言，支持通过弱约束进行优化，并为新约束类型的集成提供基础。该系统不自定义搜索过程，而是利用当前最先进的SMT求解器（如CVC5、YICES、Z3）进行推理。论文通过基准测试对比了EZSMTV3与同类系统CLINGCON、CLINGO[DL]、CLINGO[LP]的表现，展示了其处理涉及整数和实数的混合域约束的能力。该系统为CASP领域的未来扩展与理论探索提供了稳健平台。
原文摘要 · Abstract (English)
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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。