Math.e, Vol. 21 No. 1, 2012.
Professional paper
Problem ispunjivosti logičke formule (SAT)
Matej Mihelčić
; student at Faculty of Science, University of Zagreb
Tihomir Lolić
; student at Faculty of Science, University of Zagreb
Abstract
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.
Keywords
Davis-Putnamov algoritam; logika sudova; pohlepni algoritam; SAT; slučajne šetnje
Hrčak ID:
103202
URI
Publication date:
30.6.2012.
Visits: 2.984 *