sha1-sat
sha1-sat copied to clipboard
vegard
PB Encoding Buggy
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 y_i \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.
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...
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.
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/