Set time limit through Kissat API

[zengjian-hu-rai]

hi,

I wonder how to set the time limit through the Kissat API? kissat_set_option doesn't seem to work. Looks like we can set it through --time in CLI, is that the only option?

https://www.mankier.com/1/kissat
https://github.com/arminbiere/kissat/blob/master/src/kissat.h

The API works better for us as the CLI'd introduce significant overhead in disk I/O.

thanks, Jian

[zengjian-hu-rai]

Thank you for the confirmation and the detailed explanation! I'm glad that you consider it as a future enhancement.

[arminbiere]

It seems my comment got lost. I was first thinking how this is done for CaDiCaL and there it is the same following problem. Having a global timer like alarm and using signals as the stand alone solver can do will not work if you have several solver instances in the same process running in multiple threads for instance. One could in principle check spent global time (process or better walk clock) in regular intervals though. This is an overhead though. This interval base termination checking was in Lingering as it uses a call back while an asynchronous terminate call is of course cheaper.

[zengjian-hu-rai]

Understood. Thank you! I wish you luck in finding a solution that maintains optimal performance.