Сделать ограничение труднее решить для решателя ограничений?

Question

Я новичок в решении SMT, и я пишу, чтобы узнать некоторые советы и указатели, чтобы понять, что на самом деле difficult constraint для решения SMT, например Z3.

Я попытался настроить длину битовых векторов, например, следующим образом:

>>> a = BitVec("a", 10000)
>>> b = BitVec("b", 10000)
>>> c = a >> 18 + 6 - 32 + 69 == b <<12 + 7 * 32
>>>
>>> s = Solver()
>>> s.add(c)
>>> s.check()

Хотя интуитивно это может привести к довольно большому пространству поиска, оказывается, что Z3 все еще делает довольно хорошую работу и быстро ее решает.

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

a * 4 != b + 5

Как я могу усложнить решение решателя ограничений? Есть ли общий способ сделать это? У меня сложилось впечатление, что каким-то образом это ограничение оказывается "нелинейным", тогда это сложно. Но мне все еще неясно, как это работает.

=================================

Спасибо за все добрые заметки и проницательные сообщения. Я очень ценю это!

Итак, вот несколько предварительных тестов по предложению @usr:

c = BitVec("c", 256)

for i in range(0, 10):
    c = c ^ (c << 13) + 0x51D36335;

s = Solver()
s.add(c == 0xdeadbeef)
print (s.check())
print (s.model())


➜  work time python test.py
sat
[c = 37865234442889991147654282251706833776025899459583617825773189302332620431087]
python test.py  0.38s user 0.07s system 81% cpu 0.550 total

Answer 1

Логика битового вектора всегда разрешима; поэтому, в то время как все может занять много времени, z3 может решить все проблемы с битвекторами. Конечно, если размеры битовых векторов велики, то решатель может занять очень много времени или исчерпать память, прежде чем найдет решение. Умножение и криптоалгоритмы являются типичными примерами, которые всегда вызывают трудности при увеличении размеров битов.

С другой стороны, у нас есть нелинейные целочисленные задачи. Для них нет процедуры принятия решения, и, хотя z3 "старается изо всех сил", такие проблемы обычно выходят за рамки теоретических соображений. Вы можете найти много таких примеров в сообщениях о переполнении стека. Вот самый последний: Z3 возвращает модель, недоступную

Answer 2

Если вы просто хотите, чтобы Z3 "работал очень усердно", вы можете попробовать факторизацию чисел, например a * b = constant и введите простое число или большой композит.

Или создайте простую хеш-функцию и получите предварительное изображение:

Что я сделал, так это увидел, как определяется SHA-1. Затем я реализовал простую версию этого. SHA-1 состоит из очень простых операций, таких как shift, add, xor. Из этого шаблона вы можете создать простую хеш-функцию для тестирования. Тогда вы говорите y = hash(x) && y = 0x1234 и Z3 даст вам x который является предварительным изображением.

Для вашего развлечения я сделаю на месте простую хеш-функцию:

BitVec currentValue = input;

for (i = 0 to 10)
 currentValue = currentValue ^ (currentValue <<< 13) + 0x51D36335;

BitVec hash = currentValue;

Это действительно функциональная реализация хэша (но не безопасная). Вы можете играть с операциями, количеством раундов и размером битового вектора. Вы можете утверждать hash = someConstant получить предварительное изображение. Например, пусть Z3 даст вам input это приводит к нулевому хешу.

Вы также можете применить более причудливые ограничения, например, input == hash или же hash % 1234 == 0 && hash & 0xF == 7, Z3 может удовлетворить любое условие при достаточной вычислительной мощности.

Я лично нашел эту возможность очень увлекательной.