Add interrupts to RC2

[hbierlee]

Hi Alexey,

For our integration of RC2 with CPMpy (CPMpy/cpmpy#729), we're requiring timeouts, so I added in the interrupt feature as seen in the other PySAT solvers. I've gotten PySAT to compile locally, however, for some PYTHONPATH reason, I cannot run the tests, but I run my own Python files. The following works at least, perhaps it should be added as test:

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)

Cheers,

Henk

[alexeyignatiev]

Thanks for this, Henk. See the comments, there seems to be a bug.

[hbierlee]

Fixed the CI!

Where there other comments, or did you mean the CI output?

[alexeyignatiev]

Henk, I left three comments there for you. You can see them if you scroll up a little. The requested changes were:

1. Explicitly add an input argument assumptions=[] rather than passing **kwargs.
2. Make sure to use clear_interrupt() if the next call to RC2 is not to be interrupted.
3. Add doc-strings to the newly created methods interrupt() and clear_interrupt().

[hbierlee]

Hi Alexey,

Weirdly, I don't see your comments on GitHub on my side. I have no idea why. Perhaps you could use the Review feature?

I've processed comments 1 and 3, I'm not sure I understand comment 2. Should I myself call clear_interrupt somewhere?

Two further questions:

• I'm actually not entirely sure what will happen in the low-probability event that interrupt is called while we're in the rc2 loop rather than during a solve call? If you think this is a real risk, perhaps a check needs to be added to interrupt whether the solver is running? Let me know if you'd like to see this, or know some solution.
• oracle_solve now always calls oracle.solve_limited, is there any benefit to checking if there are 0 assumptions and no intterupt expected, and then in that case just calling oracle.solve?

[alexeyignatiev]

I obviously did that via the review functionality of GitHub, Henk. See the screenshot:

As for your question, the answer is yes, clear_interrupt must be called as per the documentation. Hold on, I presume it will be quicker if I do it.

[hbierlee]

For some reason, the review does not show up on my side (and I thought perhaps you had used line comments without review, although I should be able to see those too afaik). It could be that you still have to hit the "submit review" button somewhere? Anyway, thanks for the help and the quick merge.

[alexeyignatiev]

I've now added asynchronous interruption in RC2 properly (it required some thought because of the incrementality). Should be available in 1.8.dev26 once it gets compiled (give GitHub a couple of hours to finish).