February 13, Winter 2009: Theory Seminar

1:00pm in 253 ICS

Sudoku as a SAT Problem

by Ines Lynce, Joel Ouaknine,

From the proceedings of the 9th International Symposium on Artificial Intelligence and Mathematics [2006]

Presented by Rishab Nithyanand, UC Irvine

The Sudoku is a famous puzzle whose popularity has grown over the last few years. I will present the methods proposed in the mentioned paper for encoding a Sudoku in CNF and then solving the formula using polynomial time SAT inference rules.