Add interrupts to RC2

examples/rc2.py

@@ -248,6 +248,12 @@ def __init__(self, formula, solver='g3', adapt=False, exhaust=False,
         if not formula.hard and len(self.sels) > 100000 and min(wght) == max(wght):
             self.minz = False
 
+    def _oracle_solve(self, assumptions=[]):
+        """
+            Calls `oracle.solve()` given `assumptions` and possible interrupts
+        """
+        return self.oracle.solve_limited(assumptions=assumptions, expect_interrupt=self.expect_interrupt)
+
     def __del__(self):
         """
             Destructor.
@@ -469,7 +475,7 @@ def delete(self):
             self.processor.delete()
             self.processor = None
 
-    def compute(self):
+    def compute(self, expect_interrupt=False):
         """
             This method can be used for computing one MaxSAT solution,
             i.e. for computing an assignment satisfying all hard
@@ -508,6 +514,7 @@ def compute(self):
                 2
                 >>> rc2.delete()
         """
+        self.expect_interrupt = expect_interrupt
 
         # simply apply MaxSAT only once
         res = self.compute_()
@@ -632,7 +639,7 @@ def compute_(self):
             self.adapt_am1()
 
         # main solving loop
-        while not self.oracle.solve(assumptions=self.sels + self.sums):
+        while not self._oracle_solve(assumptions=self.sels + self.sums):
             self.get_core()
 
             if not self.core:
@@ -892,7 +899,7 @@ def trim_core(self):
         for i in range(self.trim):
             # call solver with core assumption only
             # it must return 'unsatisfiable'
-            self.oracle.solve(assumptions=self.core)
+            self._oracle_solve(assumptions=self.core)
 
             # extract a new core
             new_core = self.oracle.get_core()
@@ -930,7 +937,7 @@ def minimize_core(self):
             while i < len(self.core):
                 to_test = self.core[:i] + self.core[(i + 1):]
 
-                if self.oracle.solve_limited(assumptions=to_test) == False:
+                if self._oracle_solve(assumptions=to_test) == False:
                     self.core = to_test
                 elif self.oracle.get_status() == True:
                     i += 1
@@ -962,7 +969,7 @@ def exhaust_core(self, tobj):
         """
 
         # the first case is simpler
-        if self.oracle.solve(assumptions=[-tobj.rhs[1]]):
+        if self._oracle_solve(assumptions=[-tobj.rhs[1]]):
             return 1
         else:
             self.cost += self.minw
@@ -975,7 +982,7 @@ def exhaust_core(self, tobj):
             # increasing the bound
             self.update_sum(-tobj.rhs[i - 1])
 
-            if self.oracle.solve(assumptions=[-tobj.rhs[i]]):
+            if self._oracle_solve(assumptions=[-tobj.rhs[i]]):
                 # the bound should be equal to i
                 return i
 
@@ -1259,6 +1266,54 @@ def _map_extlit(self, l):
 
             return int(copysign(i, l))
 
+    def interrupt(self):
+        """
+            Interrupt the execution of the current *limited* SAT call in the RC2
+            algorithm. Can be used to enforce time limits using timer objects.
+            The interrupt must be cleared before performing another `compute`
+            call (see :meth:`clear_interrupt`).
+
+            **Note** that this method can be called if the `compute` call was
+            made with the option ``expect_interrupt`` set to ``True``. Behaviour is **undefined** if used to ``expect_interrupt`` was set to ``False``.
+
+            Example:
+
+            .. code-block:: python
+                >>> from pysat.examples.rc2 import RC2
+                >>> from pysat.examples.genhard import PHP
+                >>> from pysat.formula import WCNF
+                >>> from threading import Timer
+
+                >>> cnf = PHP(nof_holes=20)
+                >>> wcnf = WCNF()
+                >>> for c in cnf.clauses:
+                >>>     wcnf.append(c)
+
+                >>> with RC2(wcnf) as rc2:
+
+                >>>     def interrupt(s):
+                >>>         print("interrupted!")
+                >>>         s.interrupt()
+
+                >>>     timer = Timer(1, interrupt, [rc2])
+                >>>     timer.start()
+                >>>     print("computing..")
+                >>>     rc2.compute(expect_interrupt=True)
+                >>>     print("done.")
+        """
+
+        if self.oracle:
+            self.oracle.interrupt()
+
+    def clear_interrupt(self):
+        """
+            Clears a previous interrupt. If a `compute` call was interrupted
+            using the :meth:`interrupt` method, this method **must be called**
+            before calling `compute` again.
+        """
+        if self.oracle:
+            self.oracle.clear_interrupt()
+
 
 #
 #==============================================================================
@@ -1343,7 +1398,7 @@ def init_wstr(self):
         # number of finished levels
         self.done = 0
 
-    def compute(self):
+    def compute(self, expect_interrupt=False):
         """
             This method solves the MaxSAT problem iteratively. Each
             optimization level is tackled the standard way, i.e. by
@@ -1353,6 +1408,7 @@ def compute(self):
             activates more soft clauses by invoking
             :func:`activate_clauses`.
         """
+        self.expect_interrupt = expect_interrupt
 
         if self.done == 0 and self.levl != None:
             # it is a fresh start of the solver