Conversation
msoos
force-pushed
the
aig-shared-ptr-better-fix
branch
from
a34f3fb to
bad75fe
Compare
msoos
force-pushed
the
aig-shared-ptr-better-fix
branch
from
4fadcf0 to
f723050
Compare
specifically on ~/media/counting/mccomp2024/track3-pmc/mc2024_track3_031.cnf.gz
msoos
force-pushed
the
aig-shared-ptr-better-fix
branch
from
6039ef3 to
faa4aaa
Compare
…on, add move semantics to SimplifiedCNF" This reverts commit e028cc0.
msoos
force-pushed
the
aig-shared-ptr-better-fix
branch
from
e2577eb to
e350b21
Compare
When a non-final Manthan strategy hits its max_repairs limit without finishing synthesis, subsequent non-final strategies are unlikely to succeed either. Reduce their repair budget to 1/4 of the original to avoid wasting time. The final (unlimited) strategy is unaffected. On sdlx-fixpoint-10, this saves ~2s by reducing the second const strategy from 400 to 100 repairs when the first const strategy already showed the approach isn't working for this instance. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
For variables repaired >= 10 times, run an additional conflict minimization pass. The greedy literal removal depends on iteration order (which is shuffled), so a second pass with different ordering can find additional removable literals, producing smaller conflicts that cover more input patterns per repair. On sdlx-fixpoint-10: 2825 vs 2944 repairs (-4%), avg needs_repair 35.41 vs 42.88 (-17%), repair time 41.74s vs 42.84s. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
When selecting the best counterexample from the collected set, weight each wrong variable by how often it has been repaired. This prefers CEXes where frequently-repaired (expensive) variables are already correct, reducing future repair work on hot variables. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…licts When find_better_ctx_normal encounters a large UNSAT conflict (>5 conflicting soft assumptions), remove all conflicting variables at once instead of one at a time. This reduces the number of solver iterations needed to converge, especially when many variables cannot be fixed simultaneously. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
When the counterexample has <= 5 variables needing repair, skip the find_better_ctx optimization step. Creating a fresh SAT solver and iteratively removing conflicting assumptions isn't worth the overhead when the repair set is already small. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
When a variable has been repaired >= 10 times, try up to 2 additional conflict minimization passes (with different random orderings) instead of just 1. Stop early if no progress is made. This further reduces conflict sizes for frequently-repaired variables, making each repair cover more input patterns. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
In find_better_ctx_normal, boost the priority weight of variables that have been repaired before, making the solver try harder to keep those vars correct. This prevents the optimizer from giving up on expensive-to-repair variables, reducing future repair work. On sdlx-fixpoint-10: 2766 vs 2810 repairs (-1.6%), which combined with earlier improvements gives 2766 vs 2944 baseline (-6%). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Raise the threshold for skipping find_better_ctx from 5 to 10. When fewer than 10 variables need repair, the overhead of creating a fresh SAT solver and iteratively removing conflicts isn't worth the potential improvement. This particularly helps the const strategies which often have small needs_repair sets. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
When the repair constant is TRUE, ITE(guard, TRUE, old) simplifies to OR(guard, old). When FALSE, ITE(guard, FALSE, old) simplifies to AND(NOT(guard), old). This creates flatter AIGs with fewer nodes and fewer CNF clauses (3 instead of 7 per repair), making the solver more efficient at finding conflicts. Benchmark sdlx-fixpoint-10: repair time 44.98s (was 52.37s), total repairs 2912 (was 3831), total time 55.37s (was 62.66s). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
In the cost-0 case (repair solver finds y_rep compatible with formula), only update y_rep and variables after it in the order from the solver model. Variables before y_rep are already correct and must stay that way for subsequent repairs. This eliminates the need for an expensive recompute_all_y_hat_cnf call since formulas and inputs haven't changed. Saves ~1300 cex_solver calls per run. Benchmark sdlx-fixpoint-10: repair time 42.60s (was 44.98s), total 53.06s (was 55.37s). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The old compose_and used neg(compose_or(neg, neg)) which creates ~7 AIG nodes per AND operation due to double negation in the AIG tree. The direct encoding creates just 1 AND node with the same 3 CNF clauses. This dramatically reduces AIG size for FALSE repairs where AND(NOT(guard), old_formula) is used. Benchmark sdlx-fixpoint-10: repair time 38.47s (was 42.60s), total 48.81s (was 53.06s), 436 loops (was 461). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Weight wrong variables quadratically by their position in y_order, heavily penalizing CEXs where early variables are wrong. Early variables are repaired first and cascade to affect later ones, so keeping them correct in the selected CEX reduces total repair effort. Also multiply repair count weight by 10 to more aggressively avoid CEXs that trigger frequently-repaired variables. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
… identity In AIG::new_not: detect NOT(NOT(x)) pattern and return x directly, and fold NOT(lit(v,neg)) into lit(v,!neg) instead of creating an AND node. In AIG::new_and: detect AND(x,x) and return x directly. These simplifications reduce AIG node count, especially for hot variables with many repair guards. Fewer nodes → smaller formulas → faster solver → fewer repairs. Benchmark sdlx-fixpoint-10: repair time 35.78s (was 38.47s), total 47.63s (was 48.81s), repairs 2751 (was 2956), cost-0 935 (was 1232). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
In new_ite: simplify ITE(TRUE,l,r)=l, ITE(FALSE,l,r)=r, ITE(b,x,x)=x. In new_not: fold NOT(const) to const with flipped polarity, avoiding unnecessary AND nodes for constant negation. These simplifications reduce AIG node count, particularly in the BVE and formula composition phases. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Detect and simplify OR(TRUE,x)=TRUE, OR(FALSE,x)=x at the formula level. Avoids creating unnecessary fresh variables and clauses when one operand is a trivial constant. This triggers during BVE and initial formula construction. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Detect and simplify AND(FALSE,x)=FALSE, AND(TRUE,x)=x at the formula level. Avoids creating unnecessary fresh variables and clauses when one operand is a trivial constant. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
For moderately hot variables (10-30 repairs), do only 1 extra minimization pass instead of 2. Reserve 2 extra passes for very hot variables (30+ repairs) where the investment in finding smaller conflicts has the highest payoff. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
When one branch of compose_ite is a constant TRUE or FALSE, the ITE can be simplified: ITE(b,TRUE,x)=OR(b,x), ITE(b,FALSE,x)=AND(!b,x), ITE(b,x,TRUE)=OR(!b,x), ITE(b,x,FALSE)=AND(b,x). This creates flatter formulas with fewer clauses than the full 4-clause ITE encoding. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
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
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.
No description provided.