I like that he has examples that show CNF formulations next to SMT formulations. SMT is really easy to write, but it seems like magic. CNF draws back the curtain a bit.