pu02

Cvičenie 2

Riešenie prvého cvičenia odovzdávajte do stredy 3.3. 23:59:59.

Či ste správne vytvorili pull request (PR) si môžete overiť v tomto zozname PR pre pu01.

Riešenie tohto cvičenia (úloha Sudoku) odovzdávajte do stredy 3.3. 23:59:59.

Či ste správne vytvorili pull request si môžete overiť v tomto zozname PR pre pu02.

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

Odovzdanie cvičenia 1

Podľa návodu na odovzdávanie riešení odovzdajte riešenie prvého cvičenia. Riešenie odovzdajte do vetvy (branch) pu01 v adresári prakticke/pu01.

Odovzdajte dva súbory: spyTheory.txt ktorý obsahuje „textovú“ verziu vstupu pre SAT solver (s atómami „N(M)“, „R(M)“ atď.) obsahujúcu teóriu a spyGoal.txt obsahujúci správne znegované tvrdenie, ktoré chcete dokázať.

Sudoku

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 9×9 čísel od 0 po 9, kde 0 znamená prázdne políčko. Metóda vráti ako výsledok dvojrozmerné pole 9×9 čí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.

Pri riešení tej úlohy sa môžete inšpirovať nasledovnými príkladmi:

• party – úvodný príklad s párty, „ručne“ zapisuje do súboru a púšťa SAT solver,
• N-queens – veľmi podobný príklad ako sudoku (ukladanie dám na šachovnicu), používa pomocné knižnice z examples/sat na zápis DIMACS vstupu a pustenie SAT solvera.

Sudoku:

• štvorcová hracia plocha rozmerov 9×9 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 3×3 sa nesmú číslice opakovať.

Pomôcka: Pomocou atómu 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.

Pomôcka 4: Pre SAT solver musíme atómy 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ódom 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).

Technické detaily riešenia

Riešenie odovzdajte do vetvy pu02 v správnom adresári podľa jazyka, v ktorom ste ho naprogramovali.

Python

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álneho 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')]
import sat

C++

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 (odovzdávané súbory).

Java

Odovzdajte súbor SudokuSolver.java obsahujúci triedu SudokuSolver s metódou solve s nasledovnou deklaráciou:

public static int[][] solve(int[][] sudoku)

Program SudokuTest.java musí byť skompilovateľný, keď sa k nemu priloží vaša knižnica (odovzdávaný súbor).

Ako si otvoriť javovský projekt v IntelliJ IDEA a spustiť testovací program si môžete pozrieť na tomto videu: