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

Allow iterating over optimal solutions

    Details

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

      Description

      The solver is not properly cleaned up once an optimal solution is found.
      Literals propagated at decision level 0 by pseudo boolean constraints used during the optimization are not properly removed.

      While this does not affect our major tools (PB or MAXSAT solvers) since they aim only at finding one optimal solution, it is an issue when one wants to find several optimal solutions. See TestLonca to see the problem in action.

        Activity

        Hide
        leberre Daniel Le Berre added a comment -

        That issue becomes critical to be able to do lexico optimization on weighted optimization functions (i.e. in p2cudf).

        Show
        leberre Daniel Le Berre added a comment - That issue becomes critical to be able to do lexico optimization on weighted optimization functions (i.e. in p2cudf).
        Hide
        leberre Daniel Le Berre added a comment -

        That issue is our show stopper for release 2.3.1. Need to be fixed ASAP.

        Show
        leberre Daniel Le Berre added a comment - That issue is our show stopper for release 2.3.1. Need to be fixed ASAP.
        Hide
        leberre Daniel Le Berre added a comment -

        Added a potential fix in r1084 for MaxWatchPb constraints. Need to be adapted to MinWatch too.

        Show
        leberre Daniel Le Berre added a comment - Added a potential fix in r1084 for MaxWatchPb constraints. Need to be adapted to MinWatch too.
        Hide
        leberre Daniel Le Berre added a comment -

        Fixed the last issue in r1092.

        Show
        leberre Daniel Le Berre added a comment - Fixed the last issue in r1092.
        Hide
        leberre Daniel Le Berre added a comment -

        The fix breaks 15 tests cases on our functional tests!!!!

        Show
        leberre Daniel Le Berre added a comment - The fix breaks 15 tests cases on our functional tests!!!!
        Hide
        leberre Daniel Le Berre added a comment -

        We need to check if Minimal4CardinalityModel class is affected or not by such issue.

        Show
        leberre Daniel Le Berre added a comment - We need to check if Minimal4CardinalityModel class is affected or not by such issue.
        Hide
        leberre Daniel Le Berre added a comment -

        That issue has been fixed thanks to the code used to fix SAT113 (and SAT110).

        Show
        leberre Daniel Le Berre added a comment - That issue has been fixed thanks to the code used to fix SAT113 (and SAT110).

          People

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

            Dates

            • Created:
              Updated:
              Resolved: