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 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.