Sum the crossing count scaled by the inside width in the T term - #44
Merged
Conversation
The separator term summed 2^w0 over the internal cuts, w0 the smallest of the inside width, the outside width and the crossing-clause count. As the width the term sums, that minimum favours a cut whose outside width is small, and the chain a shallow edge-binarized reading builds keeps the outside width small at every node while carrying most of the formula across each cut. The conversion search chose those chains, and they do not compile. The term now sums 2^(cross · in / m) per cut: the crossing count scaled by the inside width over the clause count, which is at most the inside width. The excess term is still measured against the sum of the smallest bound, and every other term is unchanged. On 44 formulas with six trees each, every tree compiled under the same compiler with a 60 s budget, the minimum ordered a compiling tree below a failing one in 71 of 240 pairs and picked a compiling tree among the portfolio's own candidates on 4 of 23 formulas; the new width reads 193 of 240 and 14 of 23. End to end, on the 1,074 model-counting competition track-1 instances at 120 s, the count goes from 511 to 574 with 65 gained and 2 lost, and the instances both solve run at the same speed. The peak-mode selection pin moves with the score: the multiplier fixture's winner was re-observed as flowcutter-primal in five of five runs.
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.
The separator term of
vtree_costsummed2^w0over the internal cuts, withw0the smallest of the inside width, the outside width and the crossing-clause count. As the width the term sums, that minimum favours a cut whose outside width is small. The chain a shallow edge-binarized reading builds keeps the outside width small at every node while carrying most of the formula across each cut, so the conversion search chose those chains, and they do not compile.The term now sums
2^(cross · in / m)per cut — the crossing count scaled by the inside width over the clause count, which is at most the inside width. The excess term is still measured against the sum of the smallest bound; every other term is unchanged, and the module doc states the formula.Evidence, offline: 44 formulas with six trees each (the previous release's pick and every catalogue family), every tree compiled under one compiler with a 60 s budget. The minimum ordered a compiling tree below a failing one in 71 of 240 pairs and picked a compiling tree among the portfolio's own candidates on 4 of 23 formulas; the new width reads 193 of 240 and 14 of 23. End to end, on the 1,074 model-counting competition track-1 instances at 120 s, the count goes from 511 to 574, 65 gained and 2 lost, with the instances both solve running at the same speed.
Two tests move with the score and are updated: the hand-computed fixture cost (separator term 3 → 1.8, worked in the comment) and the peak-mode selection pin, whose multiplier-fixture winner was re-observed as
flowcutter-primalin five of five runs.