5/07/2012

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

No comments:

Post a Comment