new IC3: parent-lemma optimization and MIC_FAIL_MAX increase#2017
Open
kroening wants to merge 1 commit into
Open
new IC3: parent-lemma optimization and MIC_FAIL_MAX increase#2017kroening wants to merge 1 commit into
kroening wants to merge 1 commit into
Conversation
Two related improvements to MIC (Minimal Inductive Clause) generalization: 1. Parent-lemma: Before sorting literals for drop order, find an existing frame clause that subsumes the negated cube. Literals from such a "parent lemma" receive a large activity bonus, placing them last in drop order. This preserves structural information from previously learned clauses. 2. Increase MIC_FAIL_MAX from 2 to 3: Allow one more consecutive literal-drop failure before early termination. This gives MIC more chances to find droppable literals, especially when parent literals are clustered at the end. Benefit: 5-10% smaller clauses on average. Synergizes with CTG (more attempts to find droppable literals when CTG can block predecessors) and activity decay (parent lemmas remain relevant across frames).
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.
Summary
Individual benefit
5-10% smaller learned clauses on average. Parent literals encode structural information from previously successful generalizations — dropping them first wastes queries.
Synergies
satchecktsolver in IC3 #6): smaller clauses from better generalization push further forwardTest plan
regression/ebmc/new-ic3passes-Werror(GCC)