feat(pumpkin-proof-processor): Minimising number of deductions in trimmed proof by giving marked deductions higher propagation priority

[MatvV04]

Closes #432

Short summary of changes

1. The propagation priority of DeductionPropagators that have been marked on the nogood_stack is set to a higher priority than their unmarked counterparts (also see diagram below).
2. Every DeductionPropagator now performs either conflict detection XOR unit propagation. This is done to implement staged propagation where we first check whether any unmarked deduction could be used for declaring a conflict before proceeding to use the unmarked deductions for unit propagation.
3. Small fix in explain_predicates to prevent including duplicate inferences for the same predicate in one proof stage. This was taken from my team's CS4535 implementation, so I was not the one to come up with it.
4. Added two new Priority levels to the PropagatorQueue to allow for the two stages of unmarked deductions to be propagated after all model constraints and marked deductions. I have briefly considered to edit the priorities of all other propagators, but as the unmarked deductions need two separate propagation levels, that would result in setting the priority of all propagators to either Priority::High or Priority::Medium, which is likely not desirable.

Diagram of Propagation Priority

Preliminary results

I ran the implementation against main (with the fix from point 3 above, as main otherwise runs out of memory very quickly on my machine) on the scaffolds I got from @maartenflippo. I did run into some issues where the pumpkin-proof-processor throws an error on test-scheduling_t20m10r10-17, though this can be replicated on main so it is not because of the changes in this PR (opened an issue for it #527). Additionally, the checker does not accept the proof given for test-scheduling_t50m20r10-17, which I am currently investigating (on main this instance runs out of memory, so this could also be unrelated to the changes in this PR). Another smaller instance that shows a similar problem is Unit-Commitment_L10-T48G10L10 for which I opened an issue #528.

The following results have been checked using the pumpkin-checker (instances which timed out or contained only a single proof stage in both are omitted):

Instance	#Proof stages with scaffold minimisation	#Proof stages without scaffold minimisation (main)
ccmcp_3_20_0_15_3	96	102
ctw_A046	711	710
efm_cstr_MODEL1507180022	6434	7890
foxgeesecorn_foxgeesecorn_61	1290	1517
graph-scan-revised_rnd_n40_p1000_c20_s1	485	488
handball_handball9	45832	46529
harmony_canon	1018	1018
hoist-benchmark_PU_2_8_4	25	25
monitor_1id_hop_counting_based_zoo_Forthnet	697	775
SPECK-Optimisation_easy_1	3	3
TableLayout_p2000_m10_r500_c20	1090	1136
triangular_n11	8943	8936
triangular_n31	4046	4311
ttp_n20_k15_c5000_l100_u200_r32	15539	17328
ttp_n20_k20_c1000_l1000_u2000_r46	3	3
vrplc_service_vrplc10_5_20_s3	74	77
yumi-dynamic_p_4_GG_GG_yumi_grid_setup_5_5_zones	3891	3900

If additional benchmarking/checking is desirable, please let me know!

[maartenflippo]

This is really good work, and the results indicate that it is worth doing. Thank you for the contribution. I have one design comment and one code-style comment.

The design comment concerns the processor's memory usage. It is not very optimised at the moment, but this change effectively duplicates the memory used by deductions, since we post two propagators per nogood. I think in this case it makes sense to Rc the predicate slice, so that the conflict checker and the propagation propagator can simply read the same instance of the nogood.

The code-style comment relates to every occurrence where the propagators are modified. There is some duplication in the following pattern:

self.state.get_propagator_mut(conflict_checker_handle).expect(...)
self.state.get_propagator_mut(propagation_handle).expect(...)

Instead, we could add an associated method PostedDeduction::get_propagators_mut(&mut State) -> [&mut DeductionPropagator; 2] that pulls out that pattern, and allows more concise modification of the propagators. Other patterns may also work, but it is worth exploring briefly. If you think it does not significantly impact code quality, you can also ignore it.

[MatvV04]

Thank you for the review!

I added the requested changes:

1. Rc'ed the predicates in the DeductionPropagators and also on the nogood_stack. I ran one small instance using Valgrind's DHAT and the peak memory usage was about 5% lower. I suspect that bigger gains could be made if a DeductionPropagator could be popped from the PropagatorStore (should in theory be possible due to the order in which DeductionPropagators are added and deactivated).
2. Refactored the propagator deactivation / priority updating. I chose to add a method KeyedVec::get_disjoint_mut, please do take a good look at especially PropagatorStore::get_propagators_mut as it is arguably the least clean part of the refactoring. I could also change the implementation to just make repeated calls to get_propagator_mut.

[maartenflippo]

I think the get_propagators_mut on State is not ideal. Let's not make changes to State here.

[ImkoMarijnissen]

Thank you for making this PR, I have some small (mostly stylistic) comments!

I will leave it to @maartenflippo to approve the PR.

[ImkoMarijnissen]

Thank you for all of the changes!

I have some final comments, but other than that it looks good to me.