用SMT解决污水处理厂问题
Solving the Wastewater Treatment Plant Problem with SMT
摘要：
在本文中，我们介绍了污水处理厂的问题，现实世界的调度问题，并比较几种工具的性能，我们表明，对于一个天真的建模，国家的最先进的SMT求解器优于其他工具，从数学规划约束规划。我们使用真实和随机生成的基准。从这个和类似的结果，我们要求开发编译器前端能够从约束程序设计语言转换到SMT-LIB标准语言的方便。
英文摘要：
In this paper we introduce the Wastewater Treatment Plant Problem, a real-world scheduling problem, and compare the performance of several tools on it. We show that, for a naive modeling, state-of-the-art SMT solvers outperform other tools ranging from mathematical programming to constraint programming. We use both real and randomly generated benchmarks. From this and similar results, we claim for the convenience of developing compiler front-ends being able to translate from constraint programming languages to the SMT-LIB standard language.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
