David Stanovský
//
|
|
MATHEMATICAL SOFTWARE 2017/18
|
Program:
Weeks 1-7: David Stanovský on computational logic tools
Weeks 8-14: Faruk Göloglu on Sage and cryptography
Computational logic:
- Boolean satisfaction, SAT-solving
- Satisfaction modulo theories
- Automated thorem proving in first order logic
Preparation for the second part (Deadline: mid November): Learn basics of Python!!!
| covered topics | recommended reading | homework |
5.10. | Boolean satisfaction. Translating problems to SAT. |
Knights and Knaves | |
12.10. | Translating problems to SAT, SAT-solving in practice (Minisat). |
viz resources about SAT below | |
19.10. | Principles of SAT-solving: clausification, the DPLL procedure. |
| HOMEWORK due on 2.11. |
26.10. | SAT-solving in practice: real examples (knot coloring, RC4), hard cases (PHP, graphs with threshold density). |
| |
2.11. | Principles of SMT-solving, translating problems to SMT. |
Oliveras's slides | |
9.11. | Lecture will be cancelled, come to the fall school of algebra! (Or, learn Python!) |
| |
16.11. | Automated theorem proving in first order logic. |
| |
23.11. | Constraint modeling with MiniZinc (by Jakub Bulín). |
slides, files |
HOMEWORK due on 31.1.
text, input files
|
30.11. | Faruk Gologlu takes over and teaches Sage. |
| |
Resources about SAT:
Resources about SMT:
Resources about First order ATP:
Resources about CSP solving:
Resources about Sage:
|