David Stanovský
//


MATHEMATICAL SOFTWARE 2017/18

Program:
Weeks 17: David Stanovský on computational logic tools
Weeks 814: Faruk Göloglu on Sage and cryptography
Computational logic:
 Boolean satisfaction, SATsolving
 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, SATsolving in practice (Minisat). 
viz resources about SAT below  
19.10.  Principles of SATsolving: clausification, the DPLL procedure. 
 HOMEWORK due on 2.11. 
26.10.  SATsolving in practice: real examples (knot coloring, RC4), hard cases (PHP, graphs with threshold density). 
 
2.11.  Principles of SMTsolving, 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:
