This is the real meat of the solver. Here the CNF is assembled. Comments are interspersed into the CNF to facilitate debugging.