The Satisfiability problem (SAT) of deciding whether a given boolean formula allows a {true,false}-assignment to variables so that the formula evaluates to true, is known to be NP-complete. However, there are several ways to tackle this problem resulting in algorithms with exponential running time. In this thesis we are interested in implementing such algorithms as presented in the lecture "Satisfiability of Boolean Formulas - Combinatorics and Algorithms", and illustrating them in a vivid way.
The visualization of the algorithms' operations could be step by step in an adequate framework. Besides the graphical representation there is the possibility to test the algorithms' performance on some generated instances. Based on the so obtained results, it would be interesting to optimize the procedures for speeding up the practical running times.
Goal: The goal of this thesis is to implement algorithms for solving Satisfiability, visualize their execution and test their performance.
Prerequisites: Some programming skills in Java (or similar language) and interest in graphical representations. The attendance of the SAT-course is not required.
Contact Persons:
Philipp Zumstein,
zuphilip@inf.ethz.ch, CAB G 17, Tel: (044) 632-7318.
Andreas Razen,
arazen@inf.ethz.ch, CAB G 37.1, Tel: (044) 632-7422.