GitLab

I am seeing a strange issue with solving a PBO problem using SAT4J: version NIGHTLY.v20151101

Attached are 2 opb files: min-nonbuggy.opb and min.opb

Differences between the files: Both files differ from line 18 onwards. "min.opb" is an extension of min-nonbuggy.opb. Note that both files have same objective function that needs to be minimized.

The first file ("min-nonbuggy.opb") returns correct answer with optimum value as "4" with x12=0, x14 = 0 and x17=0. I agree with this answer. I also verified this by manually solving the constraints and objective function.

The second file ("min.opb") returns answer with optimum value as "5" with x12=1, x14=0 and x17=0. I think this is wrong.

(I am interested in values that appear in objective function only)

This is quite surprising given that - no additional constraint involving "x12" appears in "min.opb". So x12 should be 0 regardless of value of x17. Isn't it? Why is the answer returned as x12=1?