SAT-based, MILP, and belief propagation preimage attacks on SHA-256 and other cryptographic hash functions