Lectures:
1. Examples of practical problems with constraints and outline of general solving methods.
Exact formulation of problems, illustrated on example of an assignment of radio frequencies; choice of unknowns and constraints on them
2. Structure of space of potential solutions
Constraint propagation methods.
3. General search strategies for the space of potential solutions.
4. Scheduling problem (lessons, work shifts,...).
Application of selected methods.
5. Formulation of logical circuits diagnosis problem and some other problems
that can be reduced to SAT (satisfiability of boolean formulas)
SAT-solvers.
6. Methods used in SAT-solvers.
7. Stochastic search strategies.
8. Combinatorial optimization.
Multicommodity flows, logistic problems.
9. Integer linear constraints and specific solution methods.
10. Planning (assigning tasks to processors).
11. Outline of some advanced topics (decomposition methods, probabilistic networks,...).
12. Hybrid methods.
13. Summary, review
-----------------------------
Outline of computer tutorials:
------------------------------
Tutorials usually consist of two parts:
- with a chalk and a blackboard (B) - 30-45 minutes,
discussion and practice of methods from lectures on different examples,
and possibly finishing of solutions of practical examples from lectures
- with computers (C) - 45-60 minutes, a work with available tools, in which
discussed method are implemented, possibly own implementation of simpler
tools using available libraries (e.g., Sat4j)
1. B: Precise formulation of problems
C: Introductory session with Gecode tool (constraint solver)
2. B: Constraint propagation
C: Gecode - construction of a model of a problem
3. B: Search of solution space
C: Gecode - the use of different search methods implemented in this tool
4. B: Scheduling problems
C: Software solution of a scheduling problem
5. B: Formulation of a problem in a form of an input for a SAT solver
C: Introductory session with MiniSAT - a simple SAT solver
6. B: Methods for solving SAT
C: Solution of practical problems with MiniSAT
7. B: Stochastic search methods
C: UBCSAT - stochastic SAT solver
8. B: Logistic problems, multicommodity flows
C: The use of JAVA library Sat4j for SAT solving in own programs
9. B: Solving of integer linear programing problems
C: Sat4j as a standalone SAT solver, other available SAT solvers, their
commonalities and differences
10. B: Planning problems
C: Solving of integer linear programming problems with software tools
11. B: Problem decomposition, probabilistic networks
C: Consultation of projects
12. B: The use of methods combining a search with a constraint propagation
C: Consultation of projects
13. A written test
Projects:
-------------------------------------------------
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.
2. Formalize verbal assignment - it means to identify unknowns, specify constraints using proper formal methods.
3. Create input for the tool (model for Gecode, formula in appropriate form for SAT-solvers,....) and find solution using the tool.
4. Try different heuristics, constraint propagation methods etc. which are provided by the tool and compare results obtained using this different options of the tool
5. Interpret solution - using common language describe valuation of unknowns found by the tool.
6. 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.
1. Examples of practical problems with constraints and outline of general solving methods.
Exact formulation of problems, illustrated on example of an assignment of radio frequencies; choice of unknowns and constraints on them
2. Structure of space of potential solutions
Constraint propagation methods.
3. General search strategies for the space of potential solutions.
4. Scheduling problem (lessons, work shifts,...).
Application of selected methods.
5. Formulation of logical circuits diagnosis problem and some other problems
that can be reduced to SAT (satisfiability of boolean formulas)
SAT-solvers.
6. Methods used in SAT-solvers.
7. Stochastic search strategies.
8. Combinatorial optimization.
Multicommodity flows, logistic problems.
9. Integer linear constraints and specific solution methods.
10. Planning (assigning tasks to processors).
11. Outline of some advanced topics (decomposition methods, probabilistic networks,...).
12. Hybrid methods.
13. Summary, review
-----------------------------
Outline of computer tutorials:
------------------------------
Tutorials usually consist of two parts:
- with a chalk and a blackboard (B) - 30-45 minutes,
discussion and practice of methods from lectures on different examples,
and possibly finishing of solutions of practical examples from lectures
- with computers (C) - 45-60 minutes, a work with available tools, in which
discussed method are implemented, possibly own implementation of simpler
tools using available libraries (e.g., Sat4j)
1. B: Precise formulation of problems
C: Introductory session with Gecode tool (constraint solver)
2. B: Constraint propagation
C: Gecode - construction of a model of a problem
3. B: Search of solution space
C: Gecode - the use of different search methods implemented in this tool
4. B: Scheduling problems
C: Software solution of a scheduling problem
5. B: Formulation of a problem in a form of an input for a SAT solver
C: Introductory session with MiniSAT - a simple SAT solver
6. B: Methods for solving SAT
C: Solution of practical problems with MiniSAT
7. B: Stochastic search methods
C: UBCSAT - stochastic SAT solver
8. B: Logistic problems, multicommodity flows
C: The use of JAVA library Sat4j for SAT solving in own programs
9. B: Solving of integer linear programing problems
C: Sat4j as a standalone SAT solver, other available SAT solvers, their
commonalities and differences
10. B: Planning problems
C: Solving of integer linear programming problems with software tools
11. B: Problem decomposition, probabilistic networks
C: Consultation of projects
12. B: The use of methods combining a search with a constraint propagation
C: Consultation of projects
13. A written test
Projects:
-------------------------------------------------
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.
2. Formalize verbal assignment - it means to identify unknowns, specify constraints using proper formal methods.
3. Create input for the tool (model for Gecode, formula in appropriate form for SAT-solvers,....) and find solution using the tool.
4. Try different heuristics, constraint propagation methods etc. which are provided by the tool and compare results obtained using this different options of the tool
5. Interpret solution - using common language describe valuation of unknowns found by the tool.
6. 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.