Problem ispunjivosti logi？ke formule (SAT)

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