Adding time-limit for solver execution using API.

[Horef]

Hello!
I was wondering if it is possible to add a time-limit for the run of the solver using the cadical API?
Or is it only possible by creating a custom terminator? (And if so, could you please provide an example of how such a terminator would be greated?)

Many thanks in advance.

[m-fleury]

In essence (I did not try it though):

1. Create an instance of the terminator https://github.com/arminbiere/cadical/blob/master/src/cadical.hpp#L1104 that reads a boolean must_terminate set to false.

class MyTerminator : public Terminator {
private:
  bool must_terminate = false;
public:
  virtual ~MyTerminator () {};
  virtual bool terminate () {return must_terminate;};
};

MyTerminator terminator ();

3. Connect that instance to CaDiCaL

cadical->connect_terminator (terminator);

5. Launch a thread from your program (see https://stackoverflow.com/questions/44616241/c11-how-to-execute-a-function-in-the-main-thread-after-n-seconds). After sleeping the flag must_terminate should be set to true
6. CaDiCaL will terminate once the flag is true.

[Horef]

Great, thank you very much for the reply, I will look into it!

I have also discovered that it could be done like this:

class TimeTerminator : public CaDiCaL::Terminator {
private:
    chrono::high_resolution_clock::time_point start;
public:
    int time_limit;
    TimeTerminator(int time_limit) {
        this->time_limit = time_limit;
        start = chrono::high_resolution_clock::now();
    }

    bool terminate() {
        auto now = chrono::high_resolution_clock::now();
        auto time = chrono::duration_cast<chrono::milliseconds>(now - start).count();
        return time > time_limit;
    }
};

And later simply instantiated:

TimeTerminator *terminator = new TimeTerminator(time_limit);
solver->connect_terminator(terminator);

It measures the time from the moment that the terminator was created, but it seems to be sufficient in my case, as I am creating instances of this object right before calling the solver.solve() command.

Also sorry for the messy cpp code, if it is a bad way to do this. I am relatively new to cpp, and mostly am just guessing how things should work based on my experience with other languages.

[m-fleury]

That should work. It might be a bit more costly though (sleep_for means that the threads waits and the OS will wake it once it has slept long enough, while you are getting the time and subtracting each time to the base).

[Horef]

Thanks for pointing that out!
Shouldn't be a problem in my use-case (as I am only interested in relative performance, so until all instances are run in the same way - I don't mind waiting a few more seconds), but it is very good to know.