Friday, January 28, 2005

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

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

Tuesday, January 25, 2005

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

Friday, January 21, 2005

CNF: Davis Putnam and variations

Friday, January 14, 2005

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.