Seminar za računarstvo i primenjenu matematiku, 27. maj 2014.

• 26. Maj,  2014
• Komentari (0)

Naredni sastanak Seminara biće održan u utorak, 27. maja 2014, sa početkom u 14:15 časova u sali 301f, Matematičkog instituta SANU.

Predavač: Mladen Nikolić, Matematički fakultet, Beograd

Naslov predavanja: SAT REŠAVAČI - SISTEMI ZA PROVERU ZADOVOLjIVOSTI ISKAZNIH FORMULA

Sadržaj: Problem zadovoljivosti iskaznih formula (SAT problem) je jedan od centralnih problema teorijskog računarstva.

Pored važnog mesta u teoriji složenosti izračunavanja, koje mu pripada kao prvom dokazano NP kompletnom problemu, SAT problem ima i važne praktične primene u oblastima poput planiranja, rasporedjivanja i verifikacije hardvera i softvera.

Praktični značaj ovog problema je inspirisao razvoj SAT rešavača - sistema za proveru zadovoljivosti iskaznih formula.

U prethodnim decenijama ovi sistemi su doživeli ogroman napredak i u mogućnosti su da provere zadovoljivost iskaznih formula koje opisuju praktične probleme i sadrže desetine hiljada promenljivih i stotine hiljada klauza. U ovom izlaganju biće opisano funkcionisanje modernih SAT rešavača.

Posebna pažnja biće posvećena najpopularnijem sistemu pravila - CDCL sistemu, koji služi kao osnova najefikasnijih SAT rešavača.

---