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

OptToPBSATAdapter does not always return an optimal solution

    Details

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

      Description

      The OptToSATAdapter and OptToPBSATAdapter allow the end user to compute an optimal solution with a simple call to isSatisfiable() using the decorator design pattern.

      That class actually compute the optimal model (using a loop on admitABetterSolution()) in the model() method.

      Such feature has been available for a while.

      However, we introduced in Sat4j 2.3.1 a method called modelWithInternalVariables() to retrieve a model from the solver with possibly extra variables that could have been introduced in the solver (the maxsat decorator for instance).

      As such, if a procedure calls modelWithInternalVariable() on an OptToPBSATAdapter instead of model(), the optimization part is not carried out, and a non optimal solution is returned.

      This is the case of the FullClauseSelector class introduced in Sat4j 2.3.3, thus the Xplain class.

      So someone decorating an OptTo[PB]SATAdapter with an Xplain[PB] object may not obtain an optimal solution.

      This is what happens in the DependencyHelper class if the explanation is enabled.

      The current workaround is to call model() before modelWithInternalVariables() to get an optimal solution.

      Note that in the upcoming 2.3.4 release, the optimization is performed on the "isSatisfiable()" method, which solves the issue.

        Activity

          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: