search

pysathq / pysat

A toolkit for SAT-based prototyping in Python
https://pysathq.github.io/
MIT License
385 stars 69 forks source link

Time out for sat solvers #78

Open algebravic opened 3 years ago

algebravic commented 3 years ago

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.

alexeyignatiev commented 3 years ago

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