Naslov
Sustav za rješavanje zadovoljivosti formula propozicijske logike
(Satisfiability solver for propositional logic formulae)

Autori
Ivišić, Robert

Vrsta, podvrsta i kategorija rada
Ocjenski radovi, diplomski rad, diplomski

Fakultet
Fakultet elektrotehnike i računarstva

Mjesto
Zagreb

Datum
04.07

Godina
2012

Stranica
55

Mentor
Bogunović, Nikola

Neposredni voditelj
Bogunović, Nikola

Ključne riječi
propozicijska logika; zadovoljivost; rjršavač zadovoljivosti
(propositional logic; satisfiability; SAT solver)

Sažetak
U računarskoj znanosti zadovoljivost (skraćeno SAT) je problem određivanja vrijednosti logičkih (Booleovih) varijabli u formuli propozicijske logike tako da cijela formula poprimi istinitu vrijednost. Takav skup vrijednosti naziva se model formule. Jednako je važno ustanoviti da za neku formulu model ne postoji, t.j. da formula nije zadovoljiva. SAT problem je NP-kompletan i vjeruje se da ne postoji algoritam koji bi efikasno riješio zadovoljivost formule s proizvoljnim brojem varijabli. U radu je formalno definiran SAT problem, navedene su poznate tehnike i postupci rješavanja te je oblikovan i ostvaren jedan sustav za rješavanje zadovoljivosti. Navedene su neke tipične primjere uporabe i pokazano je kako se ti primjeri preslikavaju u SAT problem. Posebna pažnja posvećena je korisničkom sučelju kako bi ostvareni generički sustav bio primjenljiv u nizu specifičnih primjena.

Izvorni jezik
Hrvatski

Znanstvena područja
Računarstvo

POVEZANOST RADA