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í: kombinatorické úlohy, plánování atd.

Čas od času se bude seminář konat v počítačové laboratoři, kde budeme provádět experimenty s nastudovanými technikami.

Rozvrh: letní semestr, 0/2 Z středa 15:40 - 17:10 S8/SU1 (začíná se 23.2.2011 v SU1)
Ú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

• 23.2.2011: Praktický seminář - organizace, souteže v SATu
• 2.3.2011: Radek Miček - SAT řešiče založené na DPLL [PDF]; Andrej Chovanec - Lokální techniky: ESG, SAPS
• 9.3.2011: Praktický seminář - generátor malých obtížných formulí

Vytvořený kód z 9.3.2011 hardgen-0.01.tgz: Rozpracovaný generátor (těžkých) formulí založený na genetickém programování.

• 16.3.2011: Martin Babka - (4/3)ⁿ algoritmus pro splnitelnost [PDF]
• 23.3.2011: Praktický seminář - pokračování s generátorem malých obtížných formulí

Vytvořený kód z 23.3.2011 a později hardgen-0.02.tgz: Nová verze generátoru (těžkých) formulí využívajícího genetické programování. Pozn.: Je potřeba opravit zavíráni souborů. Konrétně soubor fitness.cnf je nutné zavřít dříve než je zavolán MiniSat. hardgen-0.03.tgz: Opraveno zavírání souborů a generování nové populace, jako fitness se místo počtu rozhodnutí používá počet propagací kombinovaný s počtem klauzulí (zatím je použita stále jen mutace, křížení ještě použito není).

• 30.3.2011: Tomáš Balyo - Paralelní algoritmy pro SAT
• 6.4.2011: Praktický seminář - pokračování s generátorem malých obtížných formulí

Vytvořený kód z 6.4.2011 a později hardgen-0.04.tgz: Nová verze generátoru (těžkých) formulí využívajícího genetické programování. Nyní jsou implementovány všechny potřebné vlastnosti, tj. mutace a křížení. Možno dále experimentovat s fitness funkcí. Pozn.: Kód odpovídá přesně stavu na konci semináře. hardgen-0.05.tgz: Verze s vylepšenou fitness funkcí. Bere se v úvahu počet propagací a počet rozhodnutí, fitness funkce se mírně dynamicky adaptuje. hardgen-0.11.tgz: Fitness je nyní vektor hodnot (počet konfliktů, počet rozhodnutí, ...), přičemž nejdůležitější složkou je počet konfliktů. Plus mnoho dalších drobných vylepšení.

• 13.4.2011: Odpadne - konference
• 20.4.2011: Praktický seminář - Tomáš Balyo - Jazyk pro formule; Martin Babka - Lloydova 15-ka; a další
• 27.4.2011: Andrej Chovanec - ILP - Inductive Logic Programming
• 4.5.2011: Praktický seminář
• 11.5.2011: Tomáš Čapka - SAT Preprocessing [PDF]
• 18.5.2011: Odpadne - rektorský den
• 25.5.2011: Odpadne - konference