Use a smarter encoding in DPLL

ebhardjan commented 6 years ago

encode the cnf formulas as integer arrays and boolean arrays instead of using object structures -> should require a lot less space -> better spacial locality -> faster!

ebhardjan commented 6 years ago

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!

ebhardjan commented 6 years ago

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

ZiweiHuang94 commented 6 years ago

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.

limo1996 / SAT-Solver

Use a smarter encoding in DPLL #20