Details

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

      Description

      When forgetting to call newVar, explanations become wrong, since clauses are being added with wrong explanation keys.

      A more user-friendly solution would be to throw an exception when adding a clause with undeclared variables, instead of silently accepting the clause and returning incorrect results afterwards.

      Here is a working example:

      package test;

      import org.sat4j.core.VecInt;
      import org.sat4j.specs.ContradictionException;
      import org.sat4j.specs.IVecInt;
      import org.sat4j.pb.IPBSolver;
      import org.sat4j.pb.SolverFactory;
      import org.sat4j.pb.tools.XplainPB;
      import org.sat4j.tools.xplain.Xplain;

      class Test {
      public static void main(String[] args) throws ContradictionException

      { Xplain<IPBSolver> solver = new XplainPB(SolverFactory.newDefault()); IVecInt clause = new VecInt(); clause.push(-1).push(-2); System.out.println("adding clause " + clause.toString()); solver.addClause(clause); System.out.println("clause added as " + clause.toString()); }

      }

      The output of this program is as following:

      adding clause -1,-2
      clause added as -1,-2,1

      Here, literal "1" was used as an explanation key, which conflicts with the variable used in the clause.

      A workaround for the wrong explanations is to never forget to call newVar for all variables before adding any clauses.

        Activity

        Hide
        Daniel Le Berre added a comment -

        Hi Alexey,

        You are right, we should throw an illegal state exception here, to prevent that wrong behavior.
        The same issue exists for the MAXSAT tool.

        I will add two testcases for that.

        This will ship in 2.3.2 final.

        Thanks for pointing that out.

        Daniel

        Show
        Daniel Le Berre added a comment - Hi Alexey, You are right, we should throw an illegal state exception here, to prevent that wrong behavior. The same issue exists for the MAXSAT tool. I will add two testcases for that. This will ship in 2.3.2 final. Thanks for pointing that out. Daniel
        Hide
        Daniel Le Berre added a comment -

        Fix released in r1333.

        Show
        Daniel Le Berre added a comment - Fix released in r1333.

          People

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

            Dates

            • Created:
              Updated:
              Resolved:

              Development