Grundlegendes zur Leistung von QFBV SMT-Solvern

SMT-Löser wie Z3 oder Boolector verwenden komplexe Heuristiken, um Probleme zu lösen. Dies macht es jedoch auch sehr schwierig, die Leistung eines solchen Lösers für ein bestimmtes Problem vorherzusagen. Meine Frage lautet also:

Frage

Gibt es eine Möglichkeit, die Leistung eines SMT-Lösers für einen bestimmten in der Theorie der quantifiziererfreien Bitvektoren (QFBV) zu verstehen oder Einblicke in diese zu gewinnen?

Dies schließt auch alle Visualisierungstools ein, die helfen würden zu verstehen, wo der Solver "stecken bleibt" / keine Fortschritte macht.

Anwendungen

• Verstehen Sie im Voraus, wie sich unterschiedliche Codierungen desselben Problems auf die Leistung des Lösers auswirken (der Stand der Technik kann hier nicht sein: "Probieren Sie einfach ein paar verschiedene Codierungen aus und hoffen Sie, dass eine schnell genug ist", oder?)

• Wenn ein bestimmtes Problem aus zeitlichen Gründen von einem SMT-Löser nicht gelöst werden kann, suchen Sie nach einer Möglichkeit, das Problem anders auszudrücken, damit es gelöst werden kann.

• Verschwenden Sie keine Zeit mit domänenspezifischen Problemvereinfachungen, die die Solver-Leistung überhaupt nicht oder sogar negativ beeinflussen.

Bestehende Forschung

Ich habe versucht, Forschung zu diesem Thema zu finden, aber ich konnte nicht viel finden. Ich habe noch nicht viel Erfahrung auf dem Gebiet der SAT / SMT-Löser, also entschuldige mich, wenn ich etwas verpasst habe.

• SATzilla : Prognostiziert den leistungsstärksten Solver basierend auf Funktionen, die mithilfe von Techniken des maschinellen Lernens aus dem Problem extrahiert wurden.

  Dies gilt nur für SAT anstelle von SMT und erklärt nicht die Gründe für die Leistung des Lösers.

• Z3-Axiom-Profiler Eine Visualisierung des Z3-Instanziierungsdiagramms und die Analyse übereinstimmender Schleifen

  Sieht so aus, als würde sich dies nur auf die quantifizierten Theorien konzentrieren.

Die kurze Antwort lautet nein, wir verstehen es nicht. Die lange Antwort lautet: Ja, wir haben einige Grenzen, aber diese Grenzen sind nicht sehr hilfreich. Es ist ziemlich klar, dass die Laufzeit im ungünstigsten Fall exponentiell ist. Das ist nicht sehr hilfreich, da wir wissen, dass es in einigen / vielen praktischen Situationen ziemlich schnell zu laufen scheint - und wir wissen nicht wirklich warum.

Wir wissen nicht, warum dies für SAT-Löser gilt, geschweige denn für QFBV. Zu verstehen, warum QFBV-Löser oft schnell sind, scheint mindestens so schwierig zu sein wie zu verstehen, warum SAT-Löser oft schnell sind, was bereits über unser derzeitiges Verständnis hinausgeht. Wenn Sie auf dieser Website mehr suchen, finden Sie eine Zusammenfassung der aktuellen Versuche, das letztere Thema zu verstehen.