Eu estaria interessado em usar o MiniZinc por sua experiência no navegador e seu suporte a muitos solucionadores, mas ao mesmo tempo acho o CP-SAT (da OR-Tools) muito eficiente e gostaria de ter certeza de que, ao escolher usar o MiniZinc com o CP-SAT como backend, não perderei nada em comparação ao uso direto do CP-SAT.
Então aqui estão minhas perguntas: quão eficiente é a tradução MiniZinc -> CP-SAT? Tenho algum benefício em codificar coisas diretamente no CP-SAT? Se sim, posso, de alguma forma, fornecer instruções alternativas no MiniZinc, como uma especializada para CP-SAT e uma para qualquer backend genérico? Existe uma lista de restrições que são conhecidas por serem mais eficientes com CP-SAT diretamente em comparação com a tradução do minizinc?
Para dar um exemplo mais preciso, o CP-SAT tem muitas funções como "NoOverlap2D", "circuits", "AddReservoirConstraint"... mas sempre há uma restrição MiniZinc equivalente, e ela será compilada corretamente para o CP-SAT? Por exemplo, para o NoOverlap2D, parece que eu quero usar diffn, então se eu usar diffn, o CP-SAT usará o código NoOverlap2D otimizado por baixo dos panos, ou ele começará de um conjunto de instruções de nível mais baixo que pode ter mais dificuldade para otimizar?
Além disso, no desafio MiniZinc, o desempenho do CP-SAT é obtido por meio de um código escrito em MiniZinc ou diretamente por meio de um código otimizado para CP-SAT?
Para as restrições correspondentes, temos uma tradução direta.
Há muitas restrições no minizinco que não estão no CP-SAT e que são disponibilizadas através do mecanismo de expansão do Minizinco.
Sobre os benchmarks, eles foram obviamente executados usando o front-end minizinc.