python-nnf
python-nnf copied to clipboard
Advanced Simplification
Either a modification of the simplify method or an extended version / separate:
- If an internal node has both a literal and it's negation, replace it with
true(if anOr) orfalse(if anAnd), as appropriate. - If every child of an
Ornodenis either literalL, or of the formAnd([L, ...]), then removeLfrom the children and add it to the parent ofn. Ifnis the root, then a new root is created:And([L, n])
The first fixes some degenerate cases, and the second propagates recognized backbones up the structure. It needs to be revised slightly for DAGs instead of trees -- (1) only remove the literal if there's no other incoming edge to the And node child of n; and (2) another simplification to remove redundant literals if they are already implied (all ancestor paths have an And node with the literal as a sibling) -- but it's an important step in being able to assess backbones quickly (useful in other fields like planning with partial observability).