A problem and some (available, free) software tool will be assigned to each student. The task is to:
1. Learn how to work with the given tool. In the case, this tool is not one of those used during tutorials, it will take more time and the assigned problem will be simpler.
Formalize verbal assignment - it means to identify unknowns, specify constraints using proper formal methods.
Create input for the tool (model for Gecode, formula in appropriate form for SAT-solvers,....) and find solution using the tool.
Try different heuristics, constraint propagation methods etc. which are provided by the tool and compare results obtained using this different options of the tool
Interpret solution - using common language describe valuation of unknowns found by the tool.
Write down a text about the whole process of finding solution.
Problems will be chosen from different areas. It could be solution of games and puzzles (e.g. some variants of Sudoku), scheduling problems, finding defective components in logic circuit etc.
