Упрощая формулу CNF, сохраняя при этом всех решениях WRT некоторых переменных

Question

Связанные: CNF simplification (на самом деле, я думаю, что податель этого вопроса мог бы быть после того, что я хочу здесь)

ряд инструментов существует для упрощения (или " preprocessing "до решения). Формат DIMACS в формате CNF, и большинство решателей SAT включают некоторые. Однако все, что мне известно, упрощает тривиально выполнимую формулу в тривиально-выполнимую CNF с нулевой или одной переменной, т. Е. Они только пытаются сохранить выполнимость формулы. Я пробовал, по крайней мере, режим предварительной обработки SatELite и cryptominisat.

Однако для построения CNF большой проблемы мне кажется, что было бы очень полезно упростить четко определенное подмножество задачи за раз, которое затем может повторяться много раз в конечной CNF с дополнительными ограничениями между некоторыми переменными в этих подформулах.

Таким образом, существуют ли какие-либо инструменты или могут использоваться обычные решатели SAT (или другие решатели, такие как Z3, которые я использую для создания CNF, которые я хотел бы свести к минимуму), как-то использовать с некоторой утонченностью, чтобы упростить формулу CNF сохраняя при этом все решения по заданному набору переменных?

Answer 1

Coprocessor SAT препроцессор может делать то, что вы хотите. Он может быть предоставлен необязательный диапазон переменных и будет применять только упрощающие эквивалентность упрощения в пределах этой области. Вне этого объема он будет применять более сильные, упрощающие и сохраняющие упрощения. По крайней мере, это было в версии 2.

Answer 2

Возможно, не совсем то, что вы ищете, но эспрессо-система (http://embedded.eecs.berkeley.edu/pubs/downloads/espresso/) может выполнять булево упрощение. К настоящему времени уже более 20 лет, но по-прежнему используется в отрасли для того, что она делает.

Answer 3

Другой подход заключается в преобразовании CNF в И-Inverter-Graph (AIG) и применять методы от логического синтеза реструктурировать и упростить AIG.

Это сделано в программном пакете ABC, разработанном в Университете Беркли. Один из методов: структурное хеширование: найти общий (эквивалент) подвыражения в пределах AIG и связать их вместе, чтобы обрезать график.

Университет Линца в Австрии предлагает набор инструментов AIGER, специально предназначенный для графиков And-Inverter.