Matematički fakultet Univerziteta u Beogradu

Seminar Katedre za računarstvo i informatiku


Jesenji semestar akademske 2016/2017. godine

Četvrtak, 8. 12. 2016. u 18.15h, Studentski Trg 16, sala 718

Milon Banković
Unapređivanje SMT rešavača korišćenjem CSP tehnika i tehnika paralelizacije
doktorska disertacija

Prikaži apstrakt

Problem zadovoljivosti u odnosu na teoriju (eng. Satisfiability Modulo Theory (SMT)) je problem ispitivanja da li postoji model neke unapred zadate teorije prvog reda u kome je data formula tačna. Softverski alati koji implementiraju procedure za rešavanje SMT problema zovu se SMT rešavači. Ovi alati se danas dominantno koriste u verifikaciji softvera. Zbog toga su tipične teorije koje se razmatraju u SMT-u prilagodjene upravo toj vrsti primene (teorija jednakosti sa neinterpretiranim funkcijskim simbolima, linearna aritmetika, teorija bitvektora, teorija nizova, itd.). U okviru ove teze razmatrani su pristupi za unapređivanje SMT rešavača. Jedan pravac unapređivanja SMT rešavača je definisanje novih SMT teorija. Ugradnja procedura odlučivanja za nove teorije u postojeće SMT rešavače omogućila bi širu primenjivost SMT tehnologija u rešavanju problema iz drugih oblasti. Jedna takva primena je rešavanje problema zadovoljavanja ograničenja (eng. Constraint Satisfaction Problem (CSP)). Postojeće SMT teorije nisu prilagođene rešavanju ovakvih problema, jer su CSP problemi po pravilu definisani nad konačnim domenima, dok tipične SMT teorije podrazumevaju beskonačne domene. Takođe, standardne SMT teorije nemaju mogućnost korišćenja globalnih ograničenja u formulaciji CSP problema, kao ni mogućnost rezonovanja o globalnim ograničenjima. Zbog toga je u okviru ove teze formulisana nova SMT teorija koja definiše sintaksu i semantiku nekih najčešćih globalnih ograničenja (pre svih ograničenja uzajamne različitosti, engl. alldifferent), a zatim je za takvu teoriju razvijena procedura odlučivanja koja je ugrađenja u DPLL(T) zasnovan SMT rešavač. Ova procedura je zasnovana na postojećim CSP tehnikama, pri čemu su te tehnike prilagođene SMT kontekstu i po potrebi proširene i unapređene. Na ovaj način smo u okviru SMT-a objedinili dobre strane SAT rešavača (efikasnost pretrage) i CSP rešavača (algoritmi prilagođeni globalnim ograničenjima). Za alldifferent ograničenje osmišljen je novi algoritam za generisanje objašnjenja konflikata i propagacija. Za linearno ograničenje osmišljen je novi poboljšani algoritam filtriranja koji koristi informacije o postojećim alldifferent ograničenjima u datom problemu za postizanje jačeg nivoa konzistentnosti. Za sve predložene algoritme i tehnike u okviru ovog dela teze data je i opsežna eksperimentalna evaluacija. Drugi skup tehnika kojima se SMT rešavači mogu unapređivati su tehnike paralelizacije, pre svega zahvaljujući ubrzanom razvoju višejezgarnih procesora koji su danas već uveliko dostupni. Tipični pristup u paralelizaciji SMT rešavača je tzv. paralelni portfolio, gde se više različito podešenih instanci rešavača pokreću istovremeno nad istom instancom problema, dok neka od njih ne pronađe rešenje. Alternativni pristup je paralelizacija vremenski zahtevnih algoritama u okviru procedura odlučivanja ugrađenih u SMT rešavače. U okviru ove teze implementiran je paralelni portfolio, a urađena je i paralelizacija simpleks procedure koja se u SMT-u koristi za ispitivanje zadovoljivosti u teoriji linearne aritmetike. Ova procedura je jedna od vremenski najzahtevnijih procedura u SMT-u, zbog čega je bilo očekivano da će njenom paralelizacijom doći do značajnog ubrzanja rada rešavača. Urađena je i opsežna eksperimentalna evaluacija navedenih pristupa paralelizaciji na velikom skupu, kako slučajno generisanih, tako i industrijskih instanci. Rezultati evaluacije prikazani u tezi govore u prilog paralelnom portfoliju, ali takođe pokazuju i značajne rezultate kada je u pitanju paralelizacija simpleksa. Takođe je evaluiran i hibridni pristup koji je takođe u nekim slučajevima dao dobre rezultate.


Četvrtak, 1. 12. 2016. u 18.15h, Studentski Trg 16, sala 718

Silvia Šušnjević i Borko Drašković, Enetel Solutions
Prediktivni alati za primenu u rešenjima eTrgovine i Georeferenciranoj poslovnoj analitici
stručna tribina

Prikaži apstrakt

Preciznost prediktivnih alata može biti iskorišćena kao komparativna prednost i kao tajno oruđe za donošenje ispravnih poslovnih odluka. Integracijom korisničkih podataka sa različitih sistema omogućava se kreiranje personalizovanih ponuda i predviđaju buduće potrebe korisnika korišćenjem prediktivne analitike, čime se ostvaruju ključni benefiti digitalne transformacije za naše klijente:

  • Optimzacija marketinških i prodajnih aktivnosti
  • Optimizacija logistike i nabavke
  • Povećanje podaje
  • Poboljšanje odnosa sa kupcima: povećanje lojalnosti brendu i smanjenje churn-a
  • Razvijanje poslovanja: proširenje na nova tržišta i oblasti poslovanja
  • Smanjenje operativnih troškova
IMPOQO: Impoqo predstavlja personalizovano, tailor made, smart eCommerce rešenje prilagođeno potrebama klijenata u okviru različitih grana industrije. Pažljivo kreirano eCommerce iskustvo doprinosi boljem korisničkom iskustvu, povećava korisničko zadovoljstvo, poverenje u brend, a samim tim i utiče na povećanje prodaje naših klijenata. Za Impoqo, personalizacija se ogleda u individualanom pristupu- mogućnosti da se u realnom vremenu isporuče relevantna, kontekstualna digitalana iskustva u svakom trenutku zavisno od potreba korisnika.

GEOTELEMARK: Geotelemark je softversko rešenje za poslovnu, georeferenciranu analitiku. Osnovni zadatak Geotelemarka je da prikupi, objedini, analizira i, kao rezultat, prikaže na mapi veliku količinu raznorodnih, georeferenciranih, podataka (podaci o različitim tipovima infrastrukture‚ komercijalne i demografske podatke iz više različitih izvora: Inventory, CRM, različita istraživanja tržišta, zavod za statistiku, geodetski zavod, hidrometeorološki zavod i dr.) Intuitivnost u radu sa georeferenciranim podacima, u kombinaciji sa snažnom analitikom omogućavaju uočavanje veza koje nije moguće zapaziti kada su podaci prikazani u tabelarnoj formi. Ova osobina Geotelemarka odvaja ga od standardnih BI rešenja. Detaljnije podatke o svemu možete videti na našem sajtu www.geotelemark.com.
Geotelemark i Impoqo omogućavaju prediktivne uvide kako bi se korisnici bolje razumeli i maksimizovala CLV (customer lifetime value).


Četvrtak, 3. 11. 2016. u 18.15h, Studentski Trg 16, sala 718

Miloš Stanković, Google
How (not) to write features at Google
stručna tribina

Prikaži apstrakt

На предавању ће студенти сазнати како изгледа свакодневни посао софтверског инжењера у великој компанији Google. На крају предавања биће речи о Google-овом програму студентских пракси, процесу интервјуисања и запошљавања итд. Google поседује широк спектар пракси и послова и презентација је прилагођена свима, те су добродошли сви студенти. Поред предавача, на предавању ће учествовати и Никола Јовановић (студент МатФ-а који је ове године био на пракси у Google-у).


Četvrtak, 13. 10. 2016. u 18.15h, Studentski Trg 16, sala 718

Mirko Stojadinović
Rešavanje problema CSP tehnikama svođenja na problem SAT
doktorska disertacija

Prikaži apstrakt

Mnogi realni problemi se danas mogu predstaviti u obliku problema zadovoljenja ograničenja (CSP) i zatim rešiti nekom od mnogobrojnih tehnika za rešavanje ovog problema. Jedna od tehnika podrazumeva svođenje na problem SAT, tj. problem iskazne zadovoljivosti. Promenljive i ograničenja problema CSP se prevode (kodiraju) u SAT instancu, ona se potom rešava pomoću modernih SAT rešavača i rešenje se, ako postoji, prevodi u rešenje problema CSP. Glavni cilj ove teze je unapređenje rešavanja problema CSP svođenjem na SAT. Razvijena su dva nova hibridna kodiranja (prevođenja u SAT formulu) koja kombinuju dobre strane postojećih kodiranja. Dat je dokaz korektnosti jednog od kodiranja koji do sada nije postojao u literaturi. Razvijen je sistem meSAT koji omogućava svođenje problema CSP na SAT pomoću četiri osnovna i dva hibridna kodiranja, kao i rešavanje problema CSP svođenjem na dva problema srodna problemu SAT, SMT i PB. Razvijen je portfolio za automatski odabir kodiranja/rešavača za ulaznu instancu koju je potrebno rešiti i pokazano je da je razvijeni portfolio uporediv sa najefikasnijim savremenim pristupima. Prikazan je novi pristup zasnovan na kratkim vremenskim ograničenjima sa ciljem da se značajno smanji vreme pripreme portfolija. Pokazano je da se ovim pristupom dobijaju rezultati konkurentni onima koji se dobijaju korišćenjem standardnog vremena za pripremu. Izvršeno je poređenje nekoliko tehnika mašinskog učenja, sa ciljem da se ustanovi koja od njih je pogodnija za pristup sa kratkim treniranjem. Prikazan je jedan realan problem, problem raspoređivanja kontrolora leta, kao i tri njegova modela. Veliki broj metoda rešavanja i raznovrsnih rešavača je upotrebljeno za rešavanje ovog problema. Razvijeno je više optimizacionih tehnika koje imaju za cilj pronalaženje optimalnih rešenja problema. Pokazuje se da je najefikasnija hibridna tehnika koja kombinuje svođenje na SAT i lokalnu pretragu. Razmotren je i problem sudoku, kao i postojeće tehnike rešavanja sudoku zagonetki većih dimenzija od 9 × 9. Pokazuje se da je u rešavanju ovih zagonetki najefikasnije već postojeće svođenje na SAT. Unapređen je postojeći algoritam za generisanje velikih sudoku zagonetki. Pokazano je da jednostavna pravila preprocesiranja dodatno unapređuju brzinu generisanja sudokua.


Raniji sastanci

2015/16. godina (letnji, zimski)
2014/15. godina (letnji, zimski)
2013/14. godina (letnji, zimski)
2012/13. godina (letnji, zimski)
2011/12. godina (letnji, zimski)
2010/11. godina (letnji, zimski)
2009/10. godina (letnji, zimski)


Seminar

Seminar Katedre za računarstvo i informatiku vodi poreklo od Seminara za računarstvo i informatiku, osnovanog daleke 1977. godine. Od osnivanja Katedre, 1987. godine, Seminar radi, sa povremenim kraćim prekidima, pod sadašnjim imenom. Seminar je osnovao i prvi rukovodio njime prof. Nedeljko Parezanović. Kasniji rukovodioci Seminara bili su prof. Vojislav Stojković, prof. Gordana Pavlović- Lažetić, doc. Nenad Mitić, prof. Duško Vitas. Na Seminaru se izlažu naučni razultati iz različitih oblasti računarstva, istraživača sa Matematičkog fakulteta kao i gostujućih istraživača iz zemlje i inostranstva.

Sastanci se (uz izuzetke) održavaju svakog drugog četvrtka od 18h u prostorijama Matematičkog fakulteta na Studentskom trgu.


Aktuelni rukovodilac seminara je prof. Miodrag Živković.