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:

- A review of classical Propositional Logic and SAT. Propositional representations of First-Order Logic.
- A catalogue of applications of propositional representations to a variety of computational problems (combinatorial problems, AI planning, model checking, semantic representation).Practical experience with tools embodying these techniques.
- An introduction to the classical theory and algorithms underlying general-purpose tools for manipulating propositional representations (DPLL SAT solvers and BDD packages).
- An introduction to probabilistic inference in propositional reasoning: Markov Random Fields, Gibbs sampling, Survey Propagation, Markov Logic Networks.

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

**Wednesday 7 January**(Fourman) Background on complexity and satisfiability. Reduction.

SAT background reading. See University of Exeter notes http://www.dcs.ex.ac.uk/studtRes/COM3412/Cook.pdf**Friday 9 January**(Nazarov) Tool demonstrations: PropSat and PropPlan Finite Domain Definition Language Sample Domains**Wednesday 14 January**(Fourman) Basic definitions (pp.1-8) and example reductions (pp. 72-82) Roberto Sebastiani's slides. Flip chart intro to QBF and PropPlan encoding of strips actions.**Friday 16 January**(Fourman) Reduction to CNF (Sebastiani pp.9-15); intro to ML.**Wednesday 21 January**(Fourman) Basic SAT Techniques (Sebastiani pp.25-39)**Friday 23 January**(Nazarov) Standard ML**Wednesday 28 January**(Fourman) The phase transition (Sebastiani pp.16-24) More on BDDs Bryant 1992**Friday 30 January**High-level ML interface to BDD package**Wednesday 4 February**(Fourman) PDDL - Planning Domain Definition Language - and translation to BDD**Friday 6 February**(Fourman) Labelling CNF conversion (see Sebastiani CADE 04 slides, pp. 25-28). Efficient expansion of numeric quantifiers.**Wednesday 11 February**(Fourman) More on CNF conversions.**Friday 13 February**(Fourman) Modelling finite state machines.**Wednesday 18 February**(Fourman) Temporal modal operators and fixed points**Friday 20 February**No Lecture**Wednesday 25 February**Student presentations: Herding, Rachels**Wiebke Herding**

Bounded Model Checking Using Satisfiability Solving (2001) Edmund Clarke, Armin Biere, Richard Raimi, Yunshan ZhuModel 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 MarraroThis 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.

**Friday 27 February**Student presentations: Lechler, Ruiz**Ivan Meza-Ruiz**

Towards the Use of Automated Reasoning in Discourse Disambiguation (2001) Claire Gardent, Bonnie Webber**Wednesday 4 March**Fourman. Time and Space experiments for BDD package.**Friday 6 March**Fourman. NuSMV Dining Philosophers- Wednesday 11 March Fourman. Linear and branching time logics (LTL, CTL, CTL*) Revision BDDs and CTL
**Friday 13 March**Fourman. Solution to dining philosophers. Revision SAT and LTL.

- Assignment 1: Reduction to CNF - a
first exercise in ML

Issued 19 January; Handin 28 January - Assignment 2 (part a): Finding the
phase transition (BDD)

Issued 28 January Updated 00:12 Saturday 31 January; Handin February 6th - Assignment 2 (part b): Finding the
phase transition (SAT)

Issued 3 March ; Handin March 14.

- 8 Jan Background on SAT http://www.dcs.ex.ac.uk/studtRes/COM3412/Cook.pdf
- 10 Jan Intro to BDDs Bryant 1992
- 15 Jan ML tutorial
- 17 Jan Conversion to CNF See pp. 1-14 of Roberto Sebastiani's slides
- 22 Jan Postponed
- 24 Jan CNF conversion in ML. Phase transition: pp14-24 of Roberto Sebastiani's slides
- 29 Jan SAT Techniques pp25-39 of Roberto Sebastiani's slides
- 31 Jan ML BDD package C interface ML interface
- 4 Feb Finite Domain Definition Language Sample Domains
- 7 Feb High-level ML interface to BDD package

`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 |