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

https://hrcak.srce.hr/103202

Datum izdavanja:

30.6.2012.

Posjeta: 2.480 *