Влияет ли переменная с большими целочисленными значениями на производительность SMT?

Question

Мне интересно, влияют ли большие целочисленные значения на производительность SMT. Иногда мне нужно работать с большими значениями. В основном я выполняю арифметические операции (в основном сложение и умножение) над ними (т. Е. Различные целочисленные термины), и мне нужно сравнить результирующее значение с ограничениями (т. Е. С некоторым другим целочисленным термином).

Answer 1

Большие целые и / или рациональные числа в задаче ввода не являются окончательным показателем твердости. Z3 может генерировать большие числа внутри, даже если вход содержит только маленькие числа. Я наблюдал много примеров, когда Z3 тратит много времени на обработку больших рациональных чисел. Много времени тратится на вычисление GCD числителя и знаменателя. Каждое вычисление GCD занимает относительно небольшое количество времени, но на сложных задачах Z3 выполнит миллионы из них. Обратите внимание, что Z3 использует рациональные числа для решения чисто целочисленных задач, потому что он использует симплексный алгоритм для решения линейной арифметики. Если вы разместите свой пример, я могу дать вам более точный ответ.