Propositional Methods (P00872)

? Credit Points : 10 ? SCQF Level : 11 ? Acronym : INF-P-PROPM

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

? Pre-requisites : For Informatics PG students only, or by special permission of the School. Students are expected to have familiarity with basic Boolean Logic and some acquaintance with SML.

Subject Areas

Home subject area

Knowledge Representation and Reasoning, (School of Informatics, Schedule O)

Other subject areas

Theoretical Computer Science, (School of Informatics, Schedule O)

Delivery Information

? Normal year taken : Postgraduate

? Delivery Period : Not being delivered

? Contact Teaching Time : 3 hour(s) per week for 10 weeks

Summary of Intended Learning Outcomes

Students will be able to apply BDD and SAT technologies in a variety of applications.
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.

Students will be able to solve problems by bringing together a variety of software tools and components.

Students will have read, presented and discussed papers from the current literature.
They will have completed an extended practical project and produce a written report.