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.