Sat4j
  1. Sat4j
  2. SAT-17

Problem with isSatisfiable(VecInt)

    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: core
    • Security Level: Public (Everybody can see)
    • Labels:
      None

      Description

      ISolver.issatisfiable(VecInt) shows unexpected behavior.

      1. BugSAT17.java
        2 kB
        Daniel Le Berre
      2. Sat4JTest.java
        0.8 kB
        Updateme Updateme

        Activity

        Hide
        Daniel Le Berre added a comment -

        The problem is due to an inconsistency in the solver state once a call with inconsistent assumptions is performed (see new test case, attached, also in head). working on a workaround.

        Show
        Daniel Le Berre added a comment - The problem is due to an inconsistency in the solver state once a call with inconsistent assumptions is performed (see new test case, attached, also in head). working on a workaround.
        Hide
        Daniel Le Berre added a comment -

        The problem was in the analyzeFinalConflictInTermsOfAssumptions() introduced in Sat4j 2.2: it was removing unit literals from the solvers. The issue has been fixed on HEAD in r938.
        I let the bug open until I get your feedback.

        Show
        Daniel Le Berre added a comment - The problem was in the analyzeFinalConflictInTermsOfAssumptions() introduced in Sat4j 2.2: it was removing unit literals from the solvers. The issue has been fixed on HEAD in r938. I let the bug open until I get your feedback.
        Hide
        Updateme Updateme added a comment -

        Works now. Thanks.

        Show
        Updateme Updateme added a comment - Works now. Thanks.
        Hide
        Daniel Le Berre added a comment -

        Fix confirmed by reporter.

        Show
        Daniel Le Berre added a comment - Fix confirmed by reporter.

          People

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

            Dates

            • Created:
              Updated:
              Resolved:

              Development