hakank
For some example of the available predicates in the bp module, see my http://hakank.org/picat/v3_utils.pi . Also, see http://hakank.org/picat/#v3 for some examples of ported Prolog programs.
But one of its drawbacks is its limitation of handling input and output (including preprocessing and postprocessing). In some cases - for example when the output is rather simple - I use for example Picat/Python to transform input to MiniZinc format (.dzn format or JSON) and then run MiniZinc.
But for more fancy output I tend to use Picat or Python + (OR-tools CP/SAT or CPMpy or minizinc-python).
That being said, one can do fancier output in MiniZinc, though it requires some work. Here is a model for certain scheduling problems which exemplifies this: http://hakank.org/minizinc/scheduling_with_assignments.mzn . But the output was a little easier to do in Picat: http://hakank.org/picat/scheduling_with_assignments.pi
For non linear models:
* Gecode (included in the MiniZincIDE distribtion)
* JaCoP (https://github.com/radsz/jacop)
* OptiMathSAT (https://optimathsat.disi.unitn.it/pages/fznreference.html)
For linear models:
* CBC (included in the MiniZincIDE distribution)
""" CP-SAT is a discrete optimization solver built on top of a SAT engine. It is available within the OR-Tools open-source repository (website: https://developers.google.com/optimization, github repository: https://github.com/google/or-tools). It has won multiple gold medals at the MiniZinc challenge (https://www.minizinc.org/challenge.html) since its debut in 2017.
The CP-SAT solver is architectured around five components: The base layer is a clause learning SAT solver. Above the SAT layer sits a Constraint Programming (CP) module with Boolean, integer and interval variables, and standard integer, scheduling and routing constraints. Alongside the CP solver, a simplex provides a global linear relaxation. Its integration with the CP and SAT layers enable the CP-SAT solver to solve MIP problems with the same techniques as (commercial) MIP solvers: relaxation, cuts, heuristics and duality based techniques. Both the CP and MIP modules rely on a unified protobuf representation of the model that can serve as a file format, as well as an intermediate representation of the model during all phases of the solve (input format, presolved model, LNS fragment). On top, the search layer implements a robust information-sharing portfolio of specialized workers that offers both good and fast solutions, and superior optimality proving capabilities.
This work was presented at the CPAIOR 2020 masterclass. The recording is available on youtube (https://www.youtube.com/watch?v=lmy1ddn4cyw). """
Here are some other constraint modelling implementations of this problem: http://hakank.org/common_cp_models/#einavpuzzle .
I agree that 1,5,9,4,8,3,7,2,6 pattern rotations is there somewhere, either in the columns or the rows of a solution, but that don't make all solutions the same.
Though, of these 9 solutions there are more similarities, i.e. some of them are the same rows except that the positions are switched.
Some other thing. if the lines are sorted, there are only 4 distinct variants.
Also, the solution of the original Miracle Sudoku instance has some invariants, for example the rows are rotations of these numbers 1,5,9,4,8,3,7,2,6 and the columns are (when rows are sorted) rotations of the numbers 1..9.
I've added comments about this in my Picat model: http://hakank.org/picat/miracle_sudoku.pi
(Also: Thanks for your links to my site.)
The page also includes some SetlX programs.
http://hakank.org/common_cp_models/ is a page which collects models that solve the same problem in different CP systems (and mostly with the same approach). It can be used to compare similarities and differences between systems, though one have to do the comparison oneself.
A long time ago (in 2012) I did a talk on comparing features in different CP systems mostly focused how "easy" - subjectively and IMHO - it was to learn the systems: http://hakank.org/constraint_programming/sweconsnet_talk_201...
Some solvers, e.g. Gecode and JaCoP, can handle nonlinear problems with floats as well as finite-domain problems.