SAT encoding for loops

• might be a good addition to enumerative methods
• also, as a showcase for my ISR course