Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (10.12.2018)
Introduction to basic ideas and methods of applying mathematical logic to solving computational problems: SAT-
solving, constraint programming, automated theorem proving, formal verification. The course will also emphasize
gaining practical experience with selected software tools.
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (10.12.2018)
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.
Literature -
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (21.05.2021)
Handbook of Satisfiability (https://dl.acm.org/doi/book/10.5555/1550723)
Decision Procedures: An Algorithmic Point of View Book by Daniel Kroening and Ofer Strichman
The Calculus of Computation: Decision Procedures with Applications to Verification Textbook by Aaron R. Bradley and Zohar Manna
Handbook of Knowledge Representation: F. Van Harmelen, Vladimir Lifschitz, and Bruce Porter 2008 Elsevier
Handbook of Constraint Programming: F. Rossi, Peter Van Beek, and Toby Walsh 2006 Elsevier
Niklas Eén, Niklas Sörensson: An Extensible SAT-solver. SAT 2003: 502-518
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (21.05.2021)
Handbook of Satisfiability (https://dl.acm.org/doi/book/10.5555/1550723)
Decision Procedures: An Algorithmic Point of View Book by Daniel Kroening and Ofer Strichman
The Calculus of Computation: Decision Procedures with Applications to Verification Textbook by Aaron R. Bradley and Zohar Manna
Handbook of Knowledge Representation: F. Van Harmelen, Vladimir Lifschitz, and Bruce Porter 2008 Elsevier
Handbook of Constraint Programming: F. Rossi, Peter Van Beek, and Toby Walsh 2006 Elsevier
Niklas Eén, Niklas Sörensson: An Extensible SAT-solver. SAT 2003: 502-518
Requirements to the exam -
Last update: RNDr. Jakub Bulín, Ph.D. (19.11.2019)
Will be specified later.
Last update: RNDr. Jakub Bulín, Ph.D. (19.11.2019)
Požadavky budou upřesněny.
Syllabus -
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (21.05.2021)
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.
Last update: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (21.05.2021)
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.
