Sat4j
  1. Sat4j
  2. SAT-14

After a call to expireTimeout(), a solver cannot be relaunched

    Details

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

      Description

      Once an expireTimeout() is performed, the solver state is in the "should stop" mode and a TimeoutException is launched whenever a call to isSatisfiable is performed.

      The fix is simple: the expireTimeout should properly reset the solver state in such a way that subsequent calls to the solver (isSatisfiable() methods) are properly handled.

      That issue as a nasty side effect on the MultiCore solver: it will prevent the various systems to be used after the first call to expireTimeout.

        Activity

        Hide
        Daniel Le Berre added a comment -

        Added test case BugSat14 in org.sat4j.pb showing the problem.

        Show
        Daniel Le Berre added a comment - Added test case BugSat14 in org.sat4j.pb showing the problem.
        Hide
        Daniel Le Berre added a comment -

        The code committed in r931 fixes the problem.

        Show
        Daniel Le Berre added a comment - The code committed in r931 fixes the problem.

          People

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

            Dates

            • Due:
              Created:
              Updated:
              Resolved:

              Development