Семинар за рачунарство и примењену математику, 27. мај 2014.
- 26. Мај, 2014
- Коментари (0)
Наредни састанак Семинара биће одржан у уторак, 27. маја 2014, са почетком у 14:15 часова у сали 301ф, Математичког института САНУ.
Предавач: Младен Николић, Математички факултет, Београд
Наслов предавања: SAT РЕШАВАЧИ - СИСТЕМИ ЗА ПРОВЕРУ ЗАДОВОЉИВОСТИ ИСКАЗНИХ ФОРМУЛА
Садржај: Проблем задовољивости исказних формула (SAT проблем) је један од централних проблема теоријског рачунарства.
Поред важног места у теорији сложености израчунавања, које му припада као првом доказано NP комплетном проблему, SAT проблем има и важне практичне примене у областима попут планирања, распоређивања и верификације хардвера и софтвера.
Практични значај овог проблема је инспирисао развој SAT решавача - система за проверу задовољивости исказних формула.
У претходним деценијама ови системи су доживели огроман напредак и у могућности су да провере задовољивост исказних формула које описују практичне проблеме и садрже десетине хиљада променљивих и стотине хиљада клауза. У овом излагању биће описано функционисање модерних SAT решавача.
Посебна пажња биће посвећена најпопуларнијем систему правила - CDCL систему, који служи као основа најефикаснијих SAT решавача.
Коментари(0)