Make literal picker break activity ties by picking smaller variable

[dewert99]

This makes literal picking somewhat more predictable and robust to the order explanations are given by theories (see https://github.com/dewert99/bat_egg_smt/pull/14). Unfortunately it seems this also makes maintaining the order heap more expensive so I'm planning to try to optimize before opening this PR.

[dewert99]

I've tried several optimizations:

• Caching activity levels in the heap
• Using f32 instead of f64
• Using a quaternary (4-ary) heap instead of a binary heap
• Using single u64 comparison instead of a f32 comparison that falls back to a u32 comparison if it is equal
  • This works because all the activity levels are positive so integer comparison is equivalent to floating point comparison.

I'm still not sure if these improvement are sufficient to negate the cost of the change, and some of these improvements could have been done regardless of whether we break ties using variables, although this new ordering scheme does give users more control over the literal picker in case they have extra information about which literals would be better to pick.

[dewert99]

I also reversed the order that Vars are processed in cancel_until which brought the performance back to about what it was before, although again that could also have been done using the old ordering scheme.

[dewert99]

I also notice that in this and some other my other recent PRs I used the let-else feature, so if/when you publish the next version to crates.io you should probably add rust-version = "1.65.0" to src/batsat/Cargo.toml

[c-cube]

Somewhat stupid question there, but could we sort the conflict before inserting things into the heap? That would make the actual order more resilient, I think?

[dewert99]

Somewhat stupid question there, but could we sort the conflict before inserting things into the heap? That would make the actual order more resilient, I think?

I think that would help with my original problem, although that may have some cost as well. Breaking ties with variable order also has the advantage of allowing users some control over the initial order. I think the main reason the original picker was so cheap was that it broke ties in a way to do the least amount of heapifying which was helpful when most variables had the same activity level, so these changes would also be helpful when randomizing the initial activity levels/