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

https://hrcak.srce.hr/103202

Publication date:

30.6.2012.

Visits: 2.513 *