Use a smarter encoding in DPLL about sat-solver HOT 3 CLOSED

This is not worth it!
Right now problems that take more than a second to solve fit nicely into cache!
For instance 35 variables, 200 clauses, 3 variables per clause:

• for the CNF object -> set of 200 clauses: 200*8 = 1.6 kB
• for the 200 clause objects -> each a set of 3 variables: 200*3*8 = 4.8 kB
• for each variable object -> 3 bools and 1 unsigned int: 200*3*(1+4) = 3 kB
  Total: 9.4 kB

Considering that even my 4 year old laptop has 128 kB of Level 1 cache, decreasing the size of the internal representation by about a factor of two is just not worth it.
The problem is the amount of computation that we do on the CNF objects...

I've added some improvements to the DPLL algorithm (pull request #22).
To improve the performance further we need a better algorithm -> CDCL!

from sat-solver.

@limo1996 and @ZiweiHuang94: let me know what you think

from sat-solver.

Really appreciate the improvement you did! Regarding further improving the performance (Try CDCL), I am not sure how much time is assumed to achieve it. Because we still need some time for the report and final presentation. I suppose performance analysis is also an important part.

from sat-solver.