MiniZinc / libminizinc

The MiniZinc compiler
http://www.minizinc.org
Other
508 stars 79 forks source link

counting solutions with Chuffed, missing -s in IDE #607

Closed dan1221 closed 1 year ago

dan1221 commented 2 years ago

I'm trying to count solutions using the MiniZinc IDE. This seems like a common desire when considering combinatorial objects. But the MiniZinc Handbook is strangely silent on the topic, except for Section 2.6.2. Effective Generators: "Imagine we want to count the number of triangles (K3 subgraphs) appearing in a graph," involving using "sum" to count true predicates by iterating over an integer range. But "sum" apparently isn't able to count solutions to global constraints, which typically involve a search space consisting of arrays, not just integer ranges.

The IDE Configuration Editor has a checkbox for "Output Solving Statistics". That works fine with the Gecode solver, but not with Chuffed. Unfortunately, Gecode is much slower than Chuffed on the models I've tried, so I can't use it on the larger models. Is there a way to get Chuffed to output the number of solutions?

Can "sum" be enhanced to iterate over an array, like global constraints, instead of just integer ranges?

Here's an example:

% count involutions, a permutation that equals its inverse; OEIS:A000085
include "inverse_fn.mzn"; 

int: n=10;
set of int: N = 1..n;
array[N] of var N: a;
constraint alldifferent(a);   

predicate equals_inverse(array[N] of var N: b) =  % involution 
let {array[N] of var N: c = inverse(b);} in b = c; 

constraint equals_inverse(a);
solve satisfy;

If we use "sum" to count involutions, we have to do some serious rearrangement of the above code, and it runs a lot slowerl

% count involutions, a permutation that equals its inverse; OEIS:A000085
include "inverse_fn.mzn"; 
include "arg_sort.mzn";

int: n;
set of int: N = 1..n;

predicate equals_inverse(array[N] of var N: b) =  % involution 
 alldifferent(b) /\ 
   let {array[N] of var N: c = arg_sort(b);} in b = c;  % had to switch to arg_sort instead of inverse

     var int: total =   % this is both awkward and inefficient
     if n==2 then
       sum(i,j in 1..n)(equals_inverse([i,j]))  
     elseif n==3 then
       sum(i,j,k in 1..n)(equals_inverse([i,j,k]))         
     elseif n==4 then
       sum(i,j,k,l in 1..n)(equals_inverse([i,j,k,l]))
     elseif n==5 then
       sum(i,j,k,l,m in 1..n)(equals_inverse([i,j,k,l,m]))
     elseif n==6 then
       sum(i,j,k,l,m,q in 1..n)(equals_inverse([i,j,k,l,m,q]))
     else 0
     endif;

   solve satisfy;

   output ["number of solutions is ", show(total)];
Dekker1 commented 2 years ago

Your initial solution would be the preferred MiniZinc way is to use the solution count as produced in the statistics.

There is a nSolutions statistic field that is produced by the MiniZinc driver, and thus is independent from the solver used. It seems, however, that there is currently an issue where the command line flag used by the IDE does not output this statistic. We will resolve this for the next MiniZinc release.

A workaround is to use the command line:

minizinc -a -s --solver chuffed model.mzn

which outputs %%%mzn-stat: nSolutions=9496 for your model.

Or, you can manually add the -s parameter using the "Add custom parameter" option in the IDE.

Screen Shot 2022-09-01 at 10 44 33
dan1221 commented 2 years ago

Yay!!!! The -s solved my problem of getting solution counts from Chuffed! Thank you!

I still have the separate issue that the solution counts apparently aren't available inside the model, when using global constraints. They are available when using "sum", but as you note, that isn't the preferred MiniZinc way.

I'd like the program to print out the first 10 or so terms of the sequence for OEIS:A000085:

1, 1, 2, 4, 10, 26, 76, 232, 764, 2620

But that doesn't work if the solution counts are only available in the IDE statistics, and only apply to one value of the parameter n.

dan1221 commented 1 year ago

Thanks!!

On 22.02.2023 20:42, Guido Tack wrote:

Closed #607 [1] as completed via 2e78416 [2].

-- Reply to this email directly, view it on GitHub [3], or unsubscribe [4]. You are receiving this because you authored the thread.Message ID: @.***>

Links:

[1] https://github.com/MiniZinc/libminizinc/issues/607 [2] https://github.com/MiniZinc/libminizinc/commit/2e78416acfe49d9bac780d522368c618c979fa24 [3] https://github.com/MiniZinc/libminizinc/issues/607#event-8587667506 [4] https://github.com/notifications/unsubscribe-auth/AUOVUCX5GYRYCR5BJYZ5U63WY3TEPANCNFSM6AAAAAAQBFAQ2Y