Упрощение формулы CNF при сохранении всех решений с определенными переменными
Связанный: упрощение CNF (фактически, я думаю, что автор этого вопроса мог быть после того, что я хочу здесь)
Существует ряд инструментов для упрощения (или "предварительной обработки" перед решением) формул CNF в формате DIMACS, и большинство решателей SAT включают некоторые из них. Однако все, что мне известно, упрощает тривиально выполнимую формулу в тривиально выполнимую ФНБ с нулем или одной переменной, то есть они только пытаются сохранить выполнимость формулы. Я пробовал по крайней мере режим предварительной обработки SatELite и cryptominisat.
Однако для построения КНФ большой проблемы мне кажется, что было бы весьма полезно упростить четко определенное подмножество задачи за один раз, что затем может повторяться большое количество раз в конечном КНФ с дополнительными ограничения между некоторыми переменными в этих подформул.
Итак, существуют ли какие-либо инструменты, или могут ли обычные SAT-решатели (или другие решатели, такие как Z3, которые я использую для создания CNF, которые я хотел бы минимизировать) каким-то образом использоваться с некоторой сообразительностью, чтобы упростить формулу CNF при сохранении всех решений относительно заданного набора переменных?
3 ответа
Препроцессор Coprocessor SAT может делать то, что вы хотите. Ему может быть предоставлена необязательная переменная область действия, и в этой области будут применяться только упрощения, сохраняющие эквивалентность. За пределами этой области будут применяться более строгие, сохраняющие удовлетворение упрощения. По крайней мере, так было в версии 2.
Возможно, не совсем то, что вы ищете, но система эспрессо ( http://embedded.eecs.berkeley.edu/pubs/downloads/espresso/) может сделать логическое упрощение. Ему уже более 20 лет, но он все еще используется в промышленности для своих целей.
Другой подход заключается в преобразовании CNF в И-Инвертор-График (AIG) и применять методы логического синтеза для реструктуризации и упрощения AIG,
Это делается в наборе программ ABC, разработанном в университете Беркли. Одним из методов является структурное хеширование: найти общие (эквивалентные) подвыражения в пределах AIG и свяжите их вместе, чтобы обрезать график.
Университет Линца в Австрии предоставляет набор инструментов AIGER, специально предназначенный для графов And-Inverter.