test(pkg): preserve single-platform SAT problem size

[Alizter]

Summary

• Add a trace-based regression for a lock directory with exactly one requested platform.
• Assert the exact SAT problem size for a fixed one-package input: two variables and two clauses.
• Guard against adding cross-platform consistency encoding to the single-platform path.

This is an independent test-only performance baseline for the joint-solver work in #15982.

Tests

• nix develop -c dune runtest test/blackbox-tests/test-cases/pkg/portable-lockdirs/portable-lockdirs-single-platform-sat-size.t
• CI=true nix develop -c dune build @fmt @check