Michael Fourman >> teaching

Spring term 2004 Propositional Methods Honours/MSc
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.
Spring term 1994 An Introduction to Algorithms and Datastructures in ML Final Honours, University of Western Australia, Perth, WA

Please contact me if you are interested in any of these - more details to follow soon