backtracking - How to implement non chronological backtracking

Question

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:

1. I try the other path -> but then it would be the same like the DPLL, means a chronological backtracking
2. 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?

标签： backtrackingsatsat-solversdpll

Answer 1

可以在使用递归进行变量分配的求解器中实现非按时间顺序的回溯（或通常称为回跳）。在支持非本地 goto 的语言中，您通常会使用该方法。例如，在 C 语言中，您将使用 setjmp() 记录堆栈中的一个点，并使用 longjmp() 回跳到该点。C# 有 try-catch 块，Lispy 语言可能有 catch-throw，等等。

如果该语言不支持非本地 goto，那么您可以在代码中实现替代。不是 dpll() 返回 FALSE，而是让它返回一个包含 FALSE 和需要回溯的级别数的元组。上游调用者递减元组中的计数器并返回它，直到返回零。