Should we do work stealing scheduling? about sat-solver HOT 3 CLOSED

@limo1996:
I suggest you take this one.
If you want you can extend the google doc with the original interface description and I can review it.
Here are a few points that I think are important:

• We should be able to turn the work stealing part on and off such that we can compare it with the current implementation
• I would suggest that we still start with master-worker until every working is doing something and then switch to workstealing among the workers
• We have to consider weird special cases such as circular dependencies (e.g worker 1 wants to steal from worker 2, worker 2 from worker 3 and worker 3 from worker 1, the only worker that is doing something is worker 4)
• I'm not sure if a master is still necessary: the "we are done sat/unsat" message could also be sent directly by the worker
• The biggest challenge is probably to identify the "we are done unsat" case. At the moment I don't see how this could be done...

from sat-solver.

Partially solved for sat cases. If there will be time I can try to solve it for unsat. However, my approach can still be improved since now I am stealing just from one neighbor(we can try to steal from all neighbour but there will be higher traffic -> bad for small cases but good for bigger ones)

from sat-solver.

UNSAT cases: future work

from sat-solver.