как такую задачу поставить SAT-солверу, научился по сути у Феди Куянова
кроме переменных со смыслом «такая-то клетка поля принадлежит такой-то фигуре» заведем, грубо говоря, по переменной для каждого потенциально возможного движения
и напишем условия
1) что каждая клетка поля принадлежит ровно одной фигуре;
2) что если данное движение выбрано (соотв. ему переменная True), то оно переводит первую фигуру во вторую;
2') что хоть одно движение выбрано
(если режем не на две, а на K частей, то для каждого движения будет не одна а (K-1) переменная со смыслом «это движение переводит фигуру №0 в фигуру №l»)
как конкретно закодировать, что движение
s переводит одну фигуру в другую? грубо говоря, для каждой клетки c надо добавить условие [-s,-c_0,s(c)_l] («если уж выбрано движение s, а клетка c выбрана в фигуру №0, то клетка s(c) должна быть выбрана в фигуру №l) и условие [-s,-c_l,s^{-1}(c)_0] (чтобы было не просто вложение, а биекция)остается еще техническая возня — потому что, скажем, символ s выше используется в трех разных (с т.з. питона) смыслах (перебираю я наборы чисел — на сколько, грубо говоря, сдвигать-поворачиать; по каждому набору строится отображение, просто так написать в коде s(c) нельзя; а сат-солверу в списке условий нужно отдавать ни то и ни другое, а отдельно заведенный номер переменной…), или, скажем, я замел под ковер то, что s(c) может вылезти за границы фигуры и тогда никакой переменной s(c)_l вообще нет (контрольный вопрос: какое условие надо тогда написать : ) — но всё ж логика не такая сложная… и даже код вышел не длинный
на кружке объясняю, что при решении задач на разрезание на равные части полезно бывает думать, какое конкретно движение их совмещает — и нравится, что та же математика помогает при общении на эти темы с компьютером