Sustav za rješavanje zadovoljivosti formula propozicijske logike (CROSBI ID 372749)
Ocjenski rad | diplomski rad
Podaci o odgovornosti
Ivišić, Robert
Bogunović, Nikola
Bogunović, Nikola
hrvatski
Sustav za rješavanje zadovoljivosti formula propozicijske logike
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.
propozicijska logika; zadovoljivost; rjršavač zadovoljivosti
nije evidentirano
engleski
Satisfiability solver for propositional logic formulae
nije evidentirano
propositional logic; satisfiability; SAT solver
nije evidentirano
Podaci o izdanju
55
04.07.2012.
obranjeno
Podaci o ustanovi koja je dodijelila akademski stupanj
Fakultet elektrotehnike i računarstva
Zagreb