Nikolaj Bjørner, Maxwell Levatich, Nuno P. Lopes, Andrey Rybalchenko, Chandrasekar Vuppalapati
We describe our experiences using Z3 for synthesizing and optimizing next generation plant configurations for a car manufacturing company. Our approach leverages unique capabilities of Z3: a combination of specialized solvers for finite domain bit-vectors and uninterpreted functions, and a programmable extension that we call constraints as code. To optimize plant configurations using Z3, we identify useful formalisms from Satisfiability Modulo Theories solvers and integrate solving capabilities for the resulting non-trivial optimization problems.
N. Bjørner, M. Levatich, N. P. Lopes, A. Rybalchenko, C. Vuppalapati. Supercharging Plant Configurations Using Z3. In Proc. of the 18th International Conference on Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR), July 2021.
@inproceedings{plantconfig-cpaior,
title = {Supercharging Plant Configurations Using Z3},
author = {Nikolaj Bj{\o}rner and Maxwell Levatich and Nuno P. Lopes and Andrey Rybalchenko and Chandrasekar Vuppalapati},
booktitle = {Proc. of the 18th International Conference on Integration of Constraint Programming, Artificial Intelligence, and Operations Research (CPAIOR)},
doi = {10.1007/978-3-030-78230-6_1},
month = jul,
year = 2021
}
The final publication is available at link.springer.com.