Как реализовать не хронологическое отслеживание

Question

Я работаю над CDCL SAT-Solver.Я не знаю, как реализовать не хронологическое отслеживание.Возможно ли это даже с рекурсией или это возможно только при итеративном подходе.

На самом деле то, что я сделал, - это реализованный DPLL Solver, который работает с рекурсией.Большое отличие от DPLL и CDCL состоит в том, что обратное отслеживание в дереве не является хронологическим.Возможно ли даже реализовать что-то подобное с помощью рекурсии.В моем мнении у меня есть два варианта в узле дерева двоичных решений, если один из путей приводит к конфликту:

1. Я пробую другой путь -> но тогда это будет так же, какDPLL означает хронологическое возвращение назад
2. Я возвращаюсь: Но тогда я никогда не вернусь к этому узлу.

Так что я что-то здесь упускаю.Может ли быть так, что единственный вариант - это реализовать его итеративно?

Answer 1

Вы можете изменить это, чтобы получить backjumping.

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;
}

Answer 2

Нехронологический возврат (или обратный переход, как его обычно называют) может быть реализован в решателях, которые используют рекурсию для присвоения переменных. На языках, которые поддерживают нелокальные переходы, вы обычно используете этот метод. Например, в языке C вы должны использовать setjmp () для записи точки в стеке и longjmp () для обратного перехода к этой точке. C # имеет блоки try-catch, языки Lispy могут иметь catch-throw и т. Д.

Если язык не поддерживает нелокальный переход, вы можете добавить замену в свой код. Вместо того, чтобы dpll () возвращала FALSE, она возвращает кортеж, содержащий FALSE и количество уровней, которые необходимо отследить. Вызывающие абоненты уменьшают счетчик в кортеже и возвращают его, пока не вернется ноль.