Как Z3 обрабатывает нелинейную целочисленную арифметику?

Question

Я знаю, что теория целых чисел с умножением вообще неразрешима. Тем не менее, в некоторых случаях Z3 возвращает модель. Мне любопытно узнать, как это делается. Имеет ли это какое-то отношение к новой процедуре принятия решения по нелинейной арифметике над вещественными числами? Какие конкретные случаи (например, целые числа с конечным модулем и т. Д.) Были распознаны, для которых Z3 возвращает модель для запроса умножения? Буду признателен за любую оказанную помощь.

Answer 1

Да, проблема решения для нелинейной целочисленной арифметики неразрешима. Мы можем закодировать задачу Остановки для машин Тьюринга в нелинейной целочисленной арифметике. Я настоятельно рекомендую прекрасную книгу десятой проблемы Гильберта всем, кто интересуется этой проблемой.

Обратите внимание, что если формула имеет решение, мы всегда можем найти его методом грубой силы. То есть мы продолжаем перечислять все возможные назначения и проверяем, удовлетворяют ли они формуле или нет. Это ничем не отличается от попытки решить проблему остановки, просто запустив программу и проверив, завершается ли она после заданного количества шагов.

Z3 не выполняет наивного перечисления. Учитывая номер k, он кодирует каждую целую переменную, используя k биты и сводит все в пропозициональную логику. Затем SAT решатель используется для поиска решения. Если решение найдено, оно преобразует его обратно в целочисленное решение для исходной формулы. Если нет решения для формального предложения, то оно пытается увеличить kили переключается на другую стратегию. Это сведение к пропозициональной логике по сути является процедурой поиска модели / решения. Это не может показать, что проблема не имеет решения. На самом деле, для задач, где каждая целочисленная переменная имеет нижнюю и верхнюю границу, она может это сделать. Таким образом, Z3 должен использовать другие стратегии, чтобы показать, что решения не существует.

Более того, редукция в логику предложения работает только в том случае, если существует очень маленькое решение (решение, которое требует небольшого количества битов для кодирования). Я обсуждаю это в следующем посте:

• Нужна помощь в понимании уравнения

Z3 не имеет хорошей поддержки нелинейной целочисленной арифметики. Описанный выше подход очень упрощен. На мой взгляд, Mathematica, похоже, обладает наиболее полным набором методик:

http://reference.wolfram.com/legacy/v5_2/functions/AdvancedDocumentationDiophantinePolynomialSystems

Наконец, решатель нелинейной вещественной арифметики (NLSat) по умолчанию не используется для нелинейных целочисленных задач. Обычно это очень малоэффективно для целочисленных задач. Тем не менее, мы можем заставить Z3 использовать NLSat даже для целочисленных задач. Мы просто должны заменить:

(check-sat)

С

(check-sat-using qfnra-nlsat)

Когда эта команда используется, Z3 решит проблему как реальную проблему. Если реальное решение не найдено, мы знаем, что нет целочисленного решения. Если решение найдено, Z3 проверит, действительно ли решение присваивает целочисленные значения целочисленным переменным. Если это не так, он вернется unknown указать, что это не решило проблему.