Postgraduate Course: Propositional Methods (INFR11009)
|School||School of Informatics
||College||College of Science and Engineering
||Availability||Available to all students
|Credit level (Normal year taken)||SCQF Level 11 (Postgraduate)
|Home subject area||Informatics
||Other subject area||None
||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)
||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
|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.
|Written Examination 70|
Assessed Assignments 20
Oral Presentations 10
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.
* 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
* Propositional Planning
* Model Checking
Tools: theory and practice
* 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
* Model Checking by E. M. Clarke, Orna Grumberg, Doron Peled, MIT Press; ISBN: 0262032708; (January 7, 2000)
Timetabled Laboratories 0
Non-timetabled assessed assignments 36
Private Study/Other 44
|Course organiser||Dr Michael Rovatsos
Tel: (0131 6)51 3263
|Course secretary||Miss Gillian Bell
Tel: (0131 6)50 2692