DPLL implemented with c++

First C++ code written... I think it's quite efficient with all the test set included in path data.

The simplest data set looks like:
-1 -3 0 -1 -5 0 -3 -5 0 -2 -4 0 -2 -6 0 -4 -6 0 1 2 0 3 4 0 5 6 0

used vector saving clauses and map saving assignments.
the main recursive function looks like following:
/*
1. If the set of clauses is empty, it returns true
2. Otherwise, if the set of clauses contains an empty clause, it returns false
3. Otherwise, if there is a unit clause, it applies unit propagation and then calls itself recursively
4. Otherwise, if there is a pure literal, it applies the pure literal rule and then calls itself recursively
5. Otherwise, it applies either the resolution rule or the splitting rule and calls itself recursively
*/

Git Repo: git@github.com:Wenling/DPLL-Algorithm.git
Google Drive: https://docs.google.com/file/d/0B0mZhauSOmW4dFZESVRtMGRpWms

DPLL Algorithm with ML

Git Repo: git@github.com:Wenling/DPLL-Algorithm.git
There are three satisfiability-preserving transformations in DP.
• The 1-literal rule
• The affirmative-negative rule
• The rule for eliminating atomic formulas
The first two steps reduce the total number of literals in the formula.
The last step reduces the number of variables in the formula.
By repeatedly applying these rules, eventually we obtain a formula containing an
empty clause, indicating unsatisfiability, or a formula with no clauses, indicating
satisfiability.


The DPLL algorithm replaces resolution with a splitting rule.
• Choose a propositional symbol p occuring in the formula.
• Let delta be the current set of clauses.
• Test the satisfiability of delta and {p}.
• If satisfiable, return true.
• Otherwise, return the result of testing delta and {¬p} for satisfiability.