Details

    • Type: Bug Bug
    • Status: Resolved
    • Priority: Major Major
    • Resolution: Fixed
    • Affects Version/s: 2.3.0
    • Fix Version/s: 2.3.1
    • Component/s: maxsat
    • Security Level: Public (Everybody can see)
    • Labels:
      None
    • Environment:
      MacOSX

      Description

      When solving PMaxSAT problems, if there is no soft clause, the method isSatisfiable() works fine, i.e. it returns true, but the method model() throws a IllegalStateException even if there is a solution. I thought that the MaxSAT solver would behave exactly like MiniSATSolver when there is no soft clause but seems not.

      Moreover, the ModelIterator is used to iterate over models obtained from any SAT (e.g. MiniSAT or MaxSAT) solver. I think this requires a special attention in the case of MaxSAT solving...

      I attached an automatically generated CNF file for testing purposes although it seems easy to regenerate the problem.

      1. test.cnf.rtf
        0.4 kB
        Updateme Updateme

        Activity

        Hide
        Updateme Updateme added a comment -

        reset() method on solvers is now corrected.
        But a call to newVar(int howmany) method is mandatory after a call to reset().

        Show
        Updateme Updateme added a comment - reset() method on solvers is now corrected. But a call to newVar(int howmany) method is mandatory after a call to reset().
        Hide
        Daniel Le Berre added a comment -

        Anne, since you found the origin of the first maxsat bug, here is another one that might be related.

        Show
        Daniel Le Berre added a comment - Anne, since you found the origin of the first maxsat bug, here is another one that might be related.
        Hide
        Updateme Updateme added a comment -

        WeightedMaxSat solver should answer correctly now, problem has been solved. Thank you, Fatih, for the test case.

        Show
        Updateme Updateme added a comment - WeightedMaxSat solver should answer correctly now, problem has been solved. Thank you, Fatih, for the test case.
        Hide
        Daniel Le Berre added a comment -

        Fatih, can you confirm that Anne's changes do fix your issue? I would like to resolve it if it is the case

        Show
        Daniel Le Berre added a comment - Fatih, can you confirm that Anne's changes do fix your issue? I would like to resolve it if it is the case
        Hide
        Updateme Updateme added a comment -

        Based on my tests, yes it seems working. However more detailed tests will reveal the result

        Show
        Updateme Updateme added a comment - Based on my tests, yes it seems working. However more detailed tests will reveal the result
        Hide
        Updateme Updateme added a comment -

        Sorry my mistake as this issue involves two problems I reported. The problem with reset() seems persisting for the MaxSAT case. I use OptToSATAdapter and WeightedMaxSatDecorator but newVar method over the decorator produces strange results. For instance, the following code:
        resetSolver();
        System.out.println("VAR NUMBER FUNCTION BEFORE " + maxSATSolver.nVars());
        System.out.println("VAR NUMBER Parameter " + varNumber);
        maxSATSolver . newVar ( varNumber );
        maxSATSolver . setExpectedNumberOfClauses ( hardClauses.length + (softClauses == null ? 0 : softClauses.length));
        System.out.println("VAR NUMBER FUNCTION " + maxSATSolver.nVars());

        gives me

        VAR NUMBER FUNCTION BEFORE 0
        VAR NUMBER Parameter 62
        VAR NUMBER FUNCTION 404

        I think there is something wrong happening here.

        Show
        Updateme Updateme added a comment - Sorry my mistake as this issue involves two problems I reported. The problem with reset() seems persisting for the MaxSAT case. I use OptToSATAdapter and WeightedMaxSatDecorator but newVar method over the decorator produces strange results. For instance, the following code: resetSolver(); System.out.println("VAR NUMBER FUNCTION BEFORE " + maxSATSolver.nVars()); System.out.println("VAR NUMBER Parameter " + varNumber); maxSATSolver . newVar ( varNumber ); maxSATSolver . setExpectedNumberOfClauses ( hardClauses.length + (softClauses == null ? 0 : softClauses.length)); System.out.println("VAR NUMBER FUNCTION " + maxSATSolver.nVars()); gives me VAR NUMBER FUNCTION BEFORE 0 VAR NUMBER Parameter 62 VAR NUMBER FUNCTION 404 I think there is something wrong happening here.
        Hide
        Daniel Le Berre added a comment -

        There is nothing wrong: the WeightedMaxSatDecorator creates one new variable per constraint, so it is to be expected that the number of allowed variables is growing in the solver. You can check this by asserting that the VAR NUMBER FUNCTION value is equals to VAR NUMBER + expected number of clauses.

        Show
        Daniel Le Berre added a comment - There is nothing wrong: the WeightedMaxSatDecorator creates one new variable per constraint, so it is to be expected that the number of allowed variables is growing in the solver. You can check this by asserting that the VAR NUMBER FUNCTION value is equals to VAR NUMBER + expected number of clauses.
        Hide
        Daniel Le Berre added a comment -

        Closing. The last remark is not a bug, it is a feature

        Show
        Daniel Le Berre added a comment - Closing. The last remark is not a bug, it is a feature

          People

          • Assignee:
            Updateme Updateme
            Reporter:
            Updateme Updateme
          • Votes:
            0 Vote for this issue
            Watchers:
            1 Start watching this issue

            Dates

            • Created:
              Updated:
              Resolved:

              Development