Stručni rad
Problem ispunjivosti logičke formule (SAT)
Matej Mihelčić
; student na Prirodoslovno mateamtičkom fakultetu, Svučilište u Zagrebu
Tihomir Lolić
; student na Prirodoslovno mateamtičkom fakultetu, Svučilište u Zagrebu
Sažetak
U članku definiramo problem ispunjivosti formule logike sudova (SAT) i promatramo neke osnovne rezultate i primjene vezane uz navedeni problem. Opisat ćemo trenutno najvažniji potpuni algoritam za rješavanje problema ispunjivosti logičke formule: Davis-Putnam-Logeman-Loveland algoritam. Čitatelj će moći vizualizirati rad DPLL algoritma koristeći DPvis applet u kojem će moći interaktivno pokušati riješiti problem ispunjivosti nekih složenijih formula. Odjeljak o algoritmima nastavljamo predstavljanjem nekoliko glavnijih skupina heurističkih algoritama za rješavanje problema SAT. Predstavit ćemo prednosti i nedostatke svake skupine algoritama. Na kraju ćemo navesti i kratko opisati neke važnije verzije SAT problema.
Ključne riječi
Davis-Putnamov algoritam; logika sudova; pohlepni algoritam; SAT; slučajne šetnje
Hrčak ID:
103202
URI
Datum izdavanja:
30.6.2012.
Posjeta: 2.955 *