Riešenie prvého cvičenia odovzdávajte do utorka 8.3. 23:59:59.
Riešenie tohto cvičenia (úloha Sudoku) odovzdávajte
do utorka 8.3. 23:59:59 štvrtka 10.3. 23:59:59.
Všetky ukážkové a testovacie súbory k tomuto cvičeniu si môžete stiahnuť ako jeden zip súbor cv02.zip.
Podľa návodu na odovzdávanie riešení odovzdajte
riešenie prvého cvičenia. Riešenie odovzdajte do vetvy (branch) cv01
v adresári cv01.
Odovzdajte súbor spy.txt ktorý obsahuje „textovú“ verzia vstupu pre SAT solver
(s názvami premenných „GM“, „RM“ atď.) vrátane správne znegovaného tvrdenia,
ktoré chcete dokázať.
Pomocou SAT solvera vyriešte problém N-dám:
Máme šachovnicu rozmerov N×N. Na ňu chceme umiestniť N šachových dám
tak, aby sa navzájom neohrozovali. Ohrozovanie dám je v zmysle
štandardných šachových pravidiel:
- žiadne dve dámy nemôžu byť v rovnakom riadku
- žiadne dve dámy nemôžu byť v rovnakom stĺpci
- žiadne dve dámy nemôžu byť na tej istej uhlopriečke
Pomôcka: Použite výrokové premenné q_i_j, 0 ≤ i,j < N,
ktorých pravdivostná hodnota bude hovoriť, či je alebo nie je na pozícii i,j
umiestnená dáma.
Pomôcka 2: Pre SAT solver musíme premenné q_i_j zakódovať na čísla.
Keďže platí 0 ≤ i, j < N, premennú q_i_j môžete zakódovať ako číslo
N*i + j + 1. Napíšte si na to funkciu! Ideálne s názvom q. Jednoduchšie
sa vám budú opravovať chyby a ľahšie sa to číta / opravuje.
Pomôcka 3: Nemusíme počítať počet dám. Stačí požadovať, že v každom riadku
musí byť nejaká dáma (určite nemôžu byť dve dámy v tom istom riadku, keďže ich
má byť N, musí byť v každom riadku práve jedna).
Pomôcka 4: Ostatné podmienky vyjadrujte vo forme jednoduchých implikácií:
q_X_Y → ¬q_X_Z pre X,Y,Z ∈ <0,N), Y≠Z
(ak je v riadku X dáma na pozícii Y, tak nemôže byť iná dáma v tom istom
riadku), atď.
Pomôcka 5: V priečinku examples/party je ukážkový program
(c++ a python), ktorý môžete použiť ako kostru vášho riešenia.
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.
Riešenie implementujte ako triedu NQueens, ktorá má metódu solve. Metóda
solve má jediný argument N (číslo – počet dám) a vracia zoznam dvojíc čísel
(súradnice dám). Priložené testy by mali s vašou triedou zbehnúť!
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 (9×9) obsahujúce samé nuly.
Sudoku:
- štvorcová hracia plocha rozmerov 9x9 rozdelená na 9 podoblastí rozmerov 3×3
- 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ýrokovej 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: 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 n je od 1, ale
je na mieste 'jednotiek' (t.j. n * 90), stačí nám pred
celou operáciou od neho odčítať jedna (a potom zase pripočítať 1 k n).
Riešenie odovzdajte do vetvy cv02 v adresári cv02.
Odovzdajte súbor SudokuSolver.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 sudokuTest.py musí korektne zbehnúť s vašou knižnicou
(súborom SudokuSolver.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
import os
sys.path[0:0] = [os.path.join(sys.path[0], '../examples/sat')]Odovzdajte súbory SudokuSolver.h a SudokuSolver.cpp, v ktorých je implementovaná
trieda SudokuSolver ktorá obsahuje metódu solve s nasledovnou
deklaráciou:
std::vector<std::vector<int> > solve(const std::vector<std::vector<int> > &sudoku)Program sudokuTest.cpp musí byť skompilovateľný keď k nemu
priložíte vašu knižnicu.
###Java:
Odovzdajte súbor SudokuSolver.java obsahujúci triedu SudokuSolver s metódou public static int[][] solve(int[][] sudoku).
Program SudokuTest.java musí byť skompilovateľný, keď sa k
nemu priloží vaša knižnica.