..:: Martin Kot ::..
Automatizované řešení úloh s omezeními - šk. rok 2012/13
Obecné informace o projektech
Každý student dostane slovně zadán nějaký problém a přidělen (volně dostupný) softwarový nástroj, s jehož pomocí jej má řešit (Gecode, Choco Solver, různé řešiče SAT, ...). Jeho úkolem bude:
  1. Pokud půjde o nástroj neprobíraný podrobně na cvičeních (ale podobný těm probíraným), tak nastudovat tento nástroj (odlišnosti ve způsobu specifikace vstupního problému, formát výstupů apod. oproti nástrojům probíraným na cvičeních). V tomto případě bude zadaný problém jednodušší, aby se celková doba potřebná k vypracování projektu přibližně shodovala s řešením pomocí nástrojů používaným na cvičeních.
  2. Formalizovat slovní zadání, tedy identifikovat proměnné, zapsat omezení vhodným formálním způsobem.
  3. Vytvořit vstup pro přidělený nástroj (model pro Gecode, formuli ve správném formátu pro řešiče SAT,...), a s pomocí nástroje najít řešení.
  4. Vyzkoušet různé heuristiky, metody propagace omezení apod. poskytované nástrojem a porovnat nalezené výsledky při takto odlišných nastaveních.
  5. Interpretovat řešení - tedy převest nástrojem nalezené ohodnocení proměnných a podobné výstupy zpět do pojmů slovního zadání tak, aby tomu rozuměl člověk pohybující se v aplikační oblasti daného problému neznající teorii z oblasti constraint processing.
  6. Vypracovat písemnou zprávu o celém postupu řešení.
Problémy budou voleny z různých oblastí, může jít o řešení her a hlavolamů (např. různé speciální varianty Sudoku), hledání vhodného rozvrhu, plánování směn, hledání vadné součástky v logickém obvodu apod.