DPLL in C# - Satisfying problems in CNF

Time for another AI post! These last couple of weeks I've been working with two fellow C# guru's, Peter Thygesen and Thomas Gravgaard on an assignment in our AI class, on implementing a couple of specific parts of the DPLL algorithm, such as the methods for choosing split symbols, finding unit clauses and identifying pure symbols.
"What's DPLL good for?" I hear you cry...Well, it's simple really - or actually it isn't all that simple but I'll try to explain it anyway.Suppose you have a boolean statement in CNF (conjunctive normal form) and you want to test if it's satisfiable, that is - if a certain configuration exist, that will make it true - then you can run the DPLL algorithm to find out. The DPLL basically searches the solution space, but during the search uses the unit-clauses and pure symbols to prune the search space.In other words (and hopefully more understandable words) if you have a problem that you can formulate as a boolean problem (A and B or C implies D), then you can change that formulation into conjunctive normal form ((A or B or C) and (A or D or E) ... ) and when thats done you can determine if it's actually possible to assign values to the variables that will make this true.The way the algorithm works is basically to pick a symbol (=variable) and assign it true or false, and then for each options recursively call itself until all variables are assigned. In order to minimize the search space it uses a couple of simple rules to shortcut through this search, like finding out which clauses only contained one unassigned symbol. It's also very important in what order it assigns variables.
Another challenge in this assignment was that the code provided for the assignment that we should use as a basis for our work and for testing was all in java (typical university assignment). We're all C# people but too lazy to rewrite everything in C#, so luckily we got the java-code working in J# and were able to base our code on it anyway (and I wouldn't be surprised if our execution performance is higher that if we had used java).

Read our project here.