A new paper shows how to write one constraint problem and hand it to five different solver types without rewriting anything.
Researchers built a modular waterfall framework in the open-source CPMpy library that translates a single high-level constraint model into the formats used by CP, SMT (QF-LIA), ILP, PB, and (Max)SAT solvers. The high-level language handles logical and arithmetic operations plus the global constraints CP practitioners rely on, like all-different or cumulative scheduling limits. Lower-level translations reuse the work already done for higher-level ones, so the SAT encoder builds on what the ILP encoder produced rather than starting from scratch. The team says two problems recur throughout: negating arbitrary sub-expressions cleanly, and keeping the number of extra auxiliary variables from ballooning.
Different solvers win on different problems, and until now testing several meant hand-remodeling the same problem for each paradigm's constraint vocabulary. That grunt work is exactly the kind of unglamorous plumbing that keeps researchers and engineers locked into whichever solver they learned first, rather than the one actually suited to their problem. The paper's own benchmarks show models change substantially as they pass through the pipeline, and that linearization choices for ILP and PB solvers aren't a minor detail but decide whether those solvers perform well at all.
It's an engineering paper, not a new algorithm. The real test is whether solver researchers actually adopt it as the default way to benchmark, rather than just adding another abstraction layer atop an already crowded solver ecosystem.