Задачи разрешимости логических формул и приложения

Курс для студентов 1 курса магистратуры факультета Вычислительной математики и кибернетики Московского государственного университета им.Ломоносова

Name		Name	Last commit message	Last commit date
Latest commit History 71 Commits
01.introduction		01.introduction
02.Conflict-Driven Clause Learning algorithm		02.Conflict-Driven Clause Learning algorithm
03.DPLL		03.DPLL
04.equalities and uninterpreted functions		04.equalities and uninterpreted functions
05.linear theory and theory of bitvectors		05.linear theory and theory of bitvectors
06.array theory		06.array theory
07.pointers theory		07.pointers theory
08.quantified formulas		08.quantified formulas
09.combination of theories		09.combination of theories
10.program analysis		10.program analysis
11.symbolic execution		11.symbolic execution
12.binary decision diagrams		12.binary decision diagrams
13.bounded model checking		13.bounded model checking
solver		solver
.gitignore		.gitignore
README.md		README.md
decision-procedure.png		decision-procedure.png

Provide feedback