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

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

Binary Decision Diagrams/SAT Phase Transition

Binary Decision Diagrams

Bryant '92

Sebastiani CADE 04 Slides pp. 53-58

Phase Transition

Sebastiani CADE 04 Slides pp. 29-37

CNF: Davis Putnam and variations

Sebastiani CADE 04 Slides pp. 25 - 28, 38 -52
Propsat Demonstration

Propositional Logic Review

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.

First Lecture Today!

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.