具有大整數值的變量是否會影響SMT的性能？

Question

我想知道大整數值是否會影響SMT的性能。有時我需要處理大量的價值。大多數情況下，我會對它們（即不同的整數項）進行算術運算（主要是加法和乘法），並需要將結果值與約束（即其他整數項）進行比較。

Answer 1

輸入問題中的大整數和/或有理數並不是硬度的明確指標。 即使輸入僅包含小數字，Z3也可能在內部生成大量數字。 我觀察到很多Z3花費大量時間處理大量有理數的例子。 花了很多時間計算分子和分母的GCD。 每個GCD計算都需要相對較少的時間，但在嚴重問題上Z3會執行數百萬次。 請注意，Z3使用有理數解決純整數問題，因爲它使用基於Simplex的算法來求解線性算術。 如果你發佈你的例子，我可以給你一個更準確的答案。