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 topicsrecommended 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: