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

Výsledky naší práce z 26.3.2009 Pavel Surynek: vsat 0.12 zdrojový kód  (vsat-0.12-wind.tgz) Experimentální SAT řešič (jednotková propagace, sledování 2 literálů, heuristika - první proměnná), zatím nepříliš výkonný, kód není komentován. Martin Babka: Lloyd-15 instance  (lloyd.tgz) Několik SAT instancí skládačky Lloydova 15-ka, soubor obsahuje řešitelné i něřešitelné problémy, přiložen je i generátor instancí napsaný v Javě. Tomáš Balyo: Sudoku instance  (sudoku.tgz) Několik SAT instancí Sudoku, soubor obsahuje pouze řešitelné problémy. Instance byly vygenerovány programem z internetové stránky: http://www.cs.qub.ac.uk/~i.spence/SuDoku/SuDoku.html. Popis způsobu kódování Sudoku jako SAT lze najít v Ines Lynce, Joel Ouaknine: Sudoku as a SAT Problem.

• 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í