Я знаю, что теория целых чисел с умножением в общем случае неразрешима. Тем не менее, в некоторых случаях Z3 возвращает модель. Мне любопытно узнать, как это делается. Связано ли это с новой процедурой принятия решений для нелинейной арифметики над реалами? Какие конкретные экземпляры (например: Целые числа под конечным модулем и т.д.) Были распознаны, для которых Z3 возвращает модель для запроса умножения? Любая помощь очень ценится.
Как Z3 обрабатывает нелинейную целочисленную арифметику?
Ответ 1
Да, проблема решения для нелинейной целочисленной арифметики неразрешима. Мы можем кодировать проблему Halting для машин Тьюринга в нелинейной целочисленной арифметике. Я настоятельно рекомендую красивую книгу проблема Хилберта десятая для любого, кто интересуется этой проблемой.
Заметим, что если формула имеет решение, мы всегда можем найти ее грубой силой. То есть мы продолжаем перечислять все возможные назначения и проверяем, удовлетворяют ли они формуле или нет. Это не так, как если бы вы пытались решить проблему Halting, просто запустив программу и проверив, завершается ли она после определенного количества шагов.
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, чтобы указать, что он не смог решить проблему.