Repository navigation
Automatic conjunct/disjunct simplification #23
Description
Not sure if this should be optional or the default, but a common pattern in building theories has raised an issue...
T = true
T &= <constraint 1>
T &= <constraint 2>
...This ends up creating a theory T such as And(<constraint 1>, And(<constraint 2>, And ( ... ))). With any moderately sized theory, the recursion depth is hit in a variety of ways (checking height, simplifying, etc). The workaround was to just store the constraints in a list of conjuncts and then wrap as And(conjuncts), but something like the following might be reasonable behaviour:
- If taking the
Andof two theories withAndas their root, return theAndof their children. I.e.,And(T1.children, T2.children) - If just one theory (wlog, assume
T1) is anAnd, add the other theory as a child of it. I.e.,And(T1.children, T2) - If neither theory is an
And, do as normal. I.e.,And(T1, T2) - Same for disjunctions.
Activity
blyxxyz commentedon Aug 30, 2020
This is tricky.
Making
&=combine nodes would give terrible performance. It's currently O(1), but combining nodes is O(n) in the number of children (because it has to construct a whole new frozenset), so repeated use of&=would go from O(n) to O(n²). It's the same problem as repeatedly using+=on strings.(It's in principle possible to solve this at a low level, see e.g. efficient mutation in the
frozenmapproposal. But I don't think that's reasonable here.)Merging nodes can also drastically increase the sentence size, at least in contrived cases and possibly even in useful cases. Consider this sentence:
If we run
.simplify()on it the singleOrnode at the bottom is merged with each of the five otherOrnodes and we get this:That increases the sentence size from 20 to 35.
For the same structure with 100 variables it increases the size from 400 to 10200.
(
.simplify()takes amerge_nodes=Falseargument for this reason.)So I'm hesitant to combine nodes automatically. It can make things worse, and the current behavior is at least very easy to analyze.
But it may be reasonable and feasible (though tricky) to restructure
.simplify()to use some kind of queue instead of the call stack so that it never hits the recursion limit. Then you could use that after constructing the sentence to "fix" it.Maybe other methods could be adjusted as well. It would definitely be nice to be able to handle sentences of unlimited depth.
haz commentedon Aug 30, 2020
Fair enough -- this issue, along with some of the others that have come up, stem from my first medium scale encoding task with the library. It occurs to me that we might want custom functionality for building theories destined for a SAT solver.
custom_object.add_constraint(<NNF>)instead ofT &= <NNF>custom_object.to_CNF(demorgan=True)I'm also thinking of a set of decorators to turn arbitrary object oriented code into SAT encodings, that would make sense in such a library.
Think it makes sense as part of
python-nnfor a separate library that builds on it?haz commentedon Sep 11, 2020
Unless there's major objections, I think we'll move forward with a companion library that focuses on advanced techniques for modelling. It will build heavily on
nnf, and the student (👋 @karishmadaga ) will likely contribute fixes/enhancements to this library too.blyxxyz commentedon Sep 11, 2020
Making
simplify()work with these tall sentences turned out to be harder than I thought, because the intermediate results take up too much memory even if you work around the recursion limit.A higher level companion library sounds like a great idea.