z3 - LRA の下での量指定子除去のための最先端のソルバーは何ですか?

Question

線形実数演算での量指定子の削除で Z3 を試しました。数式はそれほど大きくありませんが、削除する変数の数が 5 を超えると、非常に時間がかかります (または終了しません)。より良いパフォーマンスを発揮できるソルバーは他にありませんか? または、Z3 を助けることができるトリックはありますか?

Answer 1

私は専門家ではありませんが、Reduce の RedLog を試すことができます。