From f7370466f0fa2f6a3dd924c730ffe446f6ffb5bb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 18:51:38 -0700 Subject: [PATCH] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index a60266a50..797f5584f 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -282,12 +282,14 @@ Ideas for other knobs that can be tested
  • Replace backoff scheme by a geometric scheme: add conflict_inc (a new parameter) every time and increment conflict_inc.
  • Revert backoff if a cube is solved.
  • Delay lemma and unit sharing.
  • +
  • Vary max_cube_size, or add a parameter to grow max_cube_size if initial attempts to conquer reach max_conflicts.
  •    cube_initial_only (bool) (default: false)          only useful when never_cube=false
       frugal_cube_only (bool) (default: false)           only useful when never_cube=false
       max_conflict_mul (double) (default: 1.5)
    +  max_cube_size (unsigned int) (default: 20)         only useful when never_cube=false
       never_cube (bool) (default: false)
       relevant_units_only (bool) (default: true)         only useful when share_units=true
       share_conflicts (bool) (default: true)             only useful when never_cube=false