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.

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