Сжатие положительного DNF

Question

Я хотел бы сжать позитивные пропозициональные формулы в дизъюнктивной нормальной форме (DNF).

Я только предполагаю простой 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.

Что бы вы взяли? Пролог реализации предпочтительнее.

до свидания

Answer 1

Я думаю, что вам нужен систематический алгоритм для вычисления минимума логического выражения в двух слоях (либо дизъюнкция конъюнкций входных переменных, либо конъюнкция дизъюнкций входных переменных).

Обычные алгоритмы, используемые для этого, - карты Карно и алгоритмы Куайна-МакКласки.

Эти алгоритмы работают с отрицательными переменными. В любом случае, по крайней мере, если ваши входные данные имеют дизъюнктивную нормальную форму (DNF) и не отображаются отрицательные переменные, выходные данные, выраженные как дизъюнкция соединения входных переменных, также не будут иметь отрицательные переменные).