Make a constraint more difficult to solve for a constraint solver?

Question

I am a newbie to SMT solving and I am writing to inquire some advice and pointers to understand what is a really difficult constraint for SMT solver to solve, for instance Z3.

I tried to tweak the length of bit vectors, for instance in the following way:

>>> 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()

While intuitively this could leads to a quite large search space, it turns out that Z3 still does a pretty good job and solve it swiftly.

I am aware that some crypto hash functions or math formulas (e.g., Collatz conjecture) could make constraint solving quite difficult. But that seems pretty extreme. On the other hand, for instance suppose I have the following constraint:

a * 4 != b + 5

How can I make it more difficult for a constraint solver to solve? Is there any general way of doing so? I got the impression that somehow it a constraint turns to be "non-linear", then it is difficult. But it is still unclear to me how that works.

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

Thank you for all the kind notes and insightful posts. I appreciate it very much!

So here are some tentative tests according to @usr's suggestion:

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

Bitvector logic is always decidable; so while things may take long, z3 can solve all bitvector problems. Of course, if the bit-vector sizes involved are large, then the solver can take extremely long, or run out of memory before finding a solution. Multiplication and crypto-algorithms are typical examples that always cause a hard time as the bit sizes increase.

On the flip side, we have non-linear integer problems. There's no decision procedure for them, and while z3 "tries its best," such problems are typically beyond scope for theoretical reasons. You can find many instances of these in stack-overflow posts. Here's a most recent one: Z3 returns model not available

Answer 2

If you just want to see Z3 "work really hard" you can try number factorization e.g. a * b = constant and input a prime number or a large composite.

Or, build a simple hash function and obtain a pre-image:

What I did was to see how SHA-1 is defined. Then, I implemented a simple version of that. SHA-1 consists of very simple operations such as shift, add, xor. From this template you can construct a simple hash function for testing purposes. Then you say y = hash(x) && y = 0x1234 and Z3 will give you x which is the pre-image.

For your entertainment I will make up a simple hash function on the spot:

BitVec currentValue = input;

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

BitVec hash = currentValue;

This is an actually functional hash implementation (but not secure). You can play with the operations, number of rounds and bitvector size. You can assert hash = someConstant to obtain a pre-image. For example, let Z3 give you an input that results in a zero hash.

You can apply more fancy constraints as well, for example input == hash or hash % 1234 == 0 && hash & 0xF == 7. Z3 can satisfy any condition at all given enough compute power.

I personally found this capability highly fascinating.