CODEWITHSUNDEEP
prologboolean-logicconjunctive-normal-form
user502187
user502187

Reputation:

Compression of a positive DNF

I would like to compress positive propositional formulas in disjunctive normal form (DNF).

I am only assuming simple DNF for the moment without negated literals. The reverse process, the decompression can be easily defined. For a formula only built from conjunction and disjunction, the following rewriting rules will generate a DNF:

A & (B v C) --> (A & B) v (A & C)
(A v B) & C --> (A & C) v (B & C)

Here is an example of a decompression:

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.

Now I wonder whether there are some algorithms around which can generate a single formula back from a DNF. I have already looked into binary decision diagrams. The problem I have with these is that they cannot combine all disjunctions on the way.

For example the algorithms for binary decision diagrams that use sharing, would still show similar branches during printing and/or introduce new prepositional variables, both things are not desired:

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.

The result should be a single formula, not anymore DNF, which is more compact than the binary decision diagram algorithms which uses only disjunction and conjunction, and the prepositional variables already found in the original DNF. Here is an example of the desired compression:

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.

What would be your take? Prolog implementations preferred.

Bye

Upvotes: 3

Views: 903

Answers (1)

gusbro
gusbro

Reputation: 22585

I think what you need is a systematic algorithm to compute the minimum of a boolean expression in two layers (either a disjunction of conjunctions of the input variables, or a conjunction of disjunctions of the input variables).

The usual algorithms used to do this are the Karnaugh maps and the Quine-McCluskey algorithms.

These algorithms do work with negated variables. In any case, at least if your input is in disjunctive normal form (DNF) and no negated variables appear, the output expressed as disjunction of conjunction of the input variables won't have negated variables either).

Upvotes: 1

Related Questions