How We Proved the 17 Clue Conjecture

Sudoku enthusiasts have long conjectured that a sound puzzle must have at least seventeen starting clues.  They were proved correct in early 2012, by a team of researchers led by the speaker.  They key advance was a new algorithm for solving the covering set problem, a question of general importance in computer science.  We will explain the major ideas that went into the proof, with particular emphasis on the close relationship between mathematics and computer science in modern research.