Syllabus
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.
Annotation
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.