Ich frage mich, ob große Integer-Werte Auswirkungen auf die Leistung von SMT haben. Manchmal muss ich mit großen Werten arbeiten. Meistens mache ich arithmetische Operationen (hauptsächlich Addition und Multiplikation) an ihnen (d. H. Verschiedene ganzzahlige Terme) und muss den resultierenden Wert mit Beschränkungen vergleichen (d. H. Mit einem anderen ganzzahligen Term).Beeinflussen Variablen mit großen Ganzzahlwerten die Leistung von SMT?
Große Zahlen und/oder Rationale im Eingabeproblem sind kein definitiver Indikator für die Härte. Z3 kann intern große Zahlen erzeugen, auch wenn der Eingang nur kleine Zahlen enthält. Ich habe viele Beispiele beobachtet, bei denen Z3 viel Zeit damit verbringt, große rationale Zahlen zu verarbeiten. Es wird viel Zeit damit verbracht, den GCD des Zählers und Nenners zu berechnen. Jede GCD-Berechnung benötigt relativ wenig Zeit, aber bei harten Problemen führt Z3 Millionen von ihnen aus. Beachten Sie, dass Z3 rationale Zahlen zum Lösen von reinen Ganzzahlproblemen verwendet, da es einen Simplex-basierten Algorithmus zum Lösen der linearen Arithmetik verwendet. Wenn Sie Ihr Beispiel veröffentlichen, kann ich Ihnen eine genauere Antwort geben.