Sat4j
  1. Sat4j
  2. SAT-16

Order of added constraints affects the results of RemiUtils

    Details

    • Type: Bug Bug
    • Status: Resolved
    • Priority: Critical Critical
    • Resolution: Duplicate
    • Affects Version/s: 2.3.0
    • Fix Version/s: 2.3.1
    • Component/s: pseudo
    • Security Level: Public (Everybody can see)
    • Labels:
      None

      Description

      The order in which the pseudo boolean constraints are added to the solver affects the result of RemiUtils which should not be the case in my opinion. I found out that the constraint that will be added at first causes the problem. If this constraint is added later, the expected result will be returned ("4,5,6"). Otherwise RemiUtils.backbone() returns "4,5" which is obviously wrong because the constraint "+1 x6 >= 1" requires literal 6 to be true in all satisfying assignments.

      • Sebastian

        Activity

        Hide
        Daniel Le Berre added a comment -

        Hi Sebastian,

        Thanks for pointing that out. It is probably a problem due to constraints simplification (In your case, the solver ignores constraints containing 6 and removes constraints containing -6). I will take a look asap.

        Regarding your testcase. Why don't you use simply addClause() instead of addPseudoBoolean()? It would allow you to save the code for managing coefficients (always one) and the degree (also always one).

        Show
        Daniel Le Berre added a comment - Hi Sebastian, Thanks for pointing that out. It is probably a problem due to constraints simplification (In your case, the solver ignores constraints containing 6 and removes constraints containing -6). I will take a look asap. Regarding your testcase. Why don't you use simply addClause() instead of addPseudoBoolean()? It would allow you to save the code for managing coefficients (always one) and the degree (also always one).
        Hide
        Daniel Le Berre added a comment -

        I cannot reproduce in HEAD.

        Show
        Daniel Le Berre added a comment - I cannot reproduce in HEAD.
        Hide
        Daniel Le Berre added a comment -

        I confirm the problem in 2.3

        Show
        Daniel Le Berre added a comment - I confirm the problem in 2.3
        Hide
        Daniel Le Berre added a comment -

        This is a consequence of bug SAT-17.

        Show
        Daniel Le Berre added a comment - This is a consequence of bug SAT-17 .
        Hide
        Updateme Updateme added a comment - - edited

        Bug does not occur in HEAD. Thanks!

        Show
        Updateme Updateme added a comment - - edited Bug does not occur in HEAD. Thanks!

          People

          • Assignee:
            Daniel Le Berre
            Reporter:
            Updateme Updateme
          • Votes:
            0 Vote for this issue
            Watchers:
            1 Start watching this issue

            Dates

            • Due:
              Created:
              Updated:
              Resolved:

              Development