Seminar Katedre za računarstvo i informatiku, 22. mart 2018.

• 20. Mart,  2018
• Komentari (0)

Naredni sastanak Seminara biće održan u četvrtak, 22. marta 2018. u sali 718 Matematičkog fakulteta sa početkom u 18:15 časova.

Predavač: prof. dr Filip Marić

Naslov predavanja: BRZ FORMALNI DOKAZ ERDOŠ-SEKEREŠOVE HIPOTEZE ZA KONVEKSNE POLIGONE SA NAJVIŠE 6 TAČAKA

Apstrakt: Hipoteza koju su formulisali Klajn i Sekereš 1932 (danas poznata pod imenom "Erdoš-Sekerešova hipoteza" ili "Hipoteza sa srećnim krajem") tvrdi za svako m>=3 svaki skup koji sadrži 2^(m-2)+1 tačku u opštem položaju (nikoje tri različite tačke nisu kolinearne) sadrži konveksni m-trougao. Hipoteza je potvrđena za svako m<=6. Slučaj m=6 su nedavno rešili Sekereš i Peters pomoću računarske pretrage koja je konzumirala "više od 3000 GHz časova".

Opisujemo dokaz koji je unapređen u nekoliko smerova. Pomoću promene reprezentacije, razmatranja simetrija i pomoću modernih SAT rešavača, smanjili smo vreme dokaza na oko samo pola sata na običnom ličnom računaru (tj. naš dokaz zahteva samo oko 1 GHz čas). Takođe, formalizovali smo dokaz u dokazivaču Isabelle/HOL, što ga čini mnogo pouzdanijim.

---