Проверить комбинаторные кодировки CNF SAT?

Я пытаюсь решить комбинаторную проблему с помощью SAT Solver.

введите описание изображения здесь

Это включает в себя следующие шаги:

  1. Закодируйте проблему как набор логических выражений.
  2. Переведите сочетание выражений в CNF / DIMACS
    (используя собственные инструменты, bc2cnf, bool2cnf или Limboole)
  3. Решите CNF
    (используя SAT Solvers, например Cryptominisat, Plingeling, застежка или Z3)
  4. Переведите решение (при условии, что результат «SAT») обратно в проблемную область.

В моем случае это работает для небольших образцов. Но для более сложных задач решателю SAT требуются часы или даже дни, чтобы не прийти к выводу SAT / UNSAT. Я пытаюсь настроить кодировку, чтобы найти решение. Но чем больше усилий я прилагаю к кодированию, тем менее уверен, что моя кодировка действительно правильная (т.е. «эквивалент выполнимости»).

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

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

Мой вопрос:

Как я могу убедиться, что данная кодировка является допустимым представлением исходного логического выражения?

Из литературы мне известны решения некоторых проблем, которые я мог бы преобразовать в присвоения переменных, чтобы получить доверие к моему процессу кодирования. Но из-за кодировки Цейтина большинство переменных в моем CNF являются вспомогательными (переключение) переменные. Без кодирования Цейтина моя CNF была бы слишком большой, чтобы ее можно было решить. Поэтому я не могу просто проверить, выполняется ли каждое предложение CNF известным решением.

Я попытался преобразовать CNF обратно в логические выражения, используя cnf2aig, но инструмент все еще в своем младенчество. Без переключения переменных легко проверить соответствие логическим выражениям основных проблемных переменных.

Есть несколько публикаций о подходах "CNF-to-circuit", но ни одна из них не дает полезного инструмента.

Есть ли какая-нибудь передовая практика для выполнения такой проверки?


encoding combinatorics boolean-expression satisfiability
person Axel Kemper    schedule 15.01.2014    source источник
comment
Вы хотите запустить проверку того же выражения, которое вы хотите решить, или небольшого тестового примера? Все схемы валидации, которые приходят мне в голову, вероятно, не менее сложны, чем решение самой проблемы SAT.   -  person CliffordVienna    schedule 17.01.2014
comment
Ты прав. Случаев валидации меньше.   -  person Axel Kemper    schedule 17.01.2014
comment
Я должен подчеркнуть (см. Пункт 2 в моем списке), что мое логическое выражение представляет собой соединение множества более мелких выражений. Итак, я мог отдельно проверить каждое из подвыражений.   -  person Axel Kemper    schedule 17.01.2014

Ответы (1)


arrow_upward
1
arrow_downward

Итак, вы спрашиваете:

Имея логическое выражение B и CNF C, есть ли способ определить, являются ли они равно удовлетворяемыми?

Или другими словами:

Существует ли модель, удовлетворяющая B, но не C, или модель C, но не B? Если такой модели не существует, то обе эквивалентны.

Мое решение этой проблемы было бы следующим:

  1. Я бы использовал заведомо хорошее программное обеспечение (например, ваш неоптимизированный код или сторонний инструмент) для создания заведомо хорошей CNF D из логического выражения.

  2. Используйте Tseitin, чтобы сгенерировать CNF для! B из C и D. Т.е. интерпретировать CNF для C как произведение сумм (конъюнкция дизъюнкции) и инвертировать все выражение. Назовем полученные CNF C 'обратными C и D' обратными D.

    Таким образом, модель, удовлетворяющая C, не удовлетворяет C ', и наоборот. Аналогично для D и D '.

  3. Используйте решатель SAT, чтобы найти модель, удовлетворяющую C и D '. Такая модель удовлетворяет C, но не удовлетворяет B.

  4. Используйте решатель SAT, чтобы найти модель, которая удовлетворяет C 'и D. Такая модель удовлетворяет B, но не C.

  5. Если шаги 3 и 4 не дают модели (неудовлетворительно), значит, вы доказали, что B и C равно выполнимы.

Шаги 3 и 4 просты. Просто создайте одну большую CNF, содержащую все предложения из двух CNF. Все переменные из B должны быть закодированы одним и тем же литералом в обеих CNF, а вспомогательные переменные должны выделяться из разных пулов.

В зависимости от вашей проблемы, шаги 3 и 4 могут быть довольно дорогостоящими в вычислительном отношении. Таким образом, этот подход может быть осуществим только в том случае, если вы можете разделить свою проблему на более мелкие части, которые можно проверить независимо друг от друга.

Надеюсь, это поможет. Вы сказали, что пытаетесь убедиться, что ваши оптимизации верны, поэтому у вас должна быть заведомо надежная реализация. В противном случае вы можете использовать библиотеку, которую я написал, как внешнюю ссылку:

https://github.com/cliffordwolf/yosys/tree/master/libs/ezsat

CNF, созданная этой библиотекой, не очень эффективна! Но это хорошо проверено ..

person CliffordVienna    schedule 17.01.2014
comment
Хороший ответ, но проверки CNF и логического выражения, вероятно, недостаточно. Я бы хотел убедиться, что CNF действительно представляет исходную проблему. - person Axel Kemper; 17.01.2014
comment
На самом деле я проверяю здесь CNF vs. CNF и просто расширяю его до CNF vs. boolean, используя известную справочную реализацию boolean ›cnf для создания второго. CNF. Вы, конечно, можете расширить это, также используя логический ›код заведомо исправной задачи для генерации второй CNF. - person CliffordVienna; 17.01.2014
comment
Извините, но я все еще сомневаюсь. Известное решение исходной проблемы как единичный минтерм не покрывает все мыслимые решения и, таким образом, не удовлетворяет проверке CNF. Неоптимизированная заведомо исправная CNF слишком велика для нетривиальных случаев. На данный момент мой подход состоит в том, чтобы разделить CNF на кластеры / конусы, которые являются диъюнктивными по отношению к. к переменным переключения. Я надеюсь, что смогу проверить их один за другим путем повторного распространения единиц. Я обновлю вопрос, как только у меня будет более четкое представление. - person Axel Kemper; 18.01.2014