Семинар за рачунарство и примењену математику, 27. мај 2014.

• 26. Мај, 2014
• Коментари (0)

Наредни састанак Семинара биће одржан у уторак, 27. маја 2014, са почетком у 14:15 часова у сали 301ф, Математичког института САНУ.

Предавач: Младен Николић, Математички факултет, Београд

Наслов предавања: SAT РЕШАВАЧИ - СИСТЕМИ ЗА ПРОВЕРУ ЗАДОВОЉИВОСТИ ИСКАЗНИХ ФОРМУЛА

Садржај: Проблем задовољивости исказних формула (SAT проблем) је један од централних проблема теоријског рачунарства.

Поред важног места у теорији сложености израчунавања, које му припада као првом доказано NP комплетном проблему, SAT проблем има и важне практичне примене у областима попут планирања, распоређивања и верификације хардвера и софтвера.

Практични значај овог проблема је инспирисао развој SAT решавача - система за проверу задовољивости исказних формула.

У претходним деценијама ови системи су доживели огроман напредак и у могућности су да провере задовољивост исказних формула које описују практичне проблеме и садрже десетине хиљада променљивих и стотине хиљада клауза. У овом излагању биће описано функционисање модерних SAT решавача.

Посебна пажња биће посвећена најпопуларнијем систему правила - CDCL систему, који служи као основа најефикаснијих SAT решавача.