Я хотел бы сжать положительные пропозициональные формулы в дизъюнктивную нормальную форму (ДНФ).
На данный момент я предполагаю только простой DNF без отрицательных литералов. Обратный процесс, декомпрессию можно легко определить. Для формулы, построенной только на основе конъюнкции и дизъюнкции, следующие правила перезаписи будут генерировать DNF:
A & (B v C) --> (A & B) v (A & C)
(A v B) & C --> (A & C) v (B & C)
Вот пример декомпрессии:
Example: Decompression
Input:
(p & (q v r) & s & (t v u)) v
w.
Output:
(p & q & s & t) v
(p & r & s & t) v
(p & q & s & u) v
(p & r & s & u) v
w.
Теперь мне интересно, есть ли какие-нибудь алгоритмы, которые могут сгенерировать одну формулу обратно из DNF. Я уже изучал диаграммы бинарных решений. Проблема, с которой я сталкиваюсь, заключается в том, что они не могут объединить все дизъюнкции на своем пути.
Например, алгоритмы для бинарных диаграмм решений, которые используют совместное использование, по-прежнему будут показывать аналогичные ветви во время печати и / или вводить новые предложные переменные, и то, и другое нежелательно:
Example: Compression (Bad)
Input:
(p & q & s & t) v
(p & r & s & t) v
(p & q & s & u) v
(p & r & s & u) v
w.
Output:
(p & ((q & s & (t v u)) v (r & s & (t v u)))) v
w.
- or -
Output:
(p & ((q & h) v (r & h))) & (h <-> s & (t v u))) v
w.
Результатом должна быть единственная формула, больше не DNF, которая более компактна, чем алгоритмы диаграммы двоичных решений, в которых используются только дизъюнкция и конъюнкция, а также предложные переменные, уже найденные в исходной DNF. Вот пример желаемого сжатия:
Example: Compression (Good)
Input:
(p & q & s & t) v
(p & r & s & t) v
(p & q & s & u) v
(p & r & s & u) v
w.
Output:
(p & (q v r) & s & (t v u)) v
w.
Что бы вы сделали? Предпочтительны реализации Prolog.
Пока
