cv04

Cvičenie 4

Riešenie odovzdávajte podľa pokynov na konci tohoto zadania do Nedele 23.3. 23:59:59.

Sudoku (4b)

Implementujte triedu SudokuSolver ktorá pomocou SAT solvera rieši sudoku.

Trieda musí mať metódu solve, ktorá ako jediný parameter dostane vstupné sudoku: dvojrozmerné pole 9x9 čísel od 0 až 9, kde 0 znamená prázdne políčko. Metóda vráti ako výsledok dvojrozmerné pole 9x9 čísel od 1 po 9 reprezentujúce (jedno možné) riešenie vstupného sudoku.

Ak zadanie sudoku nemá riešenie, metóda solve vráti dvojrozmerné pole obsahujúce samé nuly.

Sudoku:

• štvorcová hracia plocha rozmerov 9x9 rozdelená na 9 podoblastí rozmerov 3x3
• cieľom je do každého políčka vpísať jednu z číslic 1 až 9

pričom musíme rešpektovať obmedzenia:

• v stĺpci sa nesmú číslice opakovať
• v riadku sa nesmú číslice opakovať
• v každej podoblasti 3x3 sa nesmú číslice opakovať

Pomôcka: Pomocou výrokovologickej premennej s_i_j_n (0 ≤ i,j ≤ 8, 1 ≤ n ≤ 9) môžeme zakódovať, že na súradniciach [i,j] je vpísané číslo n.

Pomôcka 2: Samozrejme potrebuje zakódovať, že na každej pozícii má byť práve jedno číslo (t.j. že tam bude aspoň jedno a že tam nebudú dve rôzne).

Pomôcka 3: Podmienky nedovoľujúce opakovanie číslic môžeme zapísať vo forme implikácií: s_i_j_n -> -s_k_l_n pre vhodné indexy i,j,k,l. (spomeňte si, ako sme riešili problém N-dám)

Pomôcka 4: Pre SAT solver musíme výrokovologické premenné s_i_j_n zakódovať na čísla (od 1). s_i_j_n môžeme zakódovať ako číslo 9 * 9 * i + 9 * j + n, kde 0 ≤ i,j ≤ 8 a 1 ≤ n ≤ 9.

Pomôcka 5: Opačná transformácia, teda SAT solver nám dá číslo x a chceme vedieť pre aké i, j, n platí x = s_i_j_n (napríklad 728 je kód pre s_8_8_8): keby sme nemali n od 1, ale od 0 (teda rovnako ako súradnice), bolo by to vlastne to isté ako zistiť cifry čísla x v deviatkovej sústave. Keďže je od 1, ale je na mieste 'jednotiek' (tj n * 90), stačí nám pred celou operáciou od neho odčítať jedna (a potom zase pripočítať 1 k n).

Technické detaily riešenia

Riešenie odovzdajte do vetvy cv04 v adresári cv04.

Všetky ukážkové a testovacie súbory k tomuto cvičeniu si môžete stiahnuť ako jeden zip súbor cv04.zip.

V priečinku examples/sat môžete nájsť knižnicu s dvoma pomocnými triedami DimacsWriter a SatSolver, ktoré vám môžu uľahčiť prácu so SAT solverom. Príklad ich použitia (a čiastočne aj vzorové riešenie cvičenia 2) možete nájsť v priečinku examples/nqueens.

Python

Odovzdajte súbor sudoku.py v ktorom je implementovaná trieda SudokuSolver obsahujúca metódu solve. Metóda solve má jediný argument: dvojrozmernú maticu čísel (zoznam zoznamov čísel) a vracia rovnako dvojrozmernú maticu čísel.

Program cv04test.py musí korektne zbehnúť s vašou knižnicou (súborom sudoku.py, ktorý odovzdáte).

Ak chcete použiť knižnicu z examples/sat, nemusíte si ju kopírovať do aktuálne adresára, stačí ak na začiatok svojej knižnice pridáte

import sys
sys.path[0:0] = [os.path.join(sys.path[0], '../examples/sat')]

C++

Odovzdajte súbory sudoku.h a sudoku.cpp obsahujúce triedu SudokuSolver ktorá implementuje interface AbstractSudokuSolver z AbstractSudokuSolver.h.

Program cv04test.cpp musí byť skompilovateľný keď k nemu priložíte vašu knižnicu (súbory sudoku.h/sudoku.cpp, ktoré odovzdáte).

###Java: Odovzdajte súbory SudokuSolver.java obsahujúce triedu SudokuSolver ktorá implementuje interface AbstractSudokuSolver z AbstractSudokuSolver.java.

Program Cv04Test.java musí byť skompilovateľný, keď sa k nemu priloží vaša knižnica.