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

Allow the solver to be aware of the user defined max var id

    Details

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

      Description

      When using SAT encodings, it is often necessary to create new variables on the fly.
      This is true for instance in the translation from MaxSAT to PBO, from Card to SAT, etc.

      In that context, it is important to make a difference between the original max var id
      and the maxvarid after adding the new variables.

      It is assumed in most cases in Sat4j that the user defined maxvarid is defined using the method
      ISolver.newVar(int maxvarid)

      Then new variables can be retrieved using nextFreeVarId().

      We could for instance fix the value set using newVar() and add a method to retrieve it.

      That way, the model iterator for instance could use that value instead of the current nVar().

        Activity

        Hide
        leberre Daniel Le Berre added a comment -

        Implemented in r1073.
        The main compatibility break with previous code is when the user did not make a call to newVar() before entering the constraint.

        The model() method would return in that case an empty model. A call to modelWithInternalVariables() is thus necessary to retrieve the model.

        I have no solution now to preserve the compatibility.

        Possibilities are:

        • in model() method, when the model is empty, return full model.
        • detect in some ways that newVar() has not been called and no nextFreeVarId() has been called, thus consider usermaxvarid = voc.maxvarid.
        • other?
        Show
        leberre Daniel Le Berre added a comment - Implemented in r1073. The main compatibility break with previous code is when the user did not make a call to newVar() before entering the constraint. The model() method would return in that case an empty model. A call to modelWithInternalVariables() is thus necessary to retrieve the model. I have no solution now to preserve the compatibility. Possibilities are: in model() method, when the model is empty, return full model. detect in some ways that newVar() has not been called and no nextFreeVarId() has been called, thus consider usermaxvarid = voc.maxvarid. other?
        Hide
        leberre Daniel Le Berre added a comment -

        Fix the backward compatibility issue: nVars() returns the number of variables in the solver when newVar() has not been called.

        Show
        leberre Daniel Le Berre added a comment - Fix the backward compatibility issue: nVars() returns the number of variables in the solver when newVar() has not been called.
        Hide
        leberre Daniel Le Berre added a comment -

        Will ship in 2.3.1.

        Show
        leberre Daniel Le Berre added a comment - Will ship in 2.3.1.

          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: