Итак, у меня есть cnf и два списка переменных K и C.
Переменные K добавляются в cnf как единичные предложения (либо отрицательные, либо не зависящие от логического массива) перед отправкой его в sat-solver. Когда спутниковый решатель возвращает модель, я забочусь только о переменных, которые также встречаются в C, и все другие переменные в модели отбрасываются.
Поскольку cnf должен запускаться повторно (с разными переменными из K, установленными в true или false), стоило бы потратить несколько часов, чтобы упростить cnf и удалить ненужные переменные (ненужными являются любые переменные, которые не входят ни в K или C) если это означает, что бритье на несколько минут каждый раз, когда это необходимо решить.
Мой вопрос заключается в том, могу ли я использовать исключение переменных разрешения, как описано в этом pdf или этом блоггпосте , чтобы исключить некоторые переменные, если я не исключаю ни одну переменную, которая встречается в или K или C. Или, если это изменит полученную модель относительно переменных в C?