Skip to content

Randomized simplifications - #896

Open
quickbeam123 wants to merge 6 commits into
masterfrom
randomized-simplifications
Open

Randomized simplifications#896
quickbeam123 wants to merge 6 commits into
masterfrom
randomized-simplifications

Conversation

@quickbeam123

Copy link
Copy Markdown
Collaborator

The same spirit as randomized preprocessing.

This "leaks" the core action for fd, fsr, bd, bsr and avatar under some small probabilities.

quickbeam123 and others added 6 commits August 5, 2026 11:30
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…lly drop a candidate rewrite early, giving a rewrite by another source (or none) a chance instead

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… occasionally drop an SR candidate early, in both the SAT-based and the code-tree implementation (proper subsumptions are never leaky)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…skip a splitting opportunity, leaving the clause in the FO loop unsplit (properly non-splittable clauses are never leaky)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…: occasionally drop an SR candidate early, with the same probability as in the forward variant (proper backward subsumptions are never leaky)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…ally drop a candidate rewrite as early as possible, with the same probability as in the forward variant

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant