From a5c9e370def01111ddfa17966791b14d8238bf63 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 17 Aug 2025 18:08:23 -0700 Subject: [PATCH] Update PARALLEL_PROJECT_NOTES.md --- PARALLEL_PROJECT_NOTES.md | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/PARALLEL_PROJECT_NOTES.md b/PARALLEL_PROJECT_NOTES.md index 00ec087b4..a60266a50 100644 --- a/PARALLEL_PROJECT_NOTES.md +++ b/PARALLEL_PROJECT_NOTES.md @@ -275,11 +275,13 @@ threads-4-cube-shareconflicts Ideas for other knobs that can be tested -
  • Only cube on literals that exist in initial formula. Don't cube on literals created during search (such as by theory lemmas). -
  • Only share units for literals that exist in the initial formula. -
  • Vary the backoff scheme for max_conflict_mul from 1.5 to lower and higher. -
  • Vary smt.threads.max_conflicts -
  • Replace backoff scheme by a geometric scheme: add conflict_inc (a new parameter) every time and increment conflict_inc +
  • Only cube on literals that exist in initial formula. Don't cube on literals created during search (such as by theory lemmas).
    • +
  • Only share units for literals that exist in the initial formula.
    • +
  • Vary the backoff scheme for max_conflict_mul from 1.5 to lower and higher.
    • +
  • Vary smt.threads.max_conflicts.
    • +
  • 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.
    •