Riešenie odovzdávajte podľa pokynov na konci tohoto zadania do štvrtka 27.4. 23:59:59.
Súbory potrebné pre toto cvičenie si môžete stiahnuť ako jeden zip
pu09.zip.
Naprogramujte SAT solver, ktorý zisťuje, či je vstupná formula (v konjunktívnej normálnej forme) splniteľná.
Na prednáške ste videli základnú kostru metódy DPLL, ktorej hlavnou ideou je propagácia klauzúl s iba jednou premennou (jednotková klauzula, unit clause). Tá ale hovorí o veciach ako vymazávanie literálov z klauzúl a vymazávanie klauzúl, čo sú veci, ktoré nie je také ľahké efektívne (či už časovo alebo pamäťovo) implementovať, hlavne ak počas backtrackovania treba zmazané literály resp. klauzuly správne naspäť obnovovať.
Použite teda techniku sledovaných literálov z predchádzajúceho cvičenia na implementáciou DPLL solvera.
Základná kostra DPLL je nasledujúca:
- Inicializujeme sledované literály. Výsledkom tejto operácie je aj zoznam jednotkových klauzúl vo vstupe.
- Unit propagate: Kým je nejaká jednotková klauzula,
nastavíme jej
posledný nenastavený literál na
true. Toto samozrejme spôsobí presun niektorých sledovaných literálov a tiež môže pridať nové jednotkové klauzuly. - Ak už nemáme žiadnu jednotkovú klauzulu, vyberieme si nejaký literál
a postupne skúsime tento literál a potom jeho negáciu nastaviť na
true, pričom zakaždým rekurzívne pokračujeme od kroku 2. Samozrejme potom zase všetky nastavené literály „odnastavíme". Pozor: „Odnastavíme" aj literály, ktoré sme nastavili v rámci propagácie jednotkových klauzúl (viď backtrackovanie nižšie).
Prehľadávanie môžeme ukončiť, ak nájdeme spĺňajúce ohodnotenie (t.j. ohodnotíme všetky premenné a nenájdeme konflikt, teda nesplnenú klauzulu).
Na jednej „úrovni“ backtrackovania môže byť nastavených viacero literálov:
jeden keď zavoláme setLiteral a potom možno ďalšie v rámci propagácie
jednotkových klauzúl. Pri návrate ich treba všetky odnastaviť.
Najjednoduchšie sa to robí tak, že si na každej úrovni zapamätáme počet
už nastavených literálov a potom voláme unsetLiteral až kým sa nedostaneme
na rovnakú úroveň:
back = number of assigned literals
...
setLiteral
unit propagate
...
while (number of assigned literals > back)
unsetLiteral
Poznámka: V knižnici Theory.java je metóda
int nAssigned().
Riešenie odovzdajte do vetvy pu09 v adresári prakticke/pu09.
Odovzdávajte súbory Theory.java
a SatSolver.java.
Program SatSolverTest.java
musí korektne zbehnúť s vašou knižnicou.
Či ste správne vytvorili pull request si môžete overiť v tomto zozname PR pre pu09.
Odovzdávanie riešení v iných jazykoch konzultujte s cvičiacimi.