Zcela nový referativní seminář o řešení problémů splnitelnosti. Hlavní náplní semináře budou moderní algoritmické techniky pro řešení problémů booleovské splnitelnosti (SAT) a problémů splňování podmínek (CSP). Koncepty SAT a CSP představují důležité nástroje pro řešení složitých úloh v umělé inteligenci. Na semináři se mimo jiné se podíváme na: symetrie, konzistence, globální podmínky jednotková propagace, filtrace, sledování literálů, učení moderní SAT řešiče - MiniSAT, zChaff, PicoSat, RSAT modelování: diagnostika jako SAT, plánování jako SAT, atd.

Čas od času se bude seminář konat v počítačové laboratoři, kde budeme provádět experimenty s nastudovanými technikami. Zařazení experimentální části je u semináře úplně nový přístup, jsem přesvědčen, že bude přínosný.

Rozvrh: letní semestr, 0/2 Z
Úmluva: Bude na společné úmluvě KTIML (úterý 24.2.2009, 12:00, chodba S300).

Plakát semináře (reklama na úmluvu)  [PDF] [PS]   |   Seminář v SISu

Na rozmyšlenou: Pokuste se najít čtverec celočíselného obsahu, který lze rozdělit na několik různých menších čtverců rovněž celočíselného obsahu (viz. obrázek výše). Navrhněte program, který by úlohu dokázal vyřešit. Částečné řešení úlohy lze nalézt na plakátu k semináři.

Zatím známý program

• 26.2.2009: Pavel Surynek - Problémy SAT a CSP, základní řešící techniky pro SAT a CSP
• 5.3.2009: Tomáš Balyo - Heuristiky pro výběr proměnné v SATu
• 12.3.2009: Petr Michalík - Dynamický backtracking a související prohledávací strategie v CSP
• 19.3.2009: Martin Suda - Efektivní implementace jednotkové propagace (2 sledované literály)
• 26.3.2009: Všichni - Modelování problémů jako SAT, řešící systémy a exprimenty

• 2.4.2009: Martin Babka - Učení klauzulí
• 9.4.2009: Alexandr Kazda - Symetrie v SATu a struktura problémů
• 16.4.2009: Alexandr Kazda - Dodatky k minulému referátu
• 23.4.2009: Daniel Toropila - Konzistence v SATu
• 30.4.2009: Tomáš Huml - Modelování problémů
• 7.5.2009: Pavel Surynek - SAT pro model checking a STRIPS plánování