Stop Cnf_CollectLeaves rescanning the vector on every push - #555
Open
TrevorHansen wants to merge 1 commit into
Open
Stop Cnf_CollectLeaves rescanning the vector on every push#555TrevorHansen wants to merge 1 commit into
TrevorHansen wants to merge 1 commit into
Conversation
Cnf_CollectLeaves() walks down from a root to the boundary of a multi-input gate and collects the leaves, suppressing duplicates with Vec_PtrPushUnique(), which scans the whole vector on every push. A gate with n leaves therefore costs O(n^2). On wide inputs that scan dominates CNF derivation. Over a sample of the non-incremental SMT-LIB benchmarks, Cnf_CollectLeaves_rec is 65.8% of the aggregate time of the eighty heaviest files, and 97-99% of the run on four of them. The widest gate in that sample has 2,393,038 leaves: about 3e12 comparisons, against about 5e7 after this change. Nothing reads vSuper during the walk, so the check does not have to happen at push time. Once the vector reaches sixteen entries the walk pushes blind and Vec_PtrUniqify() takes the repeats out at the end; below that the original scan stays, so the small gates -- 99.3% of collections return four leaves or fewer -- keep the old path. Leaves are compared by literal rather than by address, so the result does not depend on the allocator. Only clause order changes. Every consumer sensitive to the order of the leaves needs fewer of them than the threshold: the absorption scan in Cnf_DeriveFastMark() runs only when the gate has under six leaves, and Cnf_CutDeriveTruth() takes at most six. Cnf_CollectVolume() depends on the leaf set rather than its order, and the remaining callers use only Vec_PtrSize(). What is left is the AND-gate path in Cnf_ComputeClauses(), which emits the big clause and the unit clauses by walking the vector, so a sorted gate gives the same clauses in a different order. Measured to the point where the CNF is complete: -60.8% of retired instructions over a tail-weighted 1,251-file subset, and 33.0s to 0.55s on the file that prompted this. The emitted CNF is byte-identical on 1,183 of those files and the same clause set, reordered, on the other 68.
TrevorHansen
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Cnf_CollectLeaves()walks down from a root to the boundary of a multi-input gate and collects the leaves, suppressing duplicates withVec_PtrPushUnique()- which scans the whole vector on every push. This is O(n^2).On a bitvector benchmark whose widest gate has 2.4M leaves, that is about 3x10^12 comparisons. With this PR it drops to about 5x10^7, about 57,000x fewer - it becomes O(n log n).
Instead of de-duplicating on each push, once a cut-off is reached entries are just pushed, then de-duplicated in a final pass with
Vec_PtrUniqify(). Below the cut-off the original scan stays.This produces the leaves of a wide gate in sorted rather than visited order. I couldn't find a stable de-dupe in the tree, and adding one seemed worse than reordering.