그래프의 논리

그래프 이론과 유한 모델 이론의 수학 분야에서는 그래프의 논리가 수학 논리의 문장을 이용한 그래프 속성의 형식적 사양을 다룬다.이러한 문장에서 사용할 수 있는 논리 연산 유형에는 몇 가지 차이가 있다.그래프의 1차 로직은 변수와 술어가 개별 정점과 그래프 가장자리와 관련된 문장과 관련된 반면, 단차 2차 그래프 로직은 정점이나 가장자리의 집합에 대해 정량화를 허용한다.최소 고정점 연산자에 기반한 로직은 정점의 튜플에 비해 더 많은 일반 술어를 허용하지만, 이러한 술어는 고정점 연산자를 통해서만 구성할 수 있어 1차 순서와 단차 순서의 중간 수준으로 힘을 제한할 수 있다.null

A sentence ${\displaystyle S}$ may be true for some graphs, and false for others; a graph ${\displaystyle G}$ is said to model ${\displaystyle S}$, written ${\displaystyle G\models S}$, if ${\displaystyle S}$ is true of the vertices and adjacency relation of ${\displaystyle G}$. The algorithmic pr모델 검사 문제는 주어진 그래프가 주어진 문장을 모형화하는지 여부를 검정하는 것과 관련이 있다.만족도의 알고리즘적 문제는 주어진 문장을 모형화하는 그래프가 있는지 여부를 시험하는 것과 관련이 있다.모델 점검과 만족도 모두 일반적으로 어렵지만, 몇몇 주요 알고리즘 메타-이론은 이러한 방식으로 표현된 속성을 중요한 등급의 그래프에 대해 효율적으로 테스트할 수 있다는 것을 보여준다.null

그래프 논리학의 다른 연구 주제로는 무작위 그래프가 특정 유형의 논리 내에서 특정 속성을 가질 가능성에 대한 조사와 고유한 그래프에 의해 모델링된 논리 문장 찾기에 기초한 데이터 압축 방법 등이 있다.null

퍼스트 오더

그래프의 1차 논리학에서 그래프 속성은 변수들이 그래프 정점을 나타내는 정량화된 논리 문장으로 표현되며, 동일성과 인접성 시험에 대한 술어가 있다.null

예

예를 들어, 그래프에 분리된 정점이 없다는 조건은 문장으로 표현될 수 있다.

${\displaystyle \forall u\reason v(u\sim v)}$

여기서${\displaystyle }$~ ${\displaystyle \sim }$ 기호는$$ 두 꼭지점 사이의 간접 인접 관계를 나타낸다.이 문장은 모든 꼭지점 $u{\displaystyle }$ ${\displaystyle u}$에 대해 $u{\displaystyle }$ ${\displaystyle u}$에 인접한$$ 또 다른 $꼭지점{\displaystyle }$ v ${\displaystyle v}$이(가) 있음을$$ 의미하는 것으로 해석할 수 있다$.$^[1]

고정 서브그래프 H에 대한 서브그래프 이형성 문제는 H가 더 큰 그래프 G의 서브그래프로 나타나는지를 묻는다.H의 각 가장자리에 대해 해당 변수 쌍이 인접 정점을 나타내고 나머지 각 H 정점 쌍에 대해 해당 변수 쌍이 구별 정점을 나타내도록 정점(H의 각 정점에 대해 하나)의 존재를 나타내는 문장으로 표현될 수 있다.^[2] 그림을 참조하십시오.특별한 경우로서, (고정 클라이크 크기에 대한) 클라이크 문제는 모두 인접한 클라이크 크기와 동일한 정점 수의 존재를 명시한 문장으로 표현될 수 있다.null

공리

단순 비방향 그래프의 경우 그래프의 1차 이론에는 공리가 포함된다.

${\displaystyle \mathrm{\forall }}$ ${\displaystyle u\mathrm{}}$(${\displaystyle u}$~${\displaystyle u}$)${\$그래프는 루프를 포함할 수 없음) 및

${\displaystyle \mathrm{\forall }}$ ${\displaystyle u}$ ${\displaystyle \mathrm{\forall }}$ ${\displaystyle v}$(${\displaystyle u}$~ ${\displaystyle v}$ ${\displaystyle \Rightarrow }$ v ~${\displaystyle u}$) ${\displaystyle$\$forall u\forall v(u\sim v\Rightarrow v\sim u)}($edges는 리디렉션되지 않음).$$^[3]

지시된 그래프와 같은 다른 유형의 그래프에는 서로 다른 공리가 포함될 수 있으며,^[4] 다중 그래프 속성의 논리적 형식은 다중 모서리 관계나^[5] 정점과 모서리 변수와 같은 특별한 처리가 필요하다.^[6]null

제로원법

Glebskiĭ 외 연구진(1969)과 독립적으로 파긴(1976)은 1차 그래프 논리에 대해 제로원 법칙을 증명했다; 파긴의 증거는 콤팩트성 정리를 사용했다.이 결과에 따르면 Erdds-Rényi 모델에서 임의 그래프에 대해 모든 1차 문장은 거의 항상 참이거나 거의 항상 거짓이다.즉, S를 고정된 1차 문장으로 하고, 라벨이 붙은 정점 집합의 모든 그래프 중에서 무작위로 임의의 n-vertex 그래프 G를_n 선택한다.그런 다음 n은 한계에서 G 모델_n S가 0 또는 1을 가질 확률을 무한대로 만드는 경향이 있다.

${\displaystyle \lim_{n\to \inflt }\operatorname {Pr}[G_{n}\models S]\in \{0,1\}.}$

또한 Rado 그래프에 의해 모델링된 문장이 무작위 유한 그래프에 의해 모델링될 확률을 정확하게 나타내는 Rado 그래프 R이라는 특정한 무한 그래프가 있다.

${\displaystyle R\models S\quad \Long left \quad \quarrow \quad \quarrow \quarrow _{n\infty }\operatorname {Pr}[G_{n}\models S]=1.}$

각 가장자리가 고정된 확률로 다른 가장자리와 독립적으로 포함되는 랜덤 그래프의 경우 동일한 문장이 0 또는 1로 증가하는 확률을 갖는 동일한 결과가 참이다.null

주어진 문장의 확률이 0인지 1인지를 결정하는 계산 복잡성은 높은데, 문제는 PSPACE-완전성이다.^[7]1차 그래프 속성이 랜덤 그래프에서 1로 조정되는 확률을 갖는 경우, 해당 속성을 모델링하는 모든 n-vertex 그래프를 그래프당 다항식 지연(n의 함수)으로 나열할 수 있다.^[3]null

가장자리 포함 확률은 정점 수의 함수이며 가장자리 포함 또는 제외 결정이 모든 가장자리의 동일한 확률로 독립적으로 이루어지는 비일관 랜덤 그래프에 대해서도 유사한 분석을 수행할 수 있다.그러나 이러한 그래프의 경우 상황은 더 복잡하다.이 경우, 1차 속성에는 하나 이상의 임계값이 있을 수 있는데, 가장자리 포함 확률이 임계값에서 떨어져 있을 때 주어진 속성을 가질 확률은 0 또는 1이 되는 경향이 있다.이러한 임계값은 결코 n의 비합리적인 힘이 될 수 없으므로, 가장자리 포함 확률이 비합리적인 힘이 되는 무작위 그래프는 균일하게 랜덤 그래프에 대한 법칙과 유사한 제로원 법칙을 따른다.유사한 제로원 법칙은 c가 초특정 비율이 아닌 한 c > 1의 가장자리 포함 확률이 n인^−c 매우 희박한 무작위 그래프를 의미한다.^[8]c가 초특수인 경우, 주어진 속성을 가질 확률은 0이나 1이 아닌 한계에 이를 수 있지만, 이 한계는 효율적으로 계산할 수 있다.^[9]문턱이 무한히 많은 1차 문장이 존재한다.^[10]null

매개 변수화된 복잡성

1차 문장이 k개의 고유 변수를 포함하는 경우, 정점의 모든 k-tule을 조사하여 정점의 그래프로 설명하는 속성을 시험할 수 있다. 그러나 이 짐승의 힘 검색 알고리즘은 O(n^k) 시간이 걸리므로 특별히 효율적이지 않다.그래프가 주어진 1차 문장을 모형화하는지 확인하는 문제는 특별한 경우로서 서브그래프 이형성 문제(문장이 고정 서브그래프를 포함하는 그래프를 설명하는 경우)와 클리크 문제(문장이 고정된 크기의 완전한 서브그래프를 포함하는 그래프를 설명하는 경우)를 포함한다.매개변수화된 복잡성의 관점에서 보면 딱딱한 문제의 서열 1단계인 W(1)에게 계급문제는 어렵다.따라서, 고정 매개변수 추적 가능한 알고리즘은 있을 것 같지 않으며, 실행 시간이 k와 n에 독립적인 함수 f와 상수^c c에 대해 O(f(k) n) 형태를 취한다.^[11]더 강하게 말하면, 지수 시간 가설이 사실이라면, clique-finding과 1차 모델 점검은 반드시 지수가 k에 비례하는 n의 힘에 비례하는 시간이 걸릴 것이다.^[12]null

제한된 등급의 그래프에서, 1차 문장의 모델 확인은 훨씬 더 효율적일 수 있다.특히 1차 문장으로 표현 가능한 모든 그래프 속성은 경계 확장 그래프에 대해 선형 시간 내에 테스트할 수 있다.이것들은 모든 얕은 미성년자가 희박한 그래프인 그래프인데, 가장자리 대 정점의 비율은 미성년자의 깊이의 함수에 의해 제한된다.보다 일반적으로, 1차 모델 검사는 무감각 그래프에 대해 거의 선형에 가까운 시간에 수행될 수 있으며, 그래프 클래스는 가능한 각 깊이에서 최소 한 개의 금지된 얕은 부위가 있다.반대로, 모델 점검이 어떤 유전적 그래프 계열에 대해서도 고정 매개변수를 추적할 수 있다면, 그 계열은 어디에도 쓸모 없는 것이어야 한다.^[13]null

데이터 압축 및 그래프 이형성

G가 S를 모형화하는 유일한 그래프라면 그래프 G를 정의하는 것이 그래프 논리상 1차 문장 S라고 한다.모든 그래프는 적어도 하나의 문장으로 정의될 수 있다. 예를 들어, n+1 변수를 가진 문장으로 n-vertex 그래프 G를 정의할 수 있다. 그래프의 각 꼭지점마다 하나씩, 그리고 그래프의 n 꼭지점 이외의 정점이 없다는 조건을 명시하기 위해 한 개 더 정의한다.문장의 추가 절은 두 정점 변수가 같지 않고, G의 각 가장자리가 없으며, G의 비인접 정점 쌍 사이에 가장자리가 없는지 확인하는 데 사용될 수 있다.그러나 일부 그래프의 경우 그래프를 정의하는 상당히 짧은 문장이 존재한다.^[14]null

여러 가지 다른 그래프 불변제는 주어진 그래프를 정의하는 가장 단순한 문장(단순함의 다른 척도로)에서 정의될 수 있다.특히 그래프의 논리적 깊이는 그래프를 정의하는 문장에서 정량자(정량자 순위)의 최소 내포 수준으로 정의된다.^[15]위에서 설명한 문장은 모든 변수에 대한 정량자를 둥지 틀기 때문에 논리적 깊이 n + 1을 갖는다.그래프의 논리적 너비는 그래프를 정의하는 문장의 최소 변수 수입니다.^[15]위에서 요약한 문장에서 이 수의 변수는 다시 n + 1이다. 논리적 깊이와 논리적 너비는 모두 주어진 그래프의 트리 너비 측면에서 경계할 수 있다.^[16]논리 길이는 유사하게 그래프를 설명하는 가장 짧은 문장의 길이로 정의된다.^[15]위에서 설명한 문장은 정점수의 제곱에 비례하는 길이를 가지지만, 가장자리 수에 비례하는 길이의 문장으로 어떤 그래프를 정의할 수 있다.null

모든 나무, 그리고 대부분의 그래프는 두 변수만으로 1차 문장으로 설명할 수 있지만 술어를 세어 확장한다.일정한 수의 변수가 고정된 이 논리에서 문장으로 설명할 수 있는 그래프의 경우 다항 시간(다항식의 지수를 변수 수와 동일)에 그래프 시성화를 찾을 수 있다.시성을 비교함으로써 다항 시간 내에 이러한 그래프에 대한 그래프 이형성 문제를 해결할 수 있다.^[17]null

만족도

주어진 1차 문장이 유한한 비방향 그래프로 실현될 수 있을지는 불분명하다.^[18]null

무한 그래프에 의해 모델링되지만 어떤 유한 그래프에 의해 모델링되지 않는 1차 문장이 존재한다.예를 들어, 1도의 꼭지점이 정확히 1이고, 다른 모든 꼭지점이 정확히 2인 성질은 1차 문장으로 표현할 수 있다.무한 레이로 모델링되지만 유한 그래프에 대한 오일러의 손떨림 보조정리 위반이다.그러나 한정되지 않은 그래프에 대한 1차 문장의 만족도가 불변의 상태로 남아 있는 것은 엔치등스프로블렘(Alonzo Churchitect와 Alan Turing의 1930년대)에 대한 부정적 해결책에서 비롯된다.또한 모든 그래프에 맞는 1차 문장과 유한 그래프에 해당하지만 일부 무한 그래프에 대해서는 거짓인 문장을 구분하는 것도 불분명하다.^[19]null

고정점

그래프의 최소 고정점 기반 로직은 특수 고정점 연산자가 정의한 술어를 허용함으로써 그래프의 1차 논리를 확장하는데, 술어는 술어의 값을 동일한 술어의 다른 값과 연관시키는 공식의 고정점으로 정의한다.예를 들어, $C{\displaystyle (u}$, v${\displaystyle }$) ${\displaystyle C(u,v)}$이(가) 주어진$$ 그래프에서 한 경로로 두 정점이 연결되었는지 여부를 결정하는 술어라면, $C{\displaystyle }$ ${\displaystyle C}$은 공식의 최소 고정점이다.

${\displaystyle C(u,v)\왼쪽 화살표 {\Bigl (}u=v)\vee \exists w{\bigl (}C(u,w)\wedge w\sim v{\bigr )}{\Bigr )}.}$

여기서 고정점이 된다는 것은 공식의 우측의 진리가 (역 함축적 함축적 화살이 시사하는 바와 같이) 좌측의 진리를 내포한다는 것을 의미한다.가장 적게 고정되었다는 것은 $C{\displaystyle }$ ${\displaystyle C}$이 참인$$ 정점 쌍이 동일한 공식의 다른 고정점이 참인 정점 쌍의 부분 집합임을 의미한다.최소 고정점 논리학에서 정의 공식의 오른쪽은 최소한의 고정점을 잘 정의하기 위해 술어를 양적으로만 사용해야 한다(즉, 각 외형은 짝수 부정 내에 내포되어야 한다).등가 변종인 인플레이션 고정점 논리에서는 공식이 단조로울 필요는 없지만, 결과 고정점은 모든 거짓 술어에서 시작하는 정의 공식에서 파생된 함축적 의미를 반복적으로 적용하여 얻은 것으로 정의된다.부정적인 함축이나 복수의 동시에 정의된 술어를 허용하는 다른 변형도 가능하지만 추가적인 정의 힘을 제공하지 않는다.이러한 방법 중 하나로 정의되는 술어는 더 큰 논리 문장의 일부로 정점의 튜플에 적용될 수 있다.^[20]null

고정 점 로직과 값이 0에서 정점 수까지 범위의 정수 계산 변수를 허용하는 이러한 로직의 확장은 다항 시간에서 결정할 수 있는 그래프 이론의 의사결정 문제에 대한 논리적 설명을 제공하기 위해 서술적 복잡성에 사용되어 왔다.논리 공식의 고정점은 다항 시간, 즉 고정점에 도달할 때까지 술어가 참인 값 집합에 튜플을 반복적으로 추가하는 알고리즘에 의해 구성될 수 있으므로, 그래프가 항상 다항 시간 내에 문장을 모델링하는지를 결정할 수 있다.모든 다항 시간 그래프 속성을 고정된 점과 계수만 사용하는 논리에서 문장으로 모델링할 수 있는 것은 아니다.^[21][22]그러나 일부 그래프의 특수 클래스의 경우 다항식 시간 속성은 카운트가 있는 고정 점 논리로 표현 가능한 속성과 동일하다.여기에는 무작위 그래프,^[21][23] 구간 그래프,^[21][24] 그리고 (그래프 구조 정리의 논리적인 표현을 통해) 금지된 미성년자로 특징지어지는 모든 종류의 그래프가 포함된다.^[21]null

두 번째 순서

그래프의 단조로운 2차 논리학에서 변수는 정점, 가장자리, 정점 집합, 가장자리 집합의 최대 4가지 유형의 객체를 나타낸다.단차 2차 그래프 논리에는 정점 및 정점 설정 변수만 허용되는₁ MSO와 네 가지 유형의 변수를 모두 허용하는 MSO의₂ 두 가지 주요한 변화가 있다.이러한 변수의 술어로는 동등성 검정, 멤버십 검사 및 정점-가장자리 발생(정점 및 가장자리 변수가 모두 허용되는 경우) 또는 정점 쌍 사이의 인접성(정점 변수만 허용되는 경우)이 있다.정의의 추가 변동은 모듈식 계산 술어와 같은 추가 술어를 허용한다.null

예

예를 들어, 비방향 그래프의 연결은 MSO로₁ 표현될 수 있다. 즉, 정점의 모든 파티션에 대해 두 개의 비어 있지 않은 하위 집합으로, 한 부분 집합에서 다른 부분 집합으로 에지가 존재한다는 것이다.정점의 파티션은 파티션의 한 쪽에 있는 정점의 부분 집합 S로 설명될 수 있으며, 그러한 부분 집합 각각은 사소한 파티션(하나 또는 다른 한쪽이 비어 있는 경우)을 설명하거나 가장자리에 의해 교차되어야 한다.즉, MSO₁ 문장을 모델링할 때 그래프가 연결된다.

${\displaystyle \forall S{\Bigl (}\forall x(x\in S)\vee \forall y{\bigl (}\lnot (y\in S){\bigr )}\vee \exists x\exists y{\bigl (}x\in S\wedge \lnot (y\in S)\wedge x\sim y{\bigr )}{\Bigr )}.}$

그러나 연결은 1차 그래프 논리로 표현할 수 없으며, 실존적 MSO₁(모든 정해진 정량자가 실존적이고 문장 시작에 일어나는 MSO의₁ 단편)에서도 실존적 MSO로₂ 표현할 수 없다.^[25]

해밀턴성은 모든 정점에 연결된 2-정규 그래프를 형성하는 일련의 에지가 존재하여 MSO로₂ 표현할 수 있으며, 연결성은 위와 같이 표현되고 2-정규성은 각 정점마다 뚜렷이 구별되는 두 에지의 발생으로 표현된다.그러나 MSO에서는₁ MSO가 양분(해밀턴어) 양쪽에 정점 수가 같은 완전 양분 그래프와 불균형 전체 양분 그래프(해밀턴어)를 구분할 수 없기 때문에 해밀턴성은 MSO에서₁ 표현할 수 없다.^[26]null

MSO의₂ 정의에 속하지는 않지만, 방향 지정되지 않은 그래프의 방향은 Tremaux 트리를 포함하는 기법으로 표현될 수 있다.이를 통해 방향과 관련된 다른 그래프 속성도 표시할 수 있다.^[27]null

쿠르셀의 정리

Courcelle의 정리에 따르면, 모든 고정 MSO₂ 속성은 경계 트리 너비 그래프에서 선형 시간 내에 테스트할 수 있으며, 모든 고정 MSO₁ 속성은 경계 클라이크 너비 그래프에서 선형 시간 내에 테스트할 수 있다.^[28]경계 트리 너비의 그래프에 대한 이 결과의 버전은 로그 공간에서 구현될 수도 있다.^[29]이 결과의 적용에는 그래프의 교차 숫자를 계산하기 위한 고정 매개변수 추적 가능한 알고리즘이 포함된다.^[30]null

세스의 정리

단조로운 2차 논리 문장에 대한 만족도 문제는 문장이 참인 그래프 하나(아마도 제한된 그래프 계열 내에)가 하나 이상 존재하는지 여부를 판단하는 문제다.임의 그래프 패밀리와 임의 문장의 경우, 이 문제는 이해할 수 없다.그러나 MSO₂ 문장의 만족도는 경계 트리 너비의 그래프에 대해 결정 가능하며, 경계 클릭 너비의 그래프에 대해서는 MSO₁ 문장의 만족도가 결정된다.그 증거는 Courcelle의 정리를 이용하여 그 성질을 시험할 수 있는 자동화를 만든 다음, 그 자동화를 검토하여 그것이 받아들일 수 있는 어떤 그래프가 있는지 결정하는 것을 포함한다.null

부분적인 반대로, Seees(1991)는 그래프 가족이 MSO₂ 만족도를 결정할 수 있는 문제를 가질 때마다, 그 가족이 트리 너비를 경계해야 한다는 것을 증명했다.그 증거는 무한 트리 너비를 가진 그래프 집단이 임의로 큰 격자 마이너스를 가지고 있다는 로버슨과 세이모어의 정리를 바탕으로 한다.See는 또한 MSO₁ 만족도 문제를 해결할 수 있는 모든 그래프 제품군이 clique-width를 경계했을 것이라고 추측했다; 이것은 입증되지 않았지만 모듈식 계산 술어로 MSO를₁ 확장하는 추측의 약화는 사실이다.^[31]null

메모들

참조