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 DescriptorThis course comes in four parts:
The Lecture Log for this course has an Atom Feed - to which you can subscribe so you can easily see when it is updated.
Wiebke Herding
Bounded
Model Checking Using Satisfiability Solving (2001) Edmund Clarke, Armin
Biere, Richard Raimi, Yunshan Zhu
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.
Justin Rachels
Logical
Cryptanalysis as a SAT Problem: the Encoding of the Data Encryption
Standard (1999) Fabio Massacci, Laura Marraro
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.
Ivan Meza-Ruiz
Towards
the Use of Automated Reasoning in Discourse Disambiguation (2001) Claire
Gardent, Bonnie Webber
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: 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 |