[jpnelson]

I wrote a thesis on using constraint satisfaction with minizinc to solve the genome edit distance problem: https://github.com/jpnelson/genome-edit/blob/master/thesis.p...

My takeaway: modeling problems in minizinc correctly is exceptionally difficult for non-trivial problems. You can model it correctly, but you'll likely still need to add additional "constraints" that improve the performance of the solver to the degree where it's even remotely usable to solve real problems.

It's a really interesting tool, but one of the reasons we thought it might be useful for this problem is so that non-technical people could easily change the constraints and play with the costs for different operations. I don't think it's particularly good for that, at least in this problem domain.

[jomoho]

I used minizinc to try and generate levels for my puzzle game by encoding the rules.

It worked quite well for the more trivial rules, but as I added more complex rules, it wouldn't solve within reasonable time.

Unfortunately I didn't really figure out how to direct the solver in way that would speed up things.

[zellyn]

Do I understand correctly that this kind of constraint satisfaction is more complex than just turning things into a bunch of SAT clauses? Otherwise (and admittedly without a deep understanding of genomics or solvers), I would be surprised if constraint satisfaction were the best approach for edit distance…

Once you added domain-specific performance-oriented constraints, did you find this to be a useful and viable approach to the problem?

[sirwhinesalot]

MiniZinc is just a modeling language, you can throw the problem at different solvers. You can use SAT solvers (assuming you have some wrapper that translates FlatZinc to CNF), CP solvers (can be SAT-based underneath or use different algorithms like MAC), SMT solvers (SAT Modulo Theories like Arithmetic), MIP solvers (usually Simplex + Branch & Bound)...

[aidos]

Is that a minizinc thing or a solver thing in general?

[shaunxcode]

https://en.wikipedia.org/wiki/Variety_(cybernetics)

key takeaway: Boisot and McKelvey updated this law to the "law of requisite complexity", that holds that, in order to be efficaciously adaptive, the internal complexity of a system must match the external complexity it confronts.

[riwsky]

“Inner platform effect”

[0cf8612b2e1e]

I have only ever used Z3, but you might be onto something. Modeling problems is really challenging. It does not help that if you search for documentation or guidance there one two types of resources: beginner Sudoku or primary literature academic papers discussing the minutia of optimization properties with so much jargon.

[sinuhe69]

How is MiniZinc in this aspect compared to Picat or other constraints solving languages?

I find the outputs command of MiniZinc particularly counter-intuitive and hard to use.

[hakank]

I really like MiniZinc, especially that one can test a lot of different type of solvers for a problem.

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