使用 SMT 求解废水处理厂问题
人工智能
2016-09-20 v1 计算机科学中的逻辑
摘要
在本文中，我们介绍了一个现实世界的调度问题——废水处理厂问题，并比较了几种工具在该问题上的性能。我们表明，对于朴素建模，SOTA 的 SMT 求解器优于从数学规划到约束编程的其他工具。我们使用了真实和随机生成的基准测试。基于此及类似结果，我们主张开发能够将约束编程语言转换为 SMT-LIB 标准语言的编译器前端。
引用
@article{arxiv.1609.05367,
title = {Solving the Wastewater Treatment Plant Problem with SMT},
author = {Miquel Bofill and Víctor Muñoz and Javier Murillo},
journal= {arXiv preprint arXiv:1609.05367},
year = {2016}
}