RE: [Help-glpk] OPB output file anomaly

[Joey Rios]

Thanks for the reply Andrew.

> Did you try specifying the option '--wnpb' to write the instance in
> normalized opb format?
>

The PB SAT solver I am using (minisat+) doesn't seem to like the normalized input, but is (usually) happy with the --wpb file that glpsol creates.  I didn't look too deeply into this and just accepted that I could create an input file that works.  Based on the code in glplpx19.c, it doesn't look like producing normalized output will affect this issue, since I'd still get empty LHS in these inequalities.  I could verify this, but looking at the code, it is only a situation like this:

if(normaized) print("blah");
else print("foo");

And the fact k == 0 prevents this code from even firing in the empty LHS cases.


> > So it looks like I have some rows where all coeff's are zero.  I am
> > not sure how to interpret this.  When I manually remove all of these
> > inequalities from the OPB file, my PB SAT solver (minisat+) is happy
> > with the file, but produces the wrong solution (i.e. different from
> > the correct/expected result from glpsol).  So these inequalities are
> > probably necessary to obtain the correct solution.
>
> An empty row, i.e. the row having all coefficients zero, can be
> either redundant or infeasible only. In your instance all rows look
> redundant, so removing them from the instance must not affect the
> solution.
>
> Probably the opb format does not allow empty rows, so such rows
> should not be included in the output file.
>

What you are saying makes sense, but:

1.  glpsol correctly solves my model.
2.  The OPB file generated from this model has some inequalities with empty LHS's.
3.  Removing these incomplete inequalities results in a file accepted by minisat+, but produces an incorrect solution.
4.  Other OPB files generated by glpsol work as expected in minisat+ (with no empty LHS's).

So either minisat+ is bugged (which is possible, but seems like it is a good piece of software) or something odd is happening in glpk when producing my OPB file.  Or I am missing something very fundamental (which is probably the most likely option).

I'll probably hack some more print statements into lpx_write_pb() to see if it makes sense in my model to have those rows counted as redundant (with this particular data set, there are no infeasibility issues).

Any further thoughts/advice appreciated.
Joey

---

Need to know the score, the latest news, or you need your Hotmail®-get your "fix". Check it out.