PB Encoding Buggy

[StephanGocht]

Hi, Nice work, but there is a bug with the PB encoding of the sum modulo 32:

The used encoding for add2 (similar issue exists for add5) is

\sum_{i=0}^{31} 2^i x_i 2^i y_i - 2^i z_i = 0

The problem is that this rules out all cases where x + y >= 2^32. The addition should be modulo 2^32, not ruling out values larger than 2^32. Hence, we need to use one more bit for z (in case of add5 it is 3 more bits I think), i.e.,

\sum_{i=0}^{31} 2^i x_i 2^i yi \sum{i=0}^{32} - 2^i z_i = 0

to encode the equality.

I tried to fix it and also add a nicer PB encoding for XORs in my fork at

https://github.com/StephanGocht/sha1-sat

However, the instance is still not solved by propagation in our solver roundingsat, when I set all input bits to fixed and no output bits to fixed, which I think it should, so there might be another problem with the encoding, which is why I didn't make a pull request.

[vegard]

Hi! Nice catch. As you could probably guess, the PB mode was never really used much -- I've mostly used the "halfadder" mode for CNF.

I understand the problem you're describing, I need to think a bit more about whether the solution is correct/sufficient...

[vegard]

Ok, I think your fixes look correct (I didn't check the xor2/xor3/xor4 improvements).

I've also seen that CNF instances are not solved immediately by propagation but have some low number of decisions/conflicts in MiniSat.

I'll try to figure it out when I get some time.

[StephanGocht]

In case it is of interest I made a python implementation for PB + CNF that also supports padding and length information so that the solutions can be checked against standard implementations of the hash function.

https://github.com/StephanGocht/hash_games/