Ist es möglich, die Laufzeit von z3 oder die Laufzeit des DPLL (T) -Algorithmus zu schätzen? Selbst im schlimmsten Fall

Question

Ich arbeite daran, einen Prototyp von Microsoft Z3 zu visualisieren. Ich frage mich, ob es möglich ist, die Laufzeit von z3 oder den Algorithmus zu schätzen? Auch wäre es toll, wenn ich eine Worst-Case-Laufzeit bekommen könnte.

Gibt es auch in z3 irgendeine Methode, um die Laufzeit jedes Prüfprozesses durch einen theoretischen Löser zu erhalten?

Danke für die Antwort.

Answer 1

Es ist generell nicht möglich. SAT ist ein NP-vollständiges Problem, und SMT ist mindestens so schwer wie SAT.