경로 합계 확인

LeetCode 확인 질문: 112. 경로 합계

problem 정의를 살펴보겠습니다.

Given the root of a binary tree and an integer targetSum, return true if the tree has a root-to-leaf path such that adding up all the values along the path equals targetSum.

A leaf is a node with no children.

구현

JavaScript/TypeScript에서 이 문제를 해결하는 방법은 다음과 같습니다.

function hasPathSum(root: TreeNode | null, targetSum: number): boolean {
    if(root == null) {
        return false;
    }
    if(root.val-targetSum == 0 && root.left == null && root.right == null) {
        return true;
    }
    return hasPathSum(root.left, targetSum-root.val) || hasPathSum(root.right, targetSum-root.val);
};

트리 문제는 종종 재귀 알고리즘으로 쉽게 해결됩니다.

사례별로 나누면 다음과 같습니다.
현재 루트가 null이면 targetSum과 일치하는 경로가 없습니다.

현재 노드 값이 targetSum과 일치하고 현재 노드가 리프 노드이면 완료되고 경로가 존재합니다.

현재 노드 왼쪽 자식에 경로가 있거나 현재 노드 오른쪽 자식에 이 노드의 현재 값을 뺀 경로가 있으면 경로가 존재합니다.

구현 지정

먼저 트리 데이터 유형을 정의합니다.

datatype TreeNode = Nil | Tree(val: nat, left: TreeNode, right: TreeNode)

문제 정의를 두 개의 도우미 함수/술어로 변환합니다. Dafny에서 시퀀스 유형인 seq는 개체와 같은 배열 유형(즉, 인덱싱할 수 있음)이며 연결 목록과도 같습니다. assert path == [path[0]+path[1..];

predicate isPath(paths: seq<TreeNode>, root: TreeNode) {
    if |paths| == 0 then false else match paths[0] {
        case Nil => false
        case Tree(val, left, right) => if |paths| == 1 then root == paths[0] else root == paths[0] && (isPath(paths[1..], left) || isPath(paths[1..], right))
    }
}

경로는 루트에서 시작하는 일련의 TreeNodes라고 합니다. 그런 다음 시퀀스가 ​​비어 있지 않고 첫 번째 노드가 Nil이 아니고 루트가 목록의 첫 번째 노드와 같으면 목록의 나머지(첫 번째 요소/루트 제거)가 루트로 시작하는 경로이거나 왼쪽 자식 또는 오른쪽 자식. 트리에서 유효한 경로인 경우 true 또는 false를 반환합니다.

function pathSum(paths: seq<TreeNode>): nat {
    if |paths| == 0 then 0 else match paths[0] {
        case Nil => 0
        case Tree(val, left, right) => val + pathSum(paths[1..])
    }
}

경로가 주어지면 목록을 첫 번째 요소와 나머지 목록으로 재귀적으로 분리한 다음 나머지 목록의 pathSum에 노드 값을 추가합니다.

이러한 정의가 주어지면 문제 정의를 다음과 같이 번역할 수 있습니다.

method hasPathSum(root: TreeNode, targetSum: int) returns (b: bool) 
    ensures b ==> exists p: seq<TreeNode> :: isPath(p, root) && pathSum(p) == targetSum
{
}

다시 말하지만, targetSum에 대한 합계가 메서드가 true를 반환하는 일부 경로 p의 존재를 확인할 수 있습니다.

구현 확인

이것은 TypeScript 코드를 Dafny로 간단히 변환해야 합니다.

method hasPathSum(root: TreeNode, targetSum: int) returns (b: bool) 
    ensures b ==> exists p: seq<TreeNode> :: isPath(p, root) && pathSum(p) == targetSum
{
    if root == Nil {
        return false;
    }

    if(root.val - targetSum == 0 && root.left == Nil && root.right == Nil) {
        return true;
    }
    var leftPath := hasPathSum(root.left, targetSum-root.val);
    var rightPath := hasPathSum(root.right, targetSum-root.val);

    return leftPath || rightPath;
}

Dafny에 대한 유도 증명

Dafny는 우리가 이 메소드를 작성할 때 우리의 ensure 절을 즉시 확신하지 않습니다. 설득하는 것은 그리 어렵지 않지만 다른 Dafny 기능을 사용해야 합니다.

먼저 엔딩 케이스를 해결합니다.

if(root.val - targetSum == 0 && root.left == Nil && root.right == Nil) {
  assert isPath([root], root) && pathSum([root]) == targetSum;
  return true;
}

[root]가 유효한 경로이고 존재함을 보여주는 어설션을 추가합니다. 두 번째로 루트 값 == targetSum이면 pathSum([root])도 targetSum과 같습니다.

이 작업을 수행한 후 Dafny는 반환 조건을 승인하지만 재귀 사례에 대해 불평합니다.

재귀 호출을 호출하고 결과를 변수에 저장한 다음 사례로 분류합니다.

var leftPath := hasPathSum(root.left, targetSum-root.val);
var rightPath := hasPathSum(root.right, targetSum-root.val);

if leftPath {
  ghost var p: seq<TreeNode> :| isPath(p, root.left) && pathSum(p) == targetSum-root.val;
  assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
}
if rightPath {
  ghost var p: seq<TreeNode> :| isPath(p, root.right) && pathSum(p) == targetSum-root.val;
  assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
}

여기서 새 구문은 고스트 var입니다. 고스트 var는 Dafny가 어설션에 유용한 데이터를 추적하는 데 사용할 수 있는 변수이지만 실제로 메서드가 실행될 때 실제로 실행되는 코드의 일부는 아닙니다.

프로그램의 실행 컨텍스트가 아닌 사양 컨텍스트에만 존재하는 변수입니다.

두 번째로 :| 연산자는 such that 를 의미하므로 기본적으로 다음과 같은 문장을 읽을 수 있습니다.

if leftPath {
  ghost var p: seq<TreeNode> :| isPath(p, root.left) && pathSum(p) == targetSum-root.val;
  assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
}

leftPath 변수가 참이면 유도적으로 hasPathSum은 루트 왼쪽 노드에서 시작하는 경로 p가 존재하고 해당 경로 합계가 targetSum-root.val과 같다고 말합니다. 해당 경로를 p에 할당합니다. 그런 다음 해당 경로에 루트를 추가하면 여전히 유효한 경로이고 pathSum이 root.val+(targetSum-root.val) == targetSum임을 보여줍니다. 오른쪽의 동일한 인수에 따라 메서드가 확인합니다.

method hasPathSum(root: TreeNode, targetSum: int) returns (b: bool) 
    ensures b ==> exists p: seq<TreeNode> :: isPath(p, root) && pathSum(p) == targetSum
{
    if root == Nil {
        return false;
    }

    if(root.val - targetSum == 0 && root.left == Nil && root.right == Nil) {
        assert isPath([root], root) && pathSum([root]) == targetSum;
        return true;
    }
    var leftPath := hasPathSum(root.left, targetSum-root.val);
    var rightPath := hasPathSum(root.right, targetSum-root.val);

    if leftPath {
        ghost var p: seq<TreeNode> :| isPath(p, root.left) && pathSum(p) == targetSum-root.val;
        assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
    }
    if rightPath {
        ghost var p: seq<TreeNode> :| isPath(p, root.right) && pathSum(p) == targetSum-root.val;
        assert isPath([root]+p, root) && pathSum([root]+p) == targetSum;
    }
    return leftPath || rightPath;
}