SAT doku Att lösa Sudoku med moderna SAT-lösare

Sammanfattning: 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.