Switch from Watch list and/or Dancing links to a complete bi-graph from Lit to Clause

[shnarazk]

It's time to ditch all the 2024 work!

No more reference updates. Clauses have no data about other clauses.

• if you can use a SIMD crate, progress == watch1 || progress == watch2 is cheap.

clauses_contain[propagating]
  .iter()
  .filter(|ci| clause[ci].watch1 == propagating || clause[ci].watch2 == propagating)
  .map(|ci| asg.propagate{&mut clause[ci], propagating))
  .fold(PropagationResult::Propagated, |acc val| acc.join(val));

or

clauses.par_iter_mut()
  .filter(|c| c.watch1 == propagating || c.watch2 == propagating)
  .map(|&mut c| c.propagate(propapating)  // Oh, c doesn't know its id.
  .fold(...)

Is this very slow even we can use rayon here?
Maybe you can't use rayon. propagate will update AssignStack.

But by switching to stage-based propagation from online propagation, the propagation process can be described as map-reduce iteration.

enum PropagationResult {
  Propagated(Vec<(Lit, ClauseId)>),
  Conflicting(Vec<(Lit, ClauseId)>),
}

clauses.par_iter_mut()
  .map(|&mut c| c.propagate(propagating)
  .fold(PropagationResult::Propagated(Vec::new()), merger);