Assignment #3

Theme: boolean evaluation, broadword computation.

Assigned: Oct. 13, 2015.

Due: Oct. 27, 2015. Reminder: homework should be in LaTeX (or TeX). Due at the beginning of class on the due date.

• Use one of Knuth's SAT solvers to determine the value of the van der Waerden number $W(4,4)$ (from the table on page 5 of 7.2.2.2 on Satisfiability). Explain how you determined the value, showing the output from the solver.

• Find a circuit for addition mod 3 like that in exercise 60 of section 7.1.2 (pg. 129), except use 11 to encode 2 instead of 10. Your cicuit should use the same number of gates as the one in Knuth's solution. Explain why it is correct; e.g., by using truth tables.

• Look up the IEEE 754 floating point standard, particularly the representation of 64 bit floating point numbers. Your computer undoubtedly implements this standard. write a C program that extracts the exponent from such numbers in order to compute $\rho x$. This is somewhat like implementing equation (55) on page 142, but in C instead of MMIX, and with $\rho x$ instead of $\lambda x$. Test your program by showing its output on the numbers $x = 2^{20}+1,2^{20}+2, \ldots, 2^{20}+2^5$. Turn in your program source and output (text files are ok here).

• Prove that \[ \nu x\ =\ x - \left\lfloor \frac{x}{2} \right\rfloor - \left\lfloor \frac{x}{4} \right\rfloor - \left\lfloor \frac{x}{8} \right\rfloor - \cdots \]

• Start thinking about a suitable project. Turn in a one paragraph description of a potential project.