Uploaded image for project: 'Sat4j'
  1. Sat4j
  2. SAT-32

Tautological PB constraints with no literals incorrectly considered asempty clauses

    Details

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

      Description

      When creating PB constraints with no literal and a degree of 0 or -1 for instance, the solver launches a contradiction exception while it should just ignore those constraints.

      This is particularly annoying when doing optimization.

        Activity

        Hide
        leberre Daniel Le Berre added a comment -

        Created a testcase, BugSAT32, to show the issue in both normal simplification mode and in competition mode.

        Show
        leberre Daniel Le Berre added a comment - Created a testcase, BugSAT32, to show the issue in both normal simplification mode and in competition mode.
        Hide
        leberre Daniel Le Berre added a comment -

        Fixed in r976

        Show
        leberre Daniel Le Berre added a comment - Fixed in r976

          People

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

            Dates

            • Created:
              Updated:
              Resolved: