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 : PGs only or with permission of Director of Teaching. Familiarity with basic Boolean Logic. Some acquaintance with SML would be helpful.

Subject Areas

Home subject area

Artificial Intelligence, (School of Informatics, Schedule O)

Delivery Information

? Normal year taken : Postgraduate

? Delivery Period : Semester 2 (Blocks 3-4)

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

First Class Information

Date	Start	End	Room	Area	Additional Information
10/01/2006	10:00	11:00			Appleton Tower, Room 5.01

All of the following classes

Type	Day	Start	End	Area
Lecture	Tuesday	10:00	10:50	Central
Lecture	Friday	10:00	10:50	Central

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.