pysat icon indicating copy to clipboard operation
pysat copied to clipboard

Time out for sat solvers

Open algebravic opened this issue 3 years ago • 1 comments

From the documentation one can use solve_limited with expect_interrupt to get a SAT solver to terminate for some external reason -- like a time limitation. However, not all of the solvers have this feature. It would be nice to have a method for each solver to query whether or not this is available. Right now, if you try to call solve_limited on one for which this isn't available, you'll get an exception. It would be nice if a time out mechanism was available for these other solvers. Since they're accessed by an external call, it would require a bit of complicated plumbing using process control.

algebravic avatar Apr 23 '21 12:04 algebravic

OK, unless there are volunteers, I will not be able to find time for this any time soon. Sorry.

alexeyignatiev avatar Apr 23 '21 12:04 alexeyignatiev