如何实现非时间顺序回溯

Question

我正在研究CDCL SAT-Solver。我不知道如何实现非时间顺序回溯。这是否可以通过递归实现，或者仅在迭代方法中才可能。

实际上，我所做的喷气式飞机是实现一个与递归一起工作的DPLL求解器。与DPLL和CDCL最大的不同在于，树中的背架不是按时间顺序排列的。甚至有可能用递归实现这样的东西吗？在我的观点中，我在二进制决策树的节点中有两个选择，如果其中一个路径导致我一个问题：

1. 我尝试另一条路径 ->但它会像 DPLL 一样，意味着按时间顺序回溯
我
2. 返回：但是我永远不会回到这个节点。

所以我在这里错过了一些东西。难道唯一的选择是迭代实现它吗？

Answer 1

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

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

Answer 2

您可以修改它以获得后跳。

private Assignment recursiveBackJumpingSearch(CSP csp, Assignment assignment) {
    Assignment result = null;
    if (assignment.isComplete(csp.getVariables())) {
        result = assignment;
    }
    else {
        Variable var= selectUnassignedVariable(assignment, csp);
        for (Object value : orderDomainValues(var, assignment, csp)) {
            assignment.setAssignment(var, value);
            fireStateChanged(assignment, csp);
            if (assignment.isConsistent(csp.getConstraints(var))) {
                    result=recursiveBackJumpingSearch(csp, assignment);
                    if (result != null) {
                        break;
                    }
                    if (result == null)
                        numberOfBacktrack++;
            }
            assignment.removeAssignment(var);
        }
    }
    return result;
}