Boolean satisfiability problems and their applications

📝 Description:

A course for 1st year Master's students of the Faculty of Computational Mathematics and Cybernetics of Lomonosov Moscow State University.

🖇 Links:

• 🎥 Video lectures
• 🔗 Course GitHub by Roman Kholin
• 👨🏼‍🏫 Lecturer: Roman Kholin

📚 Lecture topics:

1. Intro to course. SAT and UNSAT
2. Representation of the problem for solvers.
3. Representation of the problem for solvers. Intro to SMT.
4. Intro to SMT.
5. Algorithm Conflict-Driven Clause Learning (CDCL).
6. CDCL optimizations.
7. The Davis–Putnam–Logemann–Loveland algorithm (Theory). Equality logic and non-interpreted functions.
8. Equality logic and non-interpreted functions.
9. Array logic.
10. Combining logic.
11. Symbolic execution.
12. Program analysis.
13. Application in biology.

🏡 Homework assignments:

1. Homework 1. CNF, AtMostTwo, SAT-solver
2. Homework 2. colorA, colorB, DIMACS, n-Sudoku, SMT-solver
3. Homework 3. Engine for symbolic execution of C-code

🙀 Examination test:

• List of questions
• Answers to questions