Detect all conflicts on Engine::check_solution

[Dekker1]

No description provided.

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Files with missing lines	Coverage Δ
crates/huub/src/solver/engine.rs	77.28% <ø> (ø)

... and 1 file with indirect coverage changes

---

🚨 Try these New Features:

• Flaky Tests Detection - Detect and resolve failed and flaky tests

[codspeed-hq]

CodSpeed Performance Report

Merging #137 will degrade performances by 65.8%

_{Comparing Dekker1:feat/check_sol_mult_conflict (405e001) with develop (4aa742b)}

Summary

⚡ 1 improvements
❌ 2 regressions
✅ 10 untouched benchmarks

⚠️ Please fix the performance issues or acknowledge them on CodSpeed.

Benchmarks breakdown

	Benchmark	develop	Dekker1:feat/check_sol_mult_conflict	Change
❌	optimization[jobshop_la02]	390.6 ms	694.5 ms	-43.77%
❌	optimization[jobshop_la03]	178.4 ms	521.5 ms	-65.8%
⚡	optimization[jobshop_la04]	400.9 ms	321.7 ms	+24.64%

[Dekker1]

@AllenZzw This was one of the changes that we discussed. It seems to affect the job shop benchmarks mostly negatively, but it's unclear to me whether this is just because of a different search order, and we are unlucky in 2 out of 3 changes. In general, giving more information back to the SAT solver with no change in runtime for check_solution would seem good.

Could you run a larger test suite to see whether this is worthwhile or not (independent of propagator deactivation)?

[AllenZzw]

The normal clauses in state.clauses and conflict clauses in state.conflict seems to be handled differently in add_external_clause. Shall we change the conflict variable into a vector to ensure the consistent handling of conflicts?

[Dekker1]

The difference is that state.clauses are persistent, and will be kept even when you backtrack. We could change conflict to be a vector and capture all conflicts immediately, but it would still require the move to state.clauses because we immediately backtrack afterwards in check_solutions. (Note that the other difference is that all other clauses and propagations are posted before the conflict, to ensure it will cause conflict in the SAT solver. However, since conflicts are added to the end of the list and there cannot be any propagations, this is not a problem).

So if we stick to my proposed design, where we detect all conflicts in check_solutions, but find only the first in propagate, then don't think we need to change it.

[AllenZzw]

I see. Probably the performance change is due to the search heuristic. Let me test it using a larger benchmark and also try the --vsids-only option.

[Dekker1]

That would be great! Thanks :)

[AllenZzw]

Tested with jobshop and openshop instances. The performance seems to remain the same.

[Dekker1]

If the performance is just the same, then I'm not sure whether the change is worthwhile.

Like we discussed in person: only one of the clauses is used in conflict resolution, so any other given clauses are added to the clause database “as is”. I'm not sure whether this wouldn't be something we would hope to avoid.

I'll at least make another branch that ensures that conflict clauses in check_solution are still added as “removable” clauses.