Comments 8
В разговорах про решения с помощью SAT как обычно тут не хватает самой главной части - как из вон той формулы получить КНФ, скормить ее солверам и по результату уже дать ответ для каких-то заданных вводных. В общем show me the code, хотя бы на том же питоне, хотя бы на SMT, как это было в статье про крестики-нолики, и чтобы запустил тест и оно все отработало и наглядно.
Это какой-то жёсткий брут-форс.
Для размера задачи 20 книг и 10 предметов, выходит 200 переменных.
Не будет ли оптимальнее взять 20 переменных по кол-ву книг xi=0/1 (книга i взята/не взята) и придумать какой-то предикат, определяющий что количество переменных x со значением 1 ровно k штук.
Тогда длина КНФ будет порядка 
.
Это если "в лоб" делать.
А если реализовать на булевских функциях комбинационную схему сумматора, и сравнивать его побитовый выход с числом k?
Тогда потребуется соединить N сумматоров. К тому же сложность решения такой задачи выполнимости может сильно возрасти. В первоначальном варианте КНФ имеет простую структуру, и методу типа резолюций будет легче справиться с этой задачей.
Тут же не полноценные сумматоры, а только делающие +1*xi к предыдущему выходу.
И длина числа (кол-во суммируемых бит log2(k), что немного.
Интересна зависимость, как растёт сложность задачи от числа свободных переменных.
Конечно, зависит от формул. Но мне кажется, в общем случае - экспоненциально.
То есть, начиная с каких-то N,M оптимизация станет обязательной.
Всё уже давно придумано: https://habr.com/ru/articles/408299
Решение задачи о покрытии с помощью SAT-солвера