LVR-sat

DPLL

Ta modul vsebuje ogrodje za delo z logičnimi izrazi (datoteka Izjave.py), primera prevedbe znanih problemov (Hadamardove matrike in sudoku) na SAT, SAT solverja (DPLL.py) ter primere uporabe (datoteka Primeri.py).

Datoteke

V modulu se nahajajo datoteke:

• CNF.py (metode za pretvarjanje izrazov v konjuktivno normalno obliko)
• Hadamard.py (prevedba Hadamardove matrike na SAT problem)
• Izjave.py (osnovno ogrodje za delo z logičnimi izrazi)
• Primeri.py (primeri uporabe)
• Sudoku.py (prevedba sudoku na SAT problem)
• DPLL.py (SAT solver - DPLL algoritem)

Uporaba

Testno okolje

Za testiranje delovanja funkcij, so v vsaki datoteki temu namenjene metode.

CNF

CNF.py datoteka vsebuje le funkcijo CNF(p), kjer je p izjava, katero želimo prevesti v CNF obliko.

V datoteki se nahaja tudi funkcija test(), ki testira delovanje CNF. Poženemo jo iz konzole. Beležimo tudi čas izvajanja funkcije CNF.

Hadamard

Hadamard.py je sestavljen iz dveh funkcij in sicer stetje(m, sez) in hadamard(n). Funkcija stetje sprejme seznam izjav sez in število m, vrne pa izjavo, ki je resnična natanko tedaj, ko je v seznamu izjav sez resničnih natanko m izjav. Hadamard funkcija pa sprejme velikost matrike in vrne izjavo, ki je resnična natanko tedaj, ko je matrika Hadamardova.

Testiranje delovanje je izvedeno s pomočjo funkcij testS(), ki testira delovanje funkcije stetje, ter testH(), ki testira delovanje funkcije hadamard. Obe kličemo iz konzole. testH beleži še hitrost delovanja za primer sestavljanja izjave za hadamardovo matriko in za primer sestavljanja izjave za hadamardovo matriko v CNF obliki, beleži se tudi razlika v hitrosti izvajanja med obema.

Opomba: Izvajanje programa za Hadamardovo matriko velikosti 4x4 je nekoliko počasnejše, zato prosimo za potrpežljivost.

Izjave

Izjave.py datoteka je sestavljena iz sledečih razredov:

• Var() (predstavlja spremenljivke)
• Tru() (predstavlja konstanto True)
• Fal() (predstavlja konstanto False)
• And() (predstavlja logični veznik And)
• Or() (predstavlja logični veznik Or)
• Not() (predstavlja negacijo)

Vsak razred (razen Tru() in Fal()) vsebuje funkcije:

• vrni (vrne objekt)
• nastavi (nastavimo vrednosti objektu; npr. v razredu Var() nastavimo ime spremenljivke)
• izracun (sprejme slovar vrednosti spremenljivk (npr. {'A':False,'B':True,'C':True}) in vrne valuirano izjavo)
• poenostavi (potisne vse negacije do spremenljivk, odstrani morebitne pojavitve Tru(), Fal() in odvečne oklepaje)

Razreda Tru() in Fal() vsebujeta le funkcijo izracun.

Izjave.py vsebujejo funkcijo za testiranje test(). V testu izvajamo poenostavljanje, računanje vrednosti izjave ter izpis nastopajočih spremenljivk. Za poenostavljanje in računanje vrednosti beležimo še čas izvajanja.

Sudoku

Sudoku.py vsebuje fukncijo sudoku(sez). Ta sprejme dvodimenzionalno tabelo (nxn matrika), ki predstavlja nerešen sudoku. Kot rezultat nam vrne izjavo, ki je resnična natanko tedaj, ko za dani sudoku obstaja rešitev.

Poleg sudoku funkcije vsebuje še testS(), s katero lahko testiramo delovanje. Beleži se tudi čas izvajanja za reševanje sudoku problema (sestavljanje izjave za sudoku), sestavljanje izjave v CNF obliki in razlika v hitrosti delovanja obeh.

DPLL

Algoritem DPLL vsebuje glavne funkcije pozdravnaMetoda(), ki nam razloži način klica DPLL algoritma in primere klicev. Algoritem DPLL sicer kličemo z ukazom "DPLL(izjava)", kjer je izjava sestavljena iz And, Or in Not operatorjev in se sklada s terminologijo v datoteki Izjave.py.

Testni primeri se nahajajo v funkciji getTestIzjava(N), kjer je N številka testnega primera in lahko zavzema vrednosti med 0 in 10.

Primeri

Tu se nahajajo primeri uporabe za Izjave.py, Hadamard.py, Sudoku.py, CNF.py in DPLL.py. Ob zagonu datoteke, se izvedejo primeri uporabe za Izjave (primeri za And, Or, Not, CNF in NNF), Sudoku (primer za sudoku velikosti 4x4 in 9x9), Hadamardovo matriko (primer za velikost 2 in 4) ter DPLL (primer za neko izjavo, 9x9 sudoku, 2x2 in 4x4 Hadamardovo matriko). Za sudoku, Hadamardove matrike in DPLL se beleži še čas izvajanja programa.