This repository is an implementation of the MIT OCW 6.005 course problem assignment 4 (2011 version, now outdated and archived here). Visit this page for the currently active version of the course.
The Sudoku Solver with SAT solves Sudoku puzzles by representing the game constraints with propositional formulas in CNF
(Conjunctive Normal Form). These formulas are then solved by an implementation of
SAT, which is constructed following
the DPLL algorithm. More details about the problem assignment can be
found in the Instructions.pdf file in the project root directory.
To run this project the IntelliJ IDEA IDE is recommended.
To execute the Sudoku solver it is enough opening the src/sudoku/Main.java file and running the main() method.
Warning: 2x2 grids aren't supported, as they require shortening the range of admissible values from 1..9 to something else. Besides that, each component of this project has been extensively tested and worked fine (and with good performance) in all the cases covered so far.