I'm working on a CDCL SAT-Solver. I don't know how to implement non-chronological backtracking. Is this even possible with recursion or is it only possible in a iterative approach.
Actually what i have done jet is implemented a DPLL Solver which works with recursion. The great differnece from DPLL and CDCL ist that the backracking in the tree is not chronological. Is it even possible to implement something like this with recursion. In my opionion i have two choices in the node of the binary-decision-tree if one of to path leads i a conlict:
- I try the other path -> but then it would be the same like the DPLL, means a chronological backtracking
- I return: But then i will never come back to this node.
So am i missing here something. Could it be that the only option is to implement it iterativly?