|
|
|
||
Poslední úprava: doc. Mgr. et Mgr. Jan Žemlička, Ph.D. (10.12.2018)
|
|
||
Poslední úprava: 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 |
|
||
Poslední úprava: RNDr. Jakub Bulín, Ph.D. (19.11.2019)
Požadavky budou upřesněny. |
|
||
Poslední úprava: 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. |