THE UNIVERSITY of EDINBURGH

DEGREE REGULATIONS & PROGRAMMES OF STUDY 2011/2012
- ARCHIVE for reference only
THIS PAGE IS OUT OF DATE

University Homepage
DRPS Homepage
DRPS Search
DRPS Contact
DRPS : Course Catalogue : School of Informatics : Informatics

Postgraduate Course: Propositional Methods (INFR11009)

Course Outline
SchoolSchool of Informatics CollegeCollege of Science and Engineering
Course typeStandard AvailabilityAvailable to all students
Credit level (Normal year taken)SCQF Level 11 (Postgraduate) Credits10
Home subject areaInformatics Other subject areaNone
Course website http://www.inf.ed.ac.uk/teaching/courses/propm Taught in Gaelic?No
Course descriptionSatisfiability (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-requisitesNone
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
KeywordsNot entered
Contacts
Course organiserDr Michael Rovatsos
Tel: (0131 6)51 3263
Email: mrovatso@inf.ed.ac.uk
Course secretaryMiss Gillian Bell
Tel: (0131 6)50 2692
Email: Gillian.Watt@ed.ac.uk
Navigation
Help & Information
Home
Introduction
Glossary
Search DPTs and Courses
Regulations
Regulations
Degree Programmes
Introduction
Browse DPTs
Courses
Introduction
Humanities and Social Science
Science and Engineering
Medicine and Veterinary Medicine
Other Information
Timetab
Prospectuses
Important Information
 
© Copyright 2011 The University of Edinburgh - 16 January 2012 6:17 am