Solving the Wastewater Treatment Plant Problem with SMT
This work addresses scheduling inefficiencies for wastewater treatment plants, but it is incremental as it applies existing SMT methods to a new domain.
The paper tackles the Wastewater Treatment Plant Problem, a real-world scheduling challenge, and demonstrates that state-of-the-art SMT solvers outperform other tools like mathematical and constraint programming on naive modeling, using real and randomly generated benchmarks.
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.