[xiphias2]

Linear and differential cryptanalisis are the 2 classical way of breaking cryptographic hash functions, I think they are a cool way to learn about the importance of the current constructs being in use:

https://alldifferences.net/difference-between-linear-and-dif...

A simple way to look at them is this: if you change some specific bits in the input, maybe not all bits change by exacly 50% chance in the output, or they are not independent. For only a few rounds of S-Box-es you can probably find something like this by hand, for many rounds, SAT-solver or a special tool is needed.

[schoen]

Can you help me understand how one might use a SAT solver to find ways in which cryptographic primitives (or their components) deviate from ideal pseudorandomness?

I know what all of these things are, my intuition just isn't jumping to a way to formulate statistical correlations as a SAT problem.