Sudoku är ett mycket populärt pusselspel som härstammar från Japan. Sudokuproblemet har visats vara NP-fullständigt och det finns därför troligen inget effektivt sätt att lösa stora pussel. På senare år har det skett mycket forskning kring SAT-lösare. I denna rapport prövades olika SAT-lösare från ”International SAT-Competition” för att undersöka om det existerar en korrelation mellan exekveringstid och svårighetsgradering samt för att avgöra vilken av dessa som är effektivast för att lösa pussel av olika svårighetsgrad och storlek. För att undersöka detta genereradesett stort antal pussel och två tester utfördes. Ett test mätteexekveringstiden för olika SAT-lösare på pussel av olika svårighetsgrad.Det andra testet mätte tiden för SAT-lösarna på pussel av olika storlek.De prövade SAT-lösarna är Glucose, Lingeling, Minisat, Plingeling,Treengeling och Zenn.Resultaten visar på en korrelation mellan exekveringstid och svårighetsgradför de prövade SAT-lösarna när ett genomsnitt för lösarnabehandlades. Vid ett linjärt regressionstest erhölls en bestämningskoefficentpå ca 0.8. Vissa lösare hade en stor korrelation och andra lösarevisade inte någon korrelation alls. Korrelationen skulle också kunna beropå skillnaden i antalet ledtrådar mellan de olika pusslena. Det förklarardock inte den skillnad som finns mellan pussel av olika svårighetsgradmed samma antal ledtrådar.Genomsnittstiden för samtliga lösare var ca 20 ms för pussel avordning tre och ca 50 s för pussel av ordning nio. Av de prövade SATlösarnavar Minisat snabbast, både för pusslena av ordning tre och avhögre ordningar.

Sudoku is a popular puzzle game that originates from Japan. The Sudokuproblem has been shown to be NP-complete and therefore thereprobably does not exist an effecient way of solving large puzzles. In recentyears there has been a lot of research into solving the SAT problem.This report examined various SAT solvers from “The International SATCompetition” to investigate whether there exists a correlation betweenthe execution time and the difficulty level of puzzles and to determinewhich of these are most effective for solving puzzles of varying difficultyand size. To examine the above a large number of puzzles were generatedand two tests were performed. One test measured the executiontime of various SAT solvers when solving puzzles of varying difficulty.The second test measured the time that the SAT solvers took to solvepuzzles of different sizes. The tested SAT solvers are Glucose, Lingling,Minisat, Plingeling, Treengeling and Zenn.The results show a correlation between the execution time of theSAT solvers and the difficulty of the puzzles when looking at the averagetime of the solvers. A linear regression test gave a coefficent ofdetermination of approximately 0.8. Some solvers had a significant correlationand other solvers showed almost no correlation at all. Thecorrelation could also be attributed to the difference in the number ofclues between the puzzles. This however does not explain the disparitybetween puzzles of varying difficulty with the same number of clues.The average time for all solvers were approximately 20 ms for puzzlesof order three and about 50 s for puzzles of order nine. Of the testedSAT solvers, Minisat was the fastest at solving both the puzzles of orderthree and puzzles of higher order.