Referativní a výzkumný seminář o řešení problémů splnitelnosti. Hlavní náplní semináře budou algoritmické otázky týkající se problémů výrokové 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, heuristiky
• MaxSAT, SMT, QBF, walksat, survey propagation
• moderní SAT řešiče – glucose, clasp, MiniSAT, implementace
• modelování: kombinatorické úlohy, plánování, kódování, atd.