Implement parallel exploration of the computation tree

[aeporreca]

Currently, the computation tree is explored sequentially depth-first, which means that if we run into a nonterminating branch, the program will not terminate even if there exists a terminating and accepting branch elsewhere.

This can be solved by exploring the tree in parallel (i.e., running the child processes in parallel) but requires recursively terminating all other descendants as soon as an accepting computation halts.

[aeporreca]

OK, this just cannot be done as such. Even in simple examples (e.g., k-colouring K_5) too many processes are generated, giving a BlockingIOError: [Errno 35] Resource temporarily unavailable error.

[aeporreca]

Reopened the issue: I’ll try actual dovetailing (execute the computation on the 1st choice for 1 × time quantum, then the computation on the 1st choice for 2 × time quantum and the computation on the 1st choice for 2 × time quantum, etc…).

This should clearly work, the question is how to do it under Unix (alarms & signals, I suppose?) and if it is fast enough in practice.

[ghamerly]

I had also wondered about how to handle this several years ago, so I'll share my thoughts. I had a vague idea (not very well thought out) about using depth-limited DFS, which is something like dovetailing. I was thinking about doing it without multiple processes, instead manipulating the runtime stack to save and restore back to known states when needed. This is where I got stuck; I could not find a way of saving/restoring the Python runtime stack. In any event, what I was thinking about would require some kind of cooperative multitasking, which may not be easy to implement or get to work well.

As I said, just some thoughts that I had; they are probably not that practical.

[aeporreca]

Thanks for your thoughts! I am also looking for a possible implementation without multiprocessing, which would certainly improve the performances of the library as a side effect.

Your solution does indeed work in principle, and I’ve actually already seen an implementation of nondeterminism in C using setjmp and longjmp. However, there are no setjmp/longjmp in Python, and I’m not sure you can just write a wrapper for some C code (would that be compatible with the data structures manipulated by the interpreter?). According to my research, you can manipulate the interpreter stack using inspect, but that does not seem to include the program counter, only the values of the variables. Maybe using exceptions?

Python also has coroutines (both in terms of generators and now with async/await), but I still have to look into that.

My main requirement for this library is that the interface must absolutely be:

• declare your funcition @nondeterministic
• use guess inside it (with a mode parameter)

for pedagogical and elegance reasons.

Other solutions, which are certainly cleaner and faster in terms of implementation, but seem to require explicitly creating and passing around some “guesser” object, are this recent nondet library and this implementation of the amb operator on Rosetta Code.