Part F: ===================================================================== Read the survey paper: The Quest for Efficient Satisfiability Solvers http://www.princeton.edu/~chaff/publication/cade_cav_2002.pdf The Quest for Efficient Boolean Satisfiability Solvers, by L. Zhang and S. Malik, Invited Paper, Proceedings of 8th International Conference on Computer Aided Deduction (CADE 2002) and also in Proceedings of 14th Conference on Computer Aided Verification (CAV2002), Copenhagen, Denmark, July 2002 The goal of the project is to implement a fast SAT solver in the time that you have available. Study the following SAT solvers, one in Java and the other in C++. http://www.sat4j.org/ http://www.sat4j.org/doc/ zchaff from Princeton University (you can also get chaff directly from Princeton) https://www.ccs.neu.edu/course/csg260/ssl/zchaff/ Let's start with a very modest improvement: Find 2 violations of the Law of Demeter in the two implementations. Turn in the violations with an explanation. Compare with: http://www.ccs.neu.edu/home/lieber/courses/csu670/f06/coupling-blog/690.aspx.htm Do you agree with the statement: Low Coupling Can Cause Unnecessary Complexity? Turn in your opinion. ==================