Details
-
Task
-
Resolution: Unresolved
-
Major - P3
-
None
-
None
-
None
-
None
-
Query Optimization
Description
Currently the way we implement conversion from CNF to DNF works by building up a tree in place, something like this:
input: (a0+a1).(b0+b1).(c0+c1)
|
|
|
take the first conjunct:
|
(a0) + (a1)
|
|
|
multiply by the next conjunct:
|
(a0.b0) +
|
(a0.b1) +
|
(a1.b0) +
|
(a1.b1)
|
|
|
multiply by the next conjunct
|
(a0.b0.c0) + (a0.b0.c1) +
|
(a0.b1.c0) + (a0.b1.c1) +
|
(a1.b0.c0) + (a1.b0.c1) +
|
(a1.b1.c0) + (a1.b1.c1)
|
These intermediate trees can't use a BoolExpr Builder because we both read and write them. It would be better to find a way to insert directly to a Builder, so we can eliminate trivial terms more eagerly, and allocate less.
This multiplication of expressions is really just one way to enumerate combinations of atoms. Given the expression (a0+a1).(b0+b1).(c0+c1), we have 3 choices with 2 options each, so the final expression has 8 terms. Each term makes a different choice of a0 vs a1, b0 vs b1, etc.
The current algorithm is like a breadth-first search: it's maintaining a set of 1-atom terms, then growing it to all 2-atom term, etc, until we have the final set of complete terms.
We could use a depth-first search instead:
input: (a0+a1).(b0+b1).(c0+c1)
|
|
|
find all terms starting with (a0)
|
find all terms starting with (a0.b0)
|
insert (a0.b0.c0) to the builder
|
insert (a0.b0.c1) to the builder
|
find all terms starting with (a0.b1)
|
insert (a0.b1.c0) to the builder
|
insert (a0.b1.c1) to the builder
|
...
|
This would use a single temp vector, or vector of indices, because it only considers one combination at a time.