Conclusion

You shall compare the running times with and without the two-watched literals data structure. As I mentioned, the I did not put much attention on the code efficiency, you can easily speed up the running time a lot by refactoring the codes.

Further, incorporating a branching heuristic and restart heuristic can significantly improve the running speed on large CNF instances. Fortunately, all of them are not as complex and hard-to-debug as a [two-watched literals CDCL solver] alone.