# FI:IA085 SAT and Automated Reasoning - Course Information

## IA085 Satisfiability and Automated Reasoning

**Faculty of Informatics**

Spring 2024

**Extent and Intensity**- 2/1/1. 4 credit(s) (plus extra credits for completion). Type of Completion: zk (examination).

Taught in person. **Teacher(s)**- RNDr. Martin Jonáš, Ph.D. (lecturer)

Bc. Jakub Šárník (seminar tutor) **Guaranteed by**- RNDr. Martin Jonáš, Ph.D.

Department of Computer Science – Faculty of Informatics

Supplier department: Department of Computer Science – Faculty of Informatics **Timetable**- Wed 16:00–17:50 A217
- Timetable of Seminar Groups:

*J. Šárník* **Course Enrolment Limitations**- The course is offered to students of any study field.
**Course objectives**- At the end of the course, students should:

- have working knowledge of propositional logic and first-order logic,

- be able to express real-world problems in a suitable logical formalism,

- be able to explain principles, algorithms, and underlying theoretical concepts of modern satisfiability solvers and theorem provers,

- be able to assess what kind of tool is relevant for their problem and apply an existing satisfiability solver or theorem prover to the problem,

- understand strengths and weaknesses of existing satisfiability solvers and theorem provers. **Learning outcomes**- At the end of the course, students should:

- have working knowledge of propositional logic and first-order logic,

- be able to express real-world problems in a suitable logical formalism,

- be able to explain principles, algorithms, and underlying theoretical concepts of modern satisfiability solvers and theorem provers,

- be able to assess what kind of tool is relevant for their problem and apply an existing satisfiability solver or theorem prover to the problem,

- understand strengths and weaknesses of existing satisfiability solvers and theorem provers. **Syllabus**- Propositional satisfiability: syntax and semantics of propositional logic , encoding of real-world problems, historical and modern satisfiability decision procedures, design and usage of modern satisfiability solvers, preprocessing techniques, proofs of unsatisfiability.
- Satisfiability Modulo Theories: syntax and semantics of first-order logic without quantifiers; first-order theories relevant for description of systems, their decidability and complexity; CDCL(T) algorithm and theory solvers for selected first-order theories.
- Reasoning with Quantifiers: syntax and semantics of first-order logic with quantifiers; encoding of real-world problems; first-order resolution, superposition, E-matching; implementation of proof search in modern theorem provers; quantifier elimination; quantifier instantiation.
- Interactive Theorem Proving: formal foundations; practical usage of a state-of-the art theorem prover.

**Literature***Handbook of satisfiability*. Edited by Armin Biere. Amsterdam: IOS Press, 2009, xiii, 966. ISBN 9781586039295. info

**Teaching methods**- Lectures, homework.
**Assessment methods**- Homework, final written exam.
**Language of instruction**- English
**Further Comments**- Study Materials

The course is taught annually.

- Enrolment Statistics (recent)

- Permalink: https://is.muni.cz/course/fi/spring2024/IA085