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

OptToPBSATAdapter does not always return an optimal solution


    • Type: Bug
    • Status: Closed
    • 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:


      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.


        OW2 Atlassian Bamboo View RSS feed


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


            • Created: