perf(pkg): make SAT decision search incremental

[Alizter]

Summary

This separates the SAT contract from the two optimizations:

1. Expose the decision level and test that an incremental decider observes a decrease after non-chronological backtracking. This commit passes before either performance change.
2. Track undecided SAT variables in a linked list instead of rescanning every variable.
3. Resume the package solver's depth-first decision traversal between decisions, resetting it when the tested decision-level signal shows a backtrack.

SAT-event speedup

Across ten real-world projects, complete sat/solve trace events were 2.83× faster by geometric mean for the four-platform solve and 2.80× faster for a single-platform solve. Every project improved in both configurations.

These numbers measure time inside sat/solve, not end-to-end dune pkg lock time. Each cell uses 10 measured runs after 2 warmups, with baseline and PR runs interleaved. Irmin was rerun with 20 measured runs after 3 warmups, pinned to a performance core with a 3 GHz preflight and median-frequency gate, because the original thermally throttled samples had excessive variance.

Per-project benchmark results

Four-platform solve

Project	Main mean ± SD (s)	PR mean ± SD (s)	Speedup
re	0.025557 ± 0.006168	0.011155 ± 0.002417	2.291×
cohttp	0.547998 ± 0.087835	0.142115 ± 0.019302	3.856×
jsoo	0.098637 ± 0.012977	0.029679 ± 0.004315	3.323×
lsp	0.171643 ± 0.020435	0.052369 ± 0.007763	3.278×
opam	0.050597 ± 0.007468	0.019356 ± 0.002736	2.614×
irmin	0.113493 ± 0.002821	0.036411 ± 0.001870	3.117×
mirage	0.013849 ± 0.002458	0.004736 ± 0.001849	2.924×
eio	0.010773 ± 0.001951	0.003753 ± 0.001668	2.871×
owl	0.010737 ± 0.001849	0.005824 ± 0.002847	1.843×
tezos	0.029278 ± 0.002267	0.010965 ± 0.001481	2.670×

Single-platform solve

Project	Main mean ± SD (s)	PR mean ± SD (s)	Speedup
re	0.002231 ± 0.000204	0.001117 ± 0.000051	1.998×
cohttp	0.019991 ± 0.000986	0.004335 ± 0.000474	4.612×
jsoo	0.002132 ± 0.000203	0.000899 ± 0.000112	2.372×
lsp	0.004384 ± 0.000243	0.000859 ± 0.000078	5.105×
opam	0.000492 ± 0.000128	0.000241 ± 0.000030	2.041×
irmin	0.052453 ± 0.000707	0.009705 ± 0.000190	5.405×
mirage	0.002342 ± 0.000074	0.001174 ± 0.000192	1.994×
eio	0.001512 ± 0.000080	0.000733 ± 0.000117	2.061×
owl	0.001480 ± 0.000078	0.000749 ± 0.000084	1.976×
tezos	0.007892 ± 0.001320	0.002665 ± 0.000893	2.961×

Tests

• The decision-level/backtracking expect test passes before the performance commits
• dune build @check @fmt
• SAT expect and solver trace tests

[rgrinberg]

Make sure that this is reviewed by somebody that understands SAT