Cvičenie 3 -- SAT

Riešenie tejto úlohy odvzajte v moodli do 30.10.2014 13:09:59.

SAT solverov je veľa, budeme používať MiniSAT. Binárka pre windows sa dá stiahnuť priamo na ich stránke, ale potrebuje ešte 2 knižnice (cygwin1.dll, cygz.dll), všetky tri súbory sa dajú stiahnuť tu.

Príklad

Cheme na párty pozvať niekoho z trojice Jim, Kim a Sára, bohužiaľ každý z nich má nejaké svoje podmienky.

• Sarah nepôjde na party ak pojde Kim.
• Jim pôjde na párty, len ak pôjde Kim.
• Sara nepôjde bez Jima.

p cnf VARS CLAUSES
c komentar
1 2 -3 0
...

p cnf 3 4
c -kim v -sarah
-1 -3 0
c -jim v kim
-2 1 0
c -sarah v jim
-3 2 0
c k v j v s
1 2 3 0

Spustíme sat solver, ako parameter dáme meno vstupného súboru. MiniSAT normálne iba vypíše, či je vstup splniteľný, ak chceme aj nejaký výstup, tak dáme ešte meno výstupného súboru (MiniSAT ho vytvorí/prepíše.)

$ minisat party.cnf party.out
...
SATISFIABLE
$ cat party.out
SAT
1 -2 -3 0

MiniSAT nájde len nejaké riešenie, ak chceme nájsť ďašie, môžeme mu povedať, že toto konkrétne nechceme (nemajú naraz platiť tieto premenne). Toto riešenie je kim ∧ ¬jim ∧ ¬sarah, znegovaním dostaneme ¬kim ∨ jim ∨ sarah, čo je priamo disjunktívna klauza a môžeme ju pridať k zadaniu:

p cnf 3 5
-1 -3 0
-2 1 0
-3 2 0
1 2 3 0
c nechceme riesenie 1 -2 -3
-1 2 3 0

$ minisat party.cnf party.out
...
SATISFIABLE
$ cat party.out
SAT
1 2 -3 0

Ak to zopakujeme ešte raz, nenájdeme už žiadne riešenie:

p cnf 3 6
-1 -3 0
-2 1 0
-3 2 0
1 2 3 0
c nechceme riesenie 1 -2 -3
-1 2 3 0
c nechceme riesenie 1 2 -3
-1 -2 3 0

$ minisat party.cnf party.out
...
UNSATISFIABLE
$ cat party.out
UNSAT

Sudoku (5b)

Napíšte program, ktorý pomocou SAT solvera rieši sudoku.

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ť

Odovzdajte program, ktorý načíta zo štandardného vstupu zadanie sudoku, vygeneruje vstup pre SAT solver, pustí ho, "dekóduje" výsledok a vypíše riešenie. (Ak máte problém so spúšťaním SAT solvera z vášho programovacieho jazyka, možete prípadne odovzdať aj dva programy, jeden ktorý generuje vstup pre SAT solver a druhý, ktorý dekóduje jeho výstup.)

Formát vstupu je nasledovný: 91 čísel od nula po deväť, oddelených medzerami alebo znakmi pre koniec riadku, ktoré reprezentujú sudoku po riadkoch zhora nadol (a zľava doprava), pričom 0 znamená nevyplnené políčko.

Výstupný formát je úplne rovnaký (preferovaný je koniec riadku po každých 9 číslach :), len obsahuje už vyplnené sudoku (žiadne nuly), ak sudoku má riešenie, alebo samé nuly, ak nemá riešenie.

 5 3   |   7   |
 6     | 1 9 5 |
   9 8 |       |   6
-------+-------+------
 8     |   6   |     3
 4     | 8   3 |     1
 7     |   2   |     6
-------+-------+------
   6   |       | 2 8
       | 4 1 9 |     5
       |   8   |   7 9

 5 3 0 0 7 0 0 0 0
 6 0 0 1 9 5 0 0 0
 0 9 8 0 0 0 0 6 0
 8 0 0 0 6 0 0 0 3
 4 0 0 8 0 3 0 0 1
 7 0 0 0 2 0 0 0 6
 0 6 0 0 0 0 2 8 0
 0 0 0 4 1 9 0 0 5
 0 0 0 0 8 0 0 7 9

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: 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 3: Pri takomto kódovaní musíme myslieť na podmienku, že v jednom políčku môže byť vpísaná iba jedna číslica.

Zápis tohto problému vo výrokovej logike bude obsahovať veľké množstvo formúl, ktoré vzniknú zo schém formúl dosadením za premenné. Preto v rámci riešenia napíšte jednoduchý program, ktorý vám uľahčí prácu a vygeneruje všetky potrebné formuly. Generátor napíšte tak, aby generoval formuly už v CNF forme.

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, 0 ≤ i,j ≤ 8.

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 n je od 1, ale je na mieste 'jednotiek' (tj n*9⁰), stačí nám pred celou operáciou od neho odčítať jedna (a potom zase pripočítať 1 k n).