20230415 rayon parallel propagation

[shnarazk]

• separate check and perform
• rename PropagationContext to ClauseTransformer; then we have to make an entry point to ClauseDB that takes a ClauseTransformer???
• collect transformers in parallel, then execute them under an immutable context sequentially
• revise to the new IF
• refactor check_in debug codes

Wow!!! It's getting slow!

I found Rayon was not good for this. I need something better.

The first idea

• current implementation

for watch in &mut watchlist {
  check_another_watcher()?;
}

• (watchlist-level) parallel propagate

let bucket = watchlist[lit].into_par_iter().map(|w| seek_another_watcher(self: &AssignStack));
if bucket.iter().any(conflicting) {
   return Conflict();
)
for (cid, to) in bucket.iter().map(|p| p.unwrap()) {
   watchlist[to].push(cid);
}
watchlist[lit].clear();

a problem caused by inappropriate evaluation assumption

A new assignment (implication) modifies the checking context. We have to purge the remains and rebuild them.

'new_context: while start < watch_list.len() {
  // parallel part
  let transformers = watch_list[start..start+bucket_size].iter().map().collect();
  // sequential part
  let mut processed = 0;
  for (i, transformer) in transformers.iter() {
     processed += 1;
     ...
     if got_new_assign {
        start = i + 1;
        continue 'new_context;
     }
  }
  start += processed;
}

[shnarazk]

🐛 This function reorders the items in the watchlist by calling swap_remove! 🐛

[shnarazk]

So we have to

1. build a new list during the iteration, then swap to the original.
2. execute in-place shrinking, then resize after the iteration
3. use $O(n)$ remove