Z3による汎用大域的最適化 - Qiita概要 Z3 Proverを用いた，"数値的"な大域的最適化手法について示す． Z3 Proverとは？ ざっくりとはMicrosoft Researchが作った，MITライセンスの定理証明器です． Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license. If you are not familiar with Z3, you can start here. Z3 can be built using Visual Studio, a Makefile or using CMake. It provides bindings for several programming languages. See the release notes for notes on various
