Further Optimize Initial Transposition
SSoelvsten opened this issue · 0 comments
SSoelvsten commented
The initial transposition sweep seems to be an endless ground for optimization in many cases.
- From #654 we unexpectedly notice that the constant involved in a simple transposition is small enough to offset any potential cost of an additional nested sweep.
- From #653 we see that terminal pruning during quantification can be worth it.
- From #647 we see that a single partial quantification is really good in some cases.
Which leads to more questions:
- Is the constant involved in a simpler Restrict-like sweep better?
- Is it enough to not have to think about a transposition being faster?
ANSWER: There is still a 2% overhead. - What is a heuristic to enable terminal pruning?
HYPOTHESIS: look at the terminal count and possibly the width/nodes ratio.
- Is it enough to not have to think about a transposition being faster?
- Is there any case, where deepest quantification is good?
- If so, what is particular to these instances?
HYPOTHESIS: this would be if the deepest variable is very shallow.
- If so, what is particular to these instances?
- Is partial quantification good/bad due to it shuffling the children around regardless of the original assignment?
- Either way, what is a proper heuristic to enable a single partial quantification?
For implementation(s) of the above, we may want to add the following.
- Replace the
__quantify__get_deepest
with a__quantify__pred_profile
that doesn't stop early but instead records a lot of information.- Total number of nodes.
- Total number of variables.
- Total number of variables quantified.
- + Number of deep variables (last N/3 and beneath the widest level)
- + Number of shallow variables (first N/3 and above the widest level)
- The deepest to-be quantified variable (independent of the above "deep").
- + the number of nodes beneath it.
- + width of this level.
- The shallowest to-be quantified variable (independent of the above "shallow").
- + the number of nodes beneath it.
- + width of this level.
- The widest to-be quantified variable.
- + the number of nodes beneath it.
- + width of this level.
- The narrowest to-be quantified variable.
- + the number of nodes beneath it.
- + width of this level.
- Min/max distance between quantified variables.
- The
__quantify__max_partial_sweeps
should also use this profile instead, instead of reopening the file.