Решение линейных уравнений с использованием Z3 - PullRequest
Новая
       14

Решение линейных уравнений с использованием Z3

0 голосов
/ 22 декабря 2018

У меня есть следующие линейные уравнения. 

m = 2 ** 31 - 1

(207560540 ∗ a + b) modulo m = 956631177
(956631177 ∗ a + b) modulo m = 2037688522

Какой самый эффективный способ решения этих уравнений?

Я использовал Z3, но он не нашел никакого решения.Мой код для Z3 для решения приведенных выше уравнений: 

#! /usr/bin/python

from z3 import *

a = Int('a')
b = Int('b')

s = Solver()

s.add((a * 207560540 + b) % 2147483647 == 956631177)
s.add((a * 956631177 + b) % 2147483647 == 2037688522)

print s.check()
print s.model()

Я знаю, что решение: a = 16807, b = 78125, однако, как я могу заставить Z3 решить его?

Другой метод, который я попробовал, это установить a и b в BitVec () вместо Integers, как показано ниже: 

a = BitVec('a', 32)
b = BitVec('b', 32)

Это дает мне неправильное решение, как показано ниже: 

[b = 3637638538, a = 4177905984]

Есть ли способ решить это с Z3?

Спасибо.

1 Ответ

0 голосов
/ 22 декабря 2018

Помимо битовых векторов: при использовании битовых векторов все операции выполняются по модулю 2^N, где N - размер битового вектора.Таким образом, z3 не дает вам incorrect решения: если вы выполните математические вычисления по модулю 2^32, вы обнаружите, что модель, которую он находит, действительно верна.

Похоже, что ваша проблема действительно нужнанеограниченные целые числа, и он не является действительно линейным из-за модуля 2^31-1.(Линейный означает умножение на константу; модуль на константу переносит вас в другое царство.) И с модулем просто не легко рассуждать;Я не думаю, что z3 является подходящим инструментом для решения подобных проблем, как и любой другой SMT-решатель.Такие инструменты, как mathematica, wolfram-alpha и т. Д., Вероятно, являются лучшим выбором в этом случае;например, см .: раствор вольфрама-альфа

...