SAT-Based Analysis of Cellular Automata