Encontrar todas las combinaciones de poliominoes libres dentro de un área específica con un solucionador SAT (Python)

Soy nuevo en el mundo de los solucionadores de SAT y necesitaría alguna orientación sobre el siguiente problema. Teniendo en cuenta que: ❶ Tengo una selección de 14 celdas adyacentes en una cuadrícula de 4 * 4 ❷ Tengo 5 poliominoes (A, B, C, D, E) de tamaños 4, 2, 5, 2 y 1 ❸ estos poliominós...