Skip to content

Gecode 6.3.0 incorrectly thinks model is unsat #199

Open
Open
Gecode 6.3.0 incorrectly thinks model is unsat#199

Description

@Wout4
Wout4
opened on Apr 5, 2024

The following model returns 'unsatisfiable' when using Gecode 6.3.0, we can easily verify that it is satisfiable by using another solver, or by adding constraint p == false; after the other constraints.

var bool: p;
var 0..10: n_neg;
var 0..5: IV8708;
var 0..5: IV8709;
var 0..5: IV8710;
var bool: BV32799;
var bool: BV32800;
var bool: BV32801;
var bool: BV32798;
constraint (p) -> (((n_neg) div 2) < (true));
constraint (p) -> (((n_neg) div 2) < (true));
constraint (p) -> (((n_neg) div 2) < 1);
constraint not(((not((p) -> (((n_neg) div 2) < (true)))) + (not((p) -> (((n_neg) div 2) < (true))))) == 1);
constraint ((n_neg) div 2) == (IV8708);
constraint (p) -> ((IV8708) < 1);
constraint ((BV32799) + (BV32801)) != 1;
constraint ((p) /\ (BV32798)) == (BV32799);
constraint ((n_neg) div 2) == (IV8709);
constraint ((IV8709) >= 1) == (BV32798);
constraint ((p) /\ (BV32800)) == (BV32801);
constraint ((n_neg) div 2) == (IV8710);
constraint ((IV8710) >= 1) == (BV32800);
constraint ((not(((not((p) -> (((n_neg) div 2) < (true)))) + (not((p) -> (((n_neg) div 2) < (true))))) == 1)) + (not(((BV32799) + (BV32801)) != 1))) == 1;

solve satisfy;

Activity

  1. Wout4 commented on Apr 5, 2024

    @Wout4
    Wout4
    on Apr 5, 2024
    Author

    Found another smaller model with the same problem:

    var -3..5: x;
var -3..5: y;
var -3..5: z;
var 0..10: l;
var bool: p;
constraint not(((not(((not(((max([x,y,z])) < (l)) == (p))) + (not(((max([x,y,z])) < (l)) == (p)))) == 1)) + (((max([x,y,z])) < (l)) == (p))) == 1);
solve satisfy;

  2. zayenz commented on Apr 5, 2024

    @zayenz
    zayenz
    on Apr 5, 2024

    This is really interesting, and also quite scary. Thanks for creating a smaller example, and especially one that does not contain div (that is a partial function, and partiality and negation are tricky things to understand fully).

    I've checked the behavior as well, and it does seem to do something quite erroneous. OR-Tools solves it, as does HiGHS. OR-Tools gets the same FlatZInc output, so it should not be something that depends on Gecode-particular translations. I also translated using the HiGHS library to FlatZinc, and that model Gecode solves correctly.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions