概要 Z3 Proverを用いた，"数値的"な大域的最適化手法について示す． Z3 Proverとは？ ざっくりとはMicrosoft Researchが作った，MITライセンスの定理証明器です． Z3 is a theorem prover from Micro...