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.)
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:
Model Checking is used to determine whether a transition system obeys a specification of its intended behaviour. This can be done in a highly automatic manner, but due to the state explosion only with rather small problems. Much research has been focussed on finding more efficient solutions to model checking problems. Clarke and Biere have successfully used recent SAT solvers for model checking. In this presentation, I'd like to demonstrate their conversion of model checking problems to satisfiability and discuss pros and cons of this technology.
This paper introduces the concept of logical cryptanalysis, the formulation of encryption-based functional relationships using formal (predicate) logic. After a brief introduction to cryptography and established cryptographic methods, I will discuss the general method by which logical cryptanalytic functions take form and then present a detail-based case study of using logical cryptanalysis to break commercial-level (56-bit) DES cyphers.
Mueller, Erik T. (2003). Story understanding through multi-representation model construction. In Graeme Hirst & Sergei Nirenburg (Eds.), Text Meaning: Proceedings of the HLT-NAACL 2003 Workshop (pp. 46-53). East Stroudsburg, PA: Association for Computational Linguistics.
Version 1.15 by MichaelFourman
Last modified 2006/05/12 03:13:55
Informatics Forum, 10 Crichton Street, Edinburgh, EH8 9AB, Scotland, UK
Tel: +44 131 651 5661, Fax: +44 131 651 1426, E-mail: firstname.lastname@example.org
Please contact our webadmin with any comments or corrections. Logging and Cookies
Unless explicitly stated otherwise, all material is copyright © The University of Edinburgh