Propositional Methods 2005

Lectures

Appleton Tower, Level 3, Room 3.03
Tuesday 10:00—10:50am, Friday 10:00—10:50am

Lecturer Michael Fourman
We plan to have around 15 meetings in total; the propm calendar (.ics  html) will be updated to provide information on exceptions to the regular schedule. Subscribe to it using any ical-aware calendar application (eg Mozilla Sunbird, Mozilla Calendar (in Firefox), Apple ical, etc.)

Synopsis

The satisfiability problem, SAT, is NP complete (Cook's Theorem). Nevertheless, modern SAT solvers routinely solve many large, naturally occurring, satisfiability problems. It turns out that for many combinatorial problems a well-crafted reduction to SAT, followed by application of a general-purpose SAT solver, provides an algorithm that performs surprisingly (even unreasonably) well on naturally ocurring problem instances.

More generally, propositional logic provides encodings for many computational problems. Applying general-purpose tools to manipulate such propositional representations often provides algorithms that turn out, in practice, to be competetive with hand-crafted heuristic and problem-specific approaches.

Clausal representations of SAT can be viewed as Markov Random Fields, with satisfying valuations corresponding to zero-energy states. This observation leads to new algorithms for SAT-solving, based on physical intuitions. On some classes of problem these algorithms provide astounding improvements on earlier techniques.

The link with MRF also provides a natural way to link classical boolean reasoning with probabilistic inference. MRF techniques lead to Markov Logic Networks, which provide a first-order setting for probabilistic inference.

Course Descriptor

This course comes in four parts:


References

Lecture Plan/Log

The Lecture Log for this course has an Atom Feed - to which you can subscribe so you can easily see when it is updated.


2004 Lecture Log

Assignments 2005


Resources

Slides and papers from CMU (Ed Clarke)

ML tutorial

Papers

Tools

PropPlan site updated 4 February 2004

Survey Propagation



NuSMV user manual

2002 Lecture Log


Version 1.15 by MichaelFourman
Last modified 2006/05/12 03:13:55


Home : Teaching : Courses 

Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: school-office@inf.ed.ac.uk
Please contact our webadmin with any comments or corrections. Logging and Cookies
Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh