460-4057/01 – Constraint Processing (ARUO)
Gurantor department | Department of Computer Science | Credits | 5 |
Subject guarantor | prof. RNDr. Petr Jančar, CSc. | Subject version guarantor | Ing. Martin Kot, Ph.D. |
Study level | undergraduate or graduate | Requirement | Optional |
Year | 1 | Semester | winter |
| | Study language | Czech |
Year of introduction | 2012/2013 | Year of cancellation | 2019/2020 |
Intended for the faculties | FEI | Intended for study types | Follow-up Master |
Subject aims expressed by acquired skills and competences
Student after successful completion of this subject:
- understands basic notions from the area "constraint processing"
- can classify practical problems from this area
- is able to find relevant unknowns for practical problem and precisely formulate corresponding constraints
- has an overview of general solution methods
- has an overview of available software tools for solving problems with constraints
- has some practice in solving practical problems using some of those tools
Teaching methods
Lectures
Tutorials
Project work
Summary
Many practical problems share the following feature - a desirable solution must
satisfy a lot of constraints resulting from reality (a timetable for teaching,
a schedule for working on something, an assignment of radio frequencies, ...).
In last several decades, an area called "constraint processing" has been developed,
where general forms of description of such constraints are examined and where
general methods for solving such problems are studied. Instances of these
methods are used successfully in many different areas, from molecular biology,
through computer graphics, natural language processing, to, for example, design
of logic circuits. The aim of this course is to introduce students to possible
forms of a description of constraints and some selected methods for finding
solutions satisfying these constraints, and to illustrate their use on some
practical problems. Students will also try to solve such problems in practice in
tutorials and in a semestral project, using freely available software libraries
and tools (as for example "SAT-solvers", i.e., solvers for satisfiability of
boolean formulas).
Compulsory literature:
Rina Dechter: Constraint Processing, Morgan Kaufmann, 2003
Recommended literature:
- Krzysztof Apt: Principles of Constraint Programming, Cambridge University
Press, 2003.
- Malik Ghallab, Dana Nau, Paolo Traverso: Automated Planning: Theory & Practice,
Morgan Kaufmann, 2004.
- Christos H. Papadimitriou, Kenneth Steiglitz: Combinatorial Optimization:
Algorithms and Complexity, Dover Publications, 1998.
- Alexander Schrijver: Combinatorial Optimization (3 volume, A,B, & C),
Springer, 2003.
- Daniel Kroening, Ofer Strichman: Decision Procedures: An Algorithmic Point of View,
Springer, 2008.
Way of continuous check of knowledge in the course of semester
Evaluation of a project and a written test.
E-learning
Other requirements
Additional requirements are placed on the student.
Prerequisities
Subject has no prerequisities.
Co-requisities
Subject has no co-requisities.
Subject syllabus:
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.
Conditions for subject completion
Occurrence in study plans
Occurrence in special blocks
Assessment of instruction