Epic: SAT solver layer for domain-gap-aware clause learning

[lifebeyondfife]

Motivation

The current clause learning (CL) infrastructure uses a bounds-only propagation trail — it records lower-bound and upper-bound changes but cannot represent interior domain removals (gaps). This is sufficient for unary/binary constraints that only tighten bounds, but is fundamentally incompatible with global constraints like AllDifferent that perform arc consistency by removing individual values from within a domain's bounds.

As a workaround, AllDifferent operates at bounds consistency when CL is enabled. This is sound but weaker than full arc consistency.

Current state: benchmarks show CL adds 2–6x runtime overhead with no backtrack reduction on any tested problem (NQueens, RCPSP, FurnitureMoving). Before investing in the SAT solver layer, we need to understand why learned clauses aren't triggering unit propagation — i.e., whether the issue is clause quality (too many literals) or clause applicability (wrong problem structure).

Investigation phase (before implementation)

• Add clause quality diagnostics (Add clause learning quality diagnostics #159) — measure clauses learned, average clause size, unit propagations triggered, clause cache hit rate
• Tighten AllDifferent explanations (Tighten AllDifferent clause explanations via minimal Hall sets #160) — use minimal Hall sets instead of citing all N variables
• Evaluate whether tighter explanations alone yield backtrack reduction on any problem
• Identify or create a benchmark problem where CL demonstrably reduces backtracks

Only proceed with the SAT layer implementation if diagnostics confirm that domain gap support (not clause quality) is the bottleneck.

Implementation scope (contingent on investigation)

• Design a literal representation for interior domain values (e.g., x = v or x ≠ v)
• Implement a watched-literal SAT propagation mechanism for learned clauses involving domain gaps
• Extend the propagation trail to record interior removals with explanations
• Update ConflictAnalyser to resolve both bound literals and domain-gap literals during 1-UIP analysis
• Re-enable arc consistency for AllDifferent when CL is enabled
• Extend to other global constraints that perform interior removals (future)

References

• Ohrimenko, Stuckey, Codish — "Propagation via lazy clause generation" (2009)
• Chuffed lazy clause generation solver
• OR-Tools CP-SAT solver