How to fake an RSA signature by encoding modular root finding as a SAT problem