search

jix / varisat

SAT solver written in Rust
https://jix.one/project/varisat
Apache License 2.0
253 stars 17 forks source link

Solving timeout #111

Open tsionyx opened 5 years ago

tsionyx commented 5 years ago

It would be great to have some optional timeout (e.g. in Solver::solve(&mut self, timeout: Option<Duration>)) to break out of the loop if the problem is too hard to solve in reasonable amount of time.

raphlinus commented 4 years ago

I have a local branch where I've added a "canceler" object (Arc<AtomicBool> under the hood). This is more useful than a time-based limit for me, because it's in the concept of an interactive application. It's also strictly more general, because you can always simulate a timeout, but on the other hand it does require the use of a separate thread.

I'm happy to post a PR if there's consensus this would be useful.

jix commented 4 years ago

Eventually I want to support setting an arbitrary termination callback, i.e. an equivalent of the ipasir_set_terminate function of the IPASIR C API. On top of that it would be possible to implement both, cancellation using an atomic bool and using a timeout w/o additional threads, ideally each with a convenience API. That requires a bit of careful design, especially if I want to allow querying the solver state from within that callback.

I don't see myself finding the time to work on that anytime soon though, so I wouldn't mind merging a PR that adds just a canceler object. Even then, it might take me some time to merge it, since the CI setup on Circle CI broke and I haven't found time to migrate this project to github actions yet.