Семинар Катедре за рачунарство и информатику, 22. март 2018.

Наредни састанак Семинара биће одржан у четвртак, 22. марта 2018. у сали 718 Математичког факултета са почетком у 18:15 часова.

Предавач: проф. др Филип Марић

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

Апстракт: Хипотеза коју су формулисали Клајн и Секереш 1932 (данас позната под именом „Ердош-Секерешова хипотеза“ или „Хипотеза са срећним крајем“) тврди за свако m>=3 сваки скуп који садржи 2m-2+1 тачку у општем положају (никоје три различите тачке нису колинеарне) садржи конвексни m-тоугао. Хипотеза је потврђена за свако m<=6. Случај m=6 су недавно решили Секереш и Петерс помоћу рачунарске претраге која је конзумирала „више од 3000 GHz часова“.

Описујемо доказ који је унапређен у неколико смерова. Помоћу промене репрезентације, разматрања симетрија и помоћу модерних САТ решавача, смањили смо време доказа на око само пола сата на обичном личном рачунару (тј. наш доказ захтева само око 1 GHz час). Такође, формализовали смо доказ у доказивачу Isabelle/HOL, што га чини много поузданијим.