Sylabus
Decision problems in propositional logic (Boolean Satisfiability, SAT). Examples of modeling using propositional logic.
Algorithms for SAT. Decision problems in first-order logic.
The Satisfiability Modulo Theories (SMT) problem. Problem encodings for SAT.
Algorithms for SMT. Constraint Programming (CP): algorithms and modeling examples.
Encodings for propositional logic. Answer Set Programming (ASP): algorithms and modeling examples.
Relationship with propositional logic. Function and enumeration problems for SAT, SMT, ASP and CP: including optimization problems and over specified sets of constraints.
Decision, function and enumeration problems with quantified propositional variables. Application examples.
Anotace
Seznámení se základními myšlenkami a metodami využití matematické logiky k řešení výpočetních problémů: SAT-solving, constraint programming, automatické dokazování, formální verifikace. Důraz bude kladen také na získání praktické zkušenosti s vybranými softwarovými nástroji.