Solving the Wastewater Treatment Plant Problem with SMT

TL;DR

This paper demonstrates that SMT solvers outperform other methods in solving a real-world wastewater treatment scheduling problem, highlighting the potential of SMT in practical constraint-solving applications.

Contribution

It introduces the Wastewater Treatment Plant Problem and compares SMT solvers with other tools, advocating for compiler front-ends translating constraint languages to SMT-LIB.

Findings

SMT solvers outperform mathematical programming and constraint programming tools.

Real and synthetic benchmarks show SMT's effectiveness.

Supports development of constraint language to SMT-LIB translation.

Abstract

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.