Replies (2)

• @edinbruh@feddit.it 2026-09-20 21:35

  I think a “constraint propagation” based solver should work well. So you can try using minizinc and play with the solvers it gives you. Using gecode and heuristics it can get very fast (try using relax_and_reconstruct, together with restart_luby and indomain_random, to obtain a simple LNS. Or you can use Google’s OR tools solver, that is based on ILP and is very fast, and can run multithreaded. You can also go fully ILP, and model your problem in ampl, and try some free (e.g. glpk) or commercial (e.g. gurobi) ILP solver. I doubt it helps, but there’s always SMT solvers (e.g. cvc5), which I don’t think can be faster but is surely easier to model than a pure SAT. And there’s also ASP solvers like clingo (clasp+gringo), that are purely logic based and implement common-sense-reasoning.

  Open ##4784362

• @edinbruh@feddit.it 2026-09-23 19:45

  Well? How did it go?

  Open ##4822047