Morning productivity

I've added the definition of the constraint variables and constraint system for a boolean formula, and a rough sketch of the equivalence between SAT solutions and CS solutions of these systems. More detail needs to be added, but it's a beginning.

I think I'll try to do more morning work from now on, the afternoons in this heat are exhausting.