[gecode-users] Checking satisfiability of a Minizinc/Flatzinc model

[Jay]

Hi,

I have a Minizinc model, which I can easily convert into a Flatzinc 
model by running mzn2fzn. I am no expert with Gecode to begin with, and 
I only seem to be able to find the class reference for FlatZincSpace, 
and it doesn't seem helpful enough.

Following the documentation, I tried this (note that it requires a 
"file.fzn" Flatzinc model file to exist):

#include <iostream>
#include <gecode/flatzinc.hh>
#include <gecode/flatzinc/parser.hh>

using namespace Gecode;

int main()
{
     FlatZinc::Printer p;
     FlatZinc::FlatZincSpace* s = FlatZinc::parse("file.fzn", p);

     FlatZinc::FlatZincOptions opt;
     Support::Timer tot;

     s->run(std::cout, p, opt, tot);
}

Basically, I only care about a SAT/UNSAT result for my model. That is, I 
don't care how variables are assigned; just use the fastest solver you 
might have and tell me the output bit and I am happy. FWIW, all 
variables in my model are small integers.

The output of the above program is a listing of all variables with their 
domain, and a line consisting of dashes. I suspect there is some member 
function of FlatZincSpace to get a yes/no answer, but I cannot figure it 
out. Can someone push me in the right direction? Thank you!