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 2009/2010, 0/2 Z, úterý 9:00 - 10:30 S301/SU1 (začíná se 2.3.2010 v S301)
Úmluva: Již proběhla.

Plakát semináře (reklama na úmluvu)  [PDF]   |   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

• 2.3.2010: Pavel Surynek - Problémy SAT a CSP, základní řešící techniky pro SAT a CSP
• 9.3.2010: Praktické řešení problémů (v laboratoři): Dimacs CNF formát, Minisat
• 16.3.2010: Pavel Surynek - Lokální techniky
• 23.3.2010: Praktické řešení problémů (v laboratoři): rovnosti/nerovnosti pro bitové vektory
• 30.3.2010: Pavel Surynek - Kliková konzistence (semetrie se nestihly, budou jindy)
• 6.4.2010: Praktické řešení problémů (v laboratoři): aritmetika pro bitové vektory
• 13.4.2010: Adam Nohejl - Chaff: Engineering an Efficient SAT Solver
• 20.4.2010: Praktické řešení problémů (v laboratoři): perfektní čtverec
• 27.4.2010: Odpadne
• 4.5.2010: Praktické řešení problémů (v laboratoři): dokončení perfektního čtverce
• 11.5.2010: Václav Vlček - Obtížné instance SAT
• 18.5.2010: Praktické řešení problémů (v laboratoři): pravděpodobně lokální techniky