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!