Postgraduate Course: Propositional Methods (INFR11009)
Course Outline
| School | School of Informatics |
College | College of Science and Engineering |
| Course type | Standard |
Availability | Available to all students |
| Credit level (Normal year taken) | SCQF Level 11 (Postgraduate) |
Credits | 10 |
| Home subject area | Informatics |
Other subject area | None |
| Course website |
http://www.inf.ed.ac.uk/teaching/courses/propm |
Taught in Gaelic? | No |
| Course description | 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. |
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. |
| Additional Costs | None |
Information for Visiting Students
| Pre-requisites | None |
| Displayed in Visiting Students Prospectus? | No |
Course Delivery Information
| Not being delivered |
Summary of Intended 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. |
Assessment Information
Written Examination 70
Assessed Assignments 20
Oral Presentations 10
Assessment
In the first four weeks ot the source, students will carry out routine assignments designed to familiarise them with current tools.
They will then undertake a four-week assignment requiring them to encode a family of combinatorial problems in propositional form and investigate the effectiveness of SAT- or BDD- based methods in solving problems from this family.
If delivered in semester 1, this course will have an option for semester 1 only visiting undergraduate students, providing assessment prior to the end of the calendar year. |
Special Arrangements
| None |
Additional Information
| Academic description |
Not entered |
| Syllabus |
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 |
| Transferable skills |
Not entered |
| 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) |
| Study Abroad |
Not entered |
| Study Pattern |
Lectures 15
Tutorials 5
Timetabled Laboratories 0
Non-timetabled assessed assignments 36
Private Study/Other 44
Total 100 |
| Keywords | Not entered |
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.Watt@ed.ac.uk |
|
|
University Homepage