Michael Jakovlev, SAT - solver v signovanej logike,doc. RNDr. Dušan Guller, PhD., jakovlev2@uniba.sk
Uvažujme viachodnotovú propozičnú logiku s množinou pravdivostných hodnôt Q. Signovaná rezolúcia pracuje nad signovanými klauzulami tvaru S1:p1 v...v Sn:pn, kde Si sú signá - podmnožiny Q.
Takáto klauzula je splnená v interpretácii V - ohodnotení propozičných atómov pi ak existuje aspon jeden signovaný literal Si:pi v klauzule, že V(pi) patrí do Si. Vašou úlohou bude implementovať spomínané refutačné dokazovacie procedúry.
Cieľom práce je vytvorenie SAT - solvera v signovanej logike na základe signovanej binárnej a hyper rezolúcie
vsetky zdroje sa daju najst tu - https://dai.fmph.uniba.sk/~guller/signed_logic/
zdrojove kody sa daju najst tu - https://github.com/jakino22/bakalarka
text prace sa da najst tu https://www.overleaf.com/read/vpmxdjftsjdj#147783
Toto je stranka progresu mojej Bakalarskej prace
Cez zimny semester som uspesne spravil translate na preklad akejkolvek finitnej
logiky do singovanej logiky
19.2-25.2:
Ciele:
- Dokoncenie DPL algoritmu - Splnene
- Vracanie ohodnoteni variables - pracuje sa na tom
- Dokaz translate algoritmu-bude napisany neskor
Za tento tyzden boli zhromazdene zdroje a napisane dve strany teoretickej casti
25.2-3.3
devat stran teoretickej casti-hotovo
4.3-10.3
implementacia najdenia ohodnotenia premennych-done
11.3 - 17.3
13 stran - uvod do problematiky - done
17.3 - 24.3
dokoncene graficke rozhranie
24.3 - 31.3
Pisanie vysledkov prace
1.4-8.4
Pisanie vysledkov prace a pridanie
funkcionality (designated values) do algoritmu
a aj grafickeho rozhrania
9.4-14.4
Pisanie vysledkov prace, implementacia WalkSAT
15.4-21.4
Porovnanie algoritmov signed-DPLL a WalkSAT
na pripravenych testoch
22.4-28.4
Dokoncenie pisania vysledkov prace
29.4-5.5
Napisanie abstraktu, uvodu a zaveru
6.5-12.5
Preorganizovanie prace a uprava textu