After completing this course, you will be able to:
- solve practical problems using modern tools such as SAT/SMT solvers
- understand algorithms underlying modern SAT and SMT solvers, such as resolution, CDCL and CDCL(T)
- use BDDs and their operations to analyze Boolean functions
- analyze predicate logic and equational reasoning using term rewriting
- connect SAT and SMT methods to problems from classical planning, term rewriting, model checking and probabilistic inference
|
|
Many problems, for example in verification of computer systems, planning and scheduling, can be expressed as proving that some big formula is always true. In this course we will concentrate on various methods for treating these kinds of problems. Not only correctness and completeness of these methods will be considered, but also efficiency and usability. In particular we will consider:
- Satisfiability of propositions: resolution and the main ingredients of modern satisfiability provers.
- Satisfiability modulo theories, in particular using linear inequalities, and the underlying simplex algorithm.
- Binary Decision Diagrams as efficient representation of boolean expressions and as the basis for solving planning and inference problems
- Unification; resolution on predicates.
- Reasoning modulo equations, term rewriting.
Instructional Modes
|
|
|
Basic knowledge of logic.
Basic programming skills.
|
|
Written examination plus practical assignment.
Both parts should be at least 5; for the final grade they both count for 50 %.
|
|
|