locuslab / SATNet

Bridging deep learning and logical reasoning using a differentiable satisfiability solver.
MIT License
405 stars 52 forks source link

different sign on the gradients dS, dz and line6 in algorithm 3 #18

Open Sichao-Yang opened 6 months ago

Sichao-Yang commented 6 months ago

Hi Dr. Po-Wei Wang

many thanks for opensourcing this greate work. When I read through your code. I have noticed there are a few differnce between the code and the paper:

  1. at src/satnet_cpu.cpp in function mix_kernel, for the backward pass, you use g = -(I-v_i v_i') (g+v_0 dz[i]), but I checked that based on the paper's algorithm 3 this should be dg=-P*(g - v_o dz[i]) with a minus sign? please correct me if im wrong.
  2. in the paper, for dl/dS and dl/zi, in both equation 11 and 12, there are minus signs. but in the code it becomes: dS = U W + V Phi and dzi = v0'Phi si. please can you tell me why the signs are reversed?

many thanks for you help! sichao y

xflash96 commented 5 months ago

Thanks for the check. It's been a few years but I remember this is because we changed the sign of dZ to save some computation... I.e., think the dz, U, and Phi in the code before returning gradient to be negated the symbol in the paper. The resulting gradient is still correct; we checked with gradcheck and you can also infer it from the symbol above.

But I agree that such change may not worth the clarity.