Z3ソルバのランタイムを計算するには

Question

私はz3pyを使って一連の方程式を解いています。どのように私はそれのランタイム順序を計算するでしょうか？ これは、線形方程式のセットで満たされる必要があるbitvecs変数を持ちます。マニュアルとガイドでは、ランタイムを計算する方法はありません。

Answer 1

使用したソルバーのうち、（最悪の場合）時間の複雑さを求めていますか？もしそうなら、私はあなたが良い答えを得ることはできないだろうと思っています。それはあなたの問題が落ちるロジックの組み合わせに依存します。 QF_BVまたはUFNIAを選択し、次にソルバがその論理の組み合わせに対して実装する（（半）決定）プロシージャを実行します。

Z3の著者（https://github.com/Z3Prover/z3/wiki/Publications）の論文を見てください - いくつかの詳細を提供するかもしれません。