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.
    •