### k-SAT => 3-SAT; intro to ML

Exercise 1 is available online, as are the ML examples.

Course Lecture Log, MSc Informatics, The University of Edinburgh, Spring 2005.

- Binary Decision Diagrams
- Bryant '92
- Sebastiani CADE 04 Slides pp. 53-58
- Phase Transition
- Sebastiani CADE 04 Slides pp. 29-37

Topics Covered (Sebastiani CADE 04 Slides pp. 8-24)

- Boolean Propositional Logic
- Connectives, Valuations, Truth Tables
- Trees and DAGs
- Best-case exponential saving in space and time.
- Normal Forms
- Negative Normal Form
- expand implications; push negations down using de Morgan and double negation
- Conjunctive Normal Form
- Distribute \/ over /\, top-down. Worst-case exponential.

Apologies for the timetabling confusion yesterday. We meet regularly on Tuesdays and Fridays 10am room 5.01 Appleton Tower.
Today I will review propositional and first-order logic, and demonstrate propsat, an online tool that uses a propositional representation to model and reason about first-order theories over finite domains.
Comments on this blog are welcome from both students and kibbitzers on the www.