Martin Kot - Osobní stránka

Automatizované řešení úloh s omezeními - šk. rok 2012/13

Materiály ke cvičením

01.11.2012	Minisat - domovská stránka
01.11.2012	Minisat - linuxová binárka
01.11.2012	Minisat - windowsovská binárka
01.11.2012	MiniSAT User Guide: How to use the MiniSAT SAT Solver
08.11.2012	Stránka s variantami sudoku (fed-sudoku.eu) pro příklady k projektům
08.11.2012	Stránka s variantami sudoku (sudokuvariante.blogspot.cz/) pro příklady k projektům
08.11.2012	Stránka s killer sudoku pro příklady k projektům
15.11.2012	Domovská stránka UBCSAT
15.11.2012	Příklady CNF souborů
15.11.2012	Generátor CNF souborů pro n dam na šachovnici
15.11.2012	Vygenerované instance pro 8, 50 a 100 dam
06.12.2012	Stránka řešiče SAT sat4j
06.12.2012	Popis formátu AIG - jednoho z možných vstupních formátů pro řešiče SAT
06.12.2012	Stránka programu Abscon 109
06.12.2012	Popis XCSP 2.0 formátu pro řešiče CSP (akceptován např. sat4j, Abscon 109, ...)
06.12.2012	4 dámy - XCSP 2.0 soubor, extension verze
06.12.2012	4 dámy - XCSP 2.0 soubor, intension verze
06.12.2012	Zebra - XCSP 2.0 soubor
15.01.2013	Ukázková zápočtová písemka
15.01.2013	Řešená ukázková zápočtová písemka

Přednášky - slidy

27.09.2012	Organizační informace, požadavky apod., příklady úloh s omezeními
27.09.2012	Základní pojmy
25.10.2012	Šíření omezení
1.11.2012	Prohledávání, algoritmy pro dopředný pohyb
1.11.2012	Prohledávání, algoritmy pro zpětný pohyb
1.11.2012	Problém SAT a jeho NP-úplnost
16.12.2012	Problém SAT, jeho varianty a metody řešení
16.12.2012	Soubor satsolvers.pdf - naskenované obrázky z knihy Logic in Computer Science ke slidům k problému SAT
16.12.2012	Optimalizační problémy
16.12.2012	On-line plánování

R. Dechter - slidy