I will use moodle to organize the course this year. Please sign up to the moodle course for further information.

Index

1. Credit requirements
2. Syllabus
3. Contents of the lecture
4. Contents of the practical

Basic information

• Teacher: Petr Kučera <> , místnost S304
• Schedule of the lecture: Wednesday 14:00 - 15:30 (S8)
• Schedule of the practical: Thursday 12:20 - 13:50 (S8)
• Subject information in SIS
• The course in Moodle
• You can at the last year lecture (given by me) and the previous version of the lecture given by Martin Blicha.
• If you are interested in thesis in the area covered by the lecture, you can contact me (see also my page to thesis, there is not much, concrete topic would be the result of a discussion with you).
• The programming tasks

Credit requirements

To get the credit, you need to get enough points from the homework. The points can be obtained in two ways.

1. Solving programming tasks and
2. Solving homework exercises to the practicals.
   • The theoretical homework assignments can be found at the course page in Moodle

To get the credit, you need to satisfy one of the following limits.

1. Have at least 40 points from the programming tasks
2. Have at least 50% of the points from the homework exercises to the practical.
   • The precise number of the points needed from the homework exercises in this case will be specified at the end of the semester as it depends on the number of practicals and point total of the homework exercises.

Note that there are no deadlines for neither the theoretical homework assignments, nor for programming tasks. However, I have made a suggestion of soft deadlines on the moodle page, please check it out. I do not think it is a good idea to leave all homework until summer holiday or even September.

Exam

There are two ways of passing the exam.

1. The first option is to pass a standard oral exam. Depending on the current situation, it is also possible to pass the oral exam remotely.
2. The second option is to solve the homework exercises and get more points than for the credit. In particular:
   • You have to get at least one half (50%) of total number of points of the theoretical homework (attached to each practical). I will specify the exact number of points at the end of the semester.
   • In addition you have to get 40 points for the programming tasks. Moreover, you are required to have a complete solver in the end (either CDCL or look-ahead up to your taste).
   The points count towards both the credit and exam in this case (i.e. each single point counts towards both the credit and the exam). Passing the exam in this way gives grade 1.

Syllabus

1. Introduction, motivation, basic notions. Normal forms: CNF, DNF, NNF
2. The problem of satisfiability of a propositional formula - SAT. Effective methods used in modern SAT solvers. Local search SAT solving algorithms
3. Satisfiability modulo theory - SMT
4. Representations of boolean functions with BDDs.
5. Satisfiability of quantified boolean formulas: QBF
6. Decision procedures for theories of first order logic
   • logic with equality
   • theory of equality and uninterpreted functions
   • theory of linear arithmetic
   • theory of arrays and pointers
   • theory of bit vectors
7. Combining logic theories