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

ISolver.isSatisfiable(VecInt) is affected by previous call

    Details

    • Type: Bug
    • Status: Resolved
    • Priority: Blocker
    • 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

      The method ISolver.isSatisfiable(VecInt) is affected by previous calls which leads to unexpected results.

      1. bug.java
        2 kB
        Updateme Updateme
      2. Eshop-fm.dimacs
        11 kB
        Updateme Updateme
      3. TestSatAssumps.java
        2 kB
        Updateme Updateme

        Activity

        Hide
        leberre Daniel Le Berre added a comment -

        This is probably an issue similar to SAT-17. I will commit a fix in HEAD asap.

        Show
        leberre Daniel Le Berre added a comment - This is probably an issue similar to SAT-17 . I will commit a fix in HEAD asap.
        Hide
        leberre Daniel Le Berre added a comment -

        There was an other issue related to the final conflict minimization method. It is now fixed on HEAD, in r941.

        Show
        leberre Daniel Le Berre added a comment - There was an other issue related to the final conflict minimization method. It is now fixed on HEAD, in r941.
        Hide
        martinj Updateme Updateme added a comment -

        The bug still seems to be reproducable. I'm having a problem with it in my project. See the attached file. Btw, the bug is is only reproducable when using the Set class to hold some variables. This is because of the internal rearrangements in the collection. If I use a List instead, preserving ordering, the bug is not reproducable.

        Show
        martinj Updateme Updateme added a comment - The bug still seems to be reproducable. I'm having a problem with it in my project. See the attached file. Btw, the bug is is only reproducable when using the Set class to hold some variables. This is because of the internal rearrangements in the collection. If I use a List instead, preserving ordering, the bug is not reproducable.
        Hide
        leberre Daniel Le Berre added a comment -

        Hi Martin,

        I can indeed reproduce the problem.
        I have to dig out the reason of that behavior. It is probably due to the use of an inconsistent set of literals as assumption.

        Show
        leberre Daniel Le Berre added a comment - Hi Martin, I can indeed reproduce the problem. I have to dig out the reason of that behavior. It is probably due to the use of an inconsistent set of literals as assumption.
        Hide
        leberre Daniel Le Berre added a comment -

        That issue is a showstopper for one user.

        Show
        leberre Daniel Le Berre added a comment - That issue is a showstopper for one user.
        Hide
        leberre Daniel Le Berre added a comment -

        Fixed in r967. The issue was caused by satisfied literals in the assumptions, causing an incoherent value for Solver.trailLim. Added a new assertion in Solver.assume() to spot easily such kind of problem in the future.

        Show
        leberre Daniel Le Berre added a comment - Fixed in r967. The issue was caused by satisfied literals in the assumptions, causing an incoherent value for Solver.trailLim. Added a new assertion in Solver.assume() to spot easily such kind of problem in the future.

          People

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

            Dates

            • Created:
              Updated:
              Resolved: