Postgraduate Course: Propositional Methods (INFR11009)
Course Outline
| School | School of Informatics |
College | College of Science and Engineering |
| Credit level (Normal year taken) | SCQF Level 11 (Postgraduate) |
Availability | Available to all students |
| SCQF Credits | 10 |
ECTS Credits | 5 |
| Summary | Satisfiability (SAT) was the first problem shown to be NP-complete and is both a cornerstone of computational complexity theory and commercially important since thousands of practical combinatorial problems would benefit from a highly efficient SAT solver.
This course will introduce modern methods and tools for representing and manipulating boolean formulae, in particular, Binary Decision Diagrams and probabilistic SAT solvers.
Students will develop facility in encoding a variety of problems in propositional form. |
| Course description |
Theory
* Propositional Logic, CNF, ROBDD
* Finite models
* SAT, NP completeness, and the phase transition
* Propositional encodings of combinatorial problems.
* Propositional encodings of graph-theoretic problems.
* Quantified Boolean Formulae
* Modal Logic
Applications,
* Propositional Planning
* Model Checking
Tools: theory and practice
* PropSat
* PropPlan
* BDD packages
* SAT solvers (deterministic and non-deterministic)
Relevant QAA Computing Curriculum Sections: Artificial Intelligence, Compilers and Syntax Directed Tools, Data Structures and Algorithms, Systems Analysis and Design
|
Entry Requirements (not applicable to Visiting Students)
| Pre-requisites |
|
Co-requisites | |
| Prohibited Combinations | |
Other requirements | For Informatics PG and final year MInf students only, or by special permission of the School. Students are expected to have familiarity with basic Boolean Logic and some acquaintance with SML. |
Information for Visiting Students
| Pre-requisites | None |
Course Delivery Information
| Not being delivered |
Learning Outcomes
1 - Students will be able to apply BDD and SAT technologies in a variety of applications.
2 - They will be able to find potential for practical applications of reductions more commonly seen in proofs of complexity results, and apply abstract methods to practical applications.
3 - Students will be able to solve problems by bringing together a variety of software tools and components.
4 - Students will have read, presented and discussed papers from the current literature.
5 - They will have completed an extended practical project and produce a written report.
|
Reading List
* http://cs-svr1.swan.ac.uk/~csoliver/SATlinks.html
* http://pvs.csl.sri.com/tutorials.html
* http://www-2.cs.cmu.edu/~modelcheck/tour.html
* http://www.ee.pdx.edu/~alanmi/research/dd/bddLinks.htm
* Model Checking by E. M. Clarke, Orna Grumberg, Doron Peled, MIT Press; ISBN: 0262032708; (January 7, 2000) |
Contacts
| Course organiser | Dr Michael Rovatsos
Tel: (0131 6)51 3263
Email: mrovatso@inf.ed.ac.uk |
Course secretary | Miss Gillian Bell
Tel: (0131 6)50 2692
Email: Gillian.Bell@ed.ac.uk |
|
|
University Homepage