pysat
pysat copied to clipboard
Time out for sat solvers
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.
OK, unless there are volunteers, I will not be able to find time for this any time soon. Sorry.