Sudoku vs. SAT