z3py solver.check () переходит от «сат» к «неизвестному», когда я увеличиваю длину Bitvector - PullRequest
Новая
       97

z3py solver.check () переходит от «сат» к «неизвестному», когда я увеличиваю длину Bitvector

0 голосов
/ 30 апреля 2020

Я хочу разложить число n с помощью битвекторов в Z3. Я использую Bitvectores, потому что я хочу ограничить отдельные биты в p an q. Этот простой пример работает, и решатель возвращает «sat». 

from z3 import *

Bits = 32

n = 12
p_vec = BitVec('p', Bits)
q_vec = BitVec('q', Bits)
n_vec = BitVecVal(n,Bits)

s = Solver()
s.add(p_vec * q_vec == n_vec)
s.add(p_vec > 1, q_vec > 1)
s.add(BVMulNoOverflow(p_vec,q_vec,False))

print (s.check())

Но теперь я хочу добавить другое число n с 4096 битами. Поэтому я изменил Bits = 4096 в этом примере и использовал те же числа. Решатель дает мне теперь «неизвестно» вместо «сел». Кажется, решатель прекращается в какой-то момент. Нужно ли менять настройки солвера или есть другой подход для этого?

1 Ответ

1 голос
/ 30 апреля 2020

Когда я запускаю вашу программу с Bits = 4096, она не говорит unknown. Он просто не завершается sh быстро (я ждал несколько минут), и я не ожидал бы, что это так.

Решение для Bitvector завершено. То есть, если вы подождете достаточно долго, он в конечном итоге вернет sat или unsat, при условии, что у вас не хватает памяти (и терпения). Однако для этой проблемы ожидаемое количество может быть практически бесконечным, и вам, скорее всего, не хватит памяти на вашем компьютере задолго до того, как это произойдет. Итак, я не уверен, как вы получаете это unknown. Возможно, вы используете некоторые параметры тайм-аута или что-то еще, чего вы здесь не видите.

Вы можете попробовать добавить ограничения вида: p_vec < n и q_vec < p_vec, чтобы нарушить симметрию. И в некоторых случаях это действительно может помочь, поскольку n является константой. Но в целом это бесполезно, и для любого разумного размера в битах для использования в практике криптографии c решатель будет практически l oop навсегда.

Факторизация - трудная проблема по очевидным причинам и SMT-решатель определенно не правильный инструмент для этого. Смотрите здесь для более раннего обсуждения: Функция битового вектора Z3

...