쿠셀의 정리

Courcelle's theorem

그래프 알고리즘의 연구에서, Courcelle의 정리는 그래프의 모노딕 2차 논리에서 정의 가능한 모든 그래프 특성은 유계 트리 [1][2][3]폭의 그래프에서 선형 시간으로 결정될 수 있다는 진술이다.이 결과는 1990년[4] 브루노 쿠셀에 의해 처음 증명되었고 보리, 파커, 토비(1992)[5]에 의해 독립적으로 재발견되었다.그것은 알고리즘 메타 [6][7]이론의 원형으로 여겨진다.

제제

정점 집합

단항의 2차 그래프 논리 MSO1으로 알려져의 한 변이에서, 그래프 vertices 일련의 이진 인접 관계 adj⁡(.,.){\displaystyle \operatorname{adj}(.,.)}, 단항의 논리는 문제의 그래프 속성은 주어진 gra의 vertices 세트 측면에서 정의될 수 있다는 의미로 설명합니다.ph. 단, 모서리 집합이나 꼭지점 튜플 집합은 제외됩니다.

예를 들어, 3가지 색상으로 색칠할 수 있는 그래프의 속성은( R R G B B의 3가지 세트로 표시됨) 모노디드 2차 공식으로 정의할 수 있습니다.

대문자 변수는 정점 집합을 나타내며 소문자 변수는 개별 정점을 나타냅니다(따라서 공식에서 생략할 수 있는 명시적 선언이 있음).이 공식의 첫 번째 부분은 세 가지 색 클래스가 그래프의 모든 정점을 커버하고 나머지 부분은 각각 독립된 집합을 형성하도록 합니다.(세 가지 색 클래스가 분리되도록 공식에 절을 추가할 수도 있지만, 이 경우에도 결과에 차이가 없습니다.)따라서, Courcelle의 정리에 의해, 유계수 폭의 그래프의 3색성은 선형 시간 내에 시험될 수 있다.

그래프 논리에 변화 들어, Courcelle의 정리 treewidth에서 clique-width 모든 고정 MSO1 속성 Π{\displaystyle \Pi}을 도울 것이며, 온갖 그래프의 clique-width에게 덤벼들다 b{\displaystyle b}고정, clique-width의 대부분의 b{\displays에서 그래프인지 시험을 위한linear-time 알고리즘은 연장될 수 있다.tb는 속성\Pi[8]를 가지고 있습니다.이 결과의 최초 공식에서는 입력 그래프가 clique-width에 경계가 있음을 증명하는 구성과 함께 제공되어야 했지만 나중에 clique-width에 대한 근사 알고리즘에 의해 이 [9]요건이 삭제되었습니다.

가장자리 세트

또한 Courcelle의 정리는 MSO로2 알려진 단항 2차 논리의 보다 강력한 변형과 함께 사용될 수 있습니다. 이 공식에서 그래프는 정점의 집합 V, 모서리의 집합 E 및 정점과 모서리 사이의 입사 관계로 나타납니다.이 변동은 정점 또는 모서리 집합에 대한 정량화를 허용하지만 정점 또는 모서리의 튜플에 대한 보다 복잡한 관계는 허용하지 않습니다.

예를 들어, 해밀턴 사이클을 갖는 특성은 MSO에서2 각 정점에 입사하는 정확히 두 개의 에지를 포함하는 에지의 집합으로 설명함으로써 표현될 수 있으며, 따라서 정점의 모든 비어 있지 않은 고유 서브셋은 추정 사이클에서 에지를 가지며 서브셋에 정확히 하나의 끝점을 가진다.그러나 해밀턴시티는 MSO로1 [10]표현할 수 없습니다.

라벨이 붙은 그래프

정점 또는 모서리에 고정된 유한 집합의 라벨이 있는 그래프에 동일한 결과를 적용할 수 있습니다.그래프 로직을 확장하여 라벨을 기술하는 술어를 포함하거나, 또는 정량화되지 않은 정점 집합 또는 가장자리 집합 [11]변수로 라벨을 표시함으로써 가능합니다.

모듈러 조합

Courcelle의 정리를 확장하기 위한 또 다른 방향은 테스트의 크기를 세기 위한 술어를 포함하는 논리 공식에 관한 것입니다.이 문맥에서는 세트 사이즈에 대해 임의의 산술 연산을 실행할 수 없습니다.또, 2 세트의 사이즈가 같은지를 테스트할 수도 없습니다.단1, MSO 및 MSO는2 CMSO 및2 CMSO라고 불리는1 로직으로 확장할 수 있습니다.이 로직에는 2개의 상수 q 및 에 대해 r ( S )\displaystyle { (S가 포함되어 있습니다.이는 세트S의 카디널리티가 모듈 Qul's에 일치하는지 여부를 테스트합니다.

의사결정과 최적화

위에서 설명한 바와 같이, Courcelle의 정리는 주로 결정 문제에 적용된다: 그래프가 속성을 가지고 있는지 여부.그러나 같은 방법을 사용하면 그래프의 꼭지점 또는 모서리가 정수 가중치를 가지며, 2차 논리로 표현되는 주어진 속성을 만족시키는 최소 또는 최대 가중치 정점 집합을 찾는 최적화 문제도 해결할 수 있습니다.이러한 최적화 문제는 경계된 클리크 [8][11]폭의 그래프에서 선형 시간 내에 해결할 수 있습니다.

공간의 복잡성

MSO 속성을 인식하는 알고리즘의 시간 복잡성을 경계하는 대신, 그러한 알고리즘의 공간 복잡성을 분석할 수도 있습니다. 즉, 입력 자체의 크기 이상에서 필요한 메모리의 양(공간이 다시 저장되도록 읽기 전용 방식으로 표현되는 것으로 가정됨)요건을 다른 목적에 적용할 수 없다.)특히, 로그 [12]공간만을 사용하는 결정론적 튜링 기계에 의해 유계 트리 폭의 그래프와 이러한 그래프상의 MSO 속성을 인식할 수 있다.

입증 전략 및 복잡성

Courcelle의 정리를 증명하기 위한 전형적인 접근법은 주어진 [6]그래프의 나무 분해에 작용하는 유한한 상향식 나무 자동화의 구성을 포함한다.

In more detail, two graphs G1 and G2, each with a specified subset T of vertices called terminals, may be defined to be equivalent with respect to an MSO formula F if, for all other graphs H whose intersection with G1 and G2 consists only of vertices in T, the two graphs G1 ∪ H and G2 ∪ H behave the same with respect to F: either they both model F 또는둘 다 F를 모형화하지 않습니다.이것은 동등성 관계이며, F의 길이에 대한 유도(T와 F의 크기가 둘 다 유계일 때)에 의해 완전히 많은 동등성 [13]클래스가 있음을 나타낼 수 있다.

주어진 그래프 G의 트리 분해는 트리 및 각 트리 노드에 대해 가방이라고 불리는 G의 정점의 서브셋으로 구성된다.G의 각 정점 v에 대해 v를 포함하는 백은 트리의 연속된 서브트리와 관련지어져야 하며, G의 각 가장자리 uv에 대해 u와 v를 모두 포함하는 백이 있어야 한다.가방의 정점은 가방에서 내려오는 나무 분해의 하위 트리로 표현되는 G의 하위 그래프의 끝이라고 생각할 수 있다.G가 유계 트리 폭을 갖는 경우, 모든 가방이 유계 크기를 갖는 트리 분해를 가지며, 그러한 분해를 고정 파라미터 추적 [14]가능 시간으로 찾을 수 있다.또한 이 트리 분해를 선택하여 가방당 2개의 하위 트리만 포함하는 이진 트리를 형성할 수 있습니다.따라서 이 트리 분해에 대해 보텀업 연산을 실시할 수 있으며, 가방 내에서 표현되는 에지와 그 두 [15]자녀의 등가 클래스에 대한 2개의 식별자를 조합함으로써 각 봉투에 뿌리를 둔 서브트리의 등가 클래스에 대한 식별자를 산출할 수 있다.

이렇게 구성된 오토마톤의 크기는 입력 MSO 공식 크기의 기본 함수가 아닙니다.([16]P = NP가 아닌 한) 매개변수에 대한 기본 의존성으로 추적 가능한 고정 매개변수 시간에 나무에 대한 MSO 특성을 테스트할 수 없다는 점에서 이러한 비원칙적인 복잡성이 필요하다.

보야시크필립추크의 정리

Courcelle의 정리의 증명은 더 강력한 결과를 보여준다: 모든 (계수하는) 단수 2차 특성은 유계 트리 폭의 그래프에 대해 선형 시간으로 인식될 수 있을 뿐만 아니라 유한 상태 트리 오토마톤에 의해서도 인식될 수 있다.Courcelle은 이와 반대로 추측했다: 만약 나무 폭의 유계 그래프의 특성이 나무 오토마톤에 의해 인식된다면, 그것은 단일한 2차 논리를 세는 데 정의될 수 있다.1998년 라푸아르(1998년)는 [17]추측의 해결을 주장했다.하지만, 그 증거는 [18][19]만족스럽지 못한 것으로 널리 받아들여지고 있다.2016년까지 몇 가지 특별한 경우만 해결되었다. 특히, 추측은 최대 [20]3개의 나무 너비 그래프, k-연결된 나무 너비 k 그래프, 일정한 나무 너비 및 화음의 그래프, k-외측 평면 그래프에 대해 입증되었다.추측의 일반적인 버전은 미코와이 보야치크와 미하우 필리프추크에 [21]의해 마침내 증명되었다.

게다가 할린 그래프(트리 폭 3개의 그래프의 특별한 경우)의 경우 카운트가 필요하지 않다. 이러한 그래프의 경우 트리 자동화에 의해 인식될 수 있는 모든 속성은 모노딕 2차 논리로 정의될 수 있다.MSOL에서 트리 분해 자체를 기술할 수 있는 특정 클래스의 그래프에 대해서도 일반적으로 동일합니다.그러나 일반적으로 카운트하지 않고 모노딕 2차 로직 위에 추가 파워를 추가하기 때문에 경계 트리 폭의 모든 그래프에 해당될 수는 없습니다.예를 들어, 짝수 정점이 있는 그래프는 카운트를 사용하여 인식할 수 있지만 [19]없으면 인식할 수 없습니다.

만족도와 세스의 정리

모노딕 2차 논리의 공식에 대한 만족도 문제는 공식이 참인 그래프가 적어도 하나(제한된 그래프 패밀리 내에) 존재하는지 여부를 결정하는 문제이다.임의의 그래프 패밀리와 임의의 공식의 경우 이 문제는 판별할 수 없습니다.그러나 MSO2 공식의 만족도는 유계 트리 폭의 그래프에 대해 결정 가능하며 MSO 공식의1 만족도는 유계 클리크 폭의 그래프에 대해 결정 가능하다.증명에는 공식에 대한 트리 오토마톤을 구축하고 오토마톤이 수용 경로를 가지고 있는지 여부를 테스트하는 것이 포함됩니다.

부분적 대화로, Seese(1991)는 그래프 집단이 결정 가능한2 MSO 만족도 문제를 가질 때마다 집단은 제한적인 나무 폭을 가져야 한다는 것을 증명했다.그 증거는 무한 트리 폭을 가진 그래프 패밀리가 임의로 큰 [22]그리드 마이너리티를 갖는다는 로버트슨과 시모어의 정리에 기초한다.Seese는 또한 결정 가능한 MSO1 만족도 문제가 있는 모든 그래프 패밀리가 경계 집단폭을 가져야 한다고 추측했다. 이는 증명되지 않았지만 MSO를 CMSO로1 대체하는1 추측의 약화는 사실이다.[23]

적용들

Grohe(2001)는 그래프 G의 교차 수를 계산하는 것이 G의 크기에 대한 2차 의존성과 함께 고정 매개변수를 다루기 쉽다는 것을 보여주기 위해 Courcelle의 정리를 사용하여 로버트슨에 기초한 입방 시간 알고리즘을 개선했다.시모어 정리.Kawarabayashi & Reed(2007)의 리니어 타임에 대한 추가 개선도 같은 접근방식을 따른다.주어진 그래프 G의 나무 폭이 작으면 Courcelle의 정리를 이 문제에 직접 적용할 수 있다.한편, G가 큰 트리폭을 가지고 있는 경우는, 큰 그리드를 포함하고 있기 때문에, 교차수를 변경하지 않고 그래프를 단순화할 수 있다.Grohe의 알고리즘은 나머지 그래프가 작은 트리폭을 가질 때까지 이러한 단순화를 수행한 후 Courcelle의 정리를 적용하여 축소된 하위 [24][25]문제를 해결합니다.

Gottlob & Lee(2007)는 Courcelle의 정리가 그래프와 절단 쌍의 집합에 의해 형성된 구조가 나무 너비에 경계를 가지고 있을 때 그래프에서 최소 다중 방향 절단을 찾는 몇 가지 문제에 적용된다고 관찰했다.그 결과, 이러한 문제에 대해 단일 매개 변수인 트리 폭에 의해 매개 변수화된 고정 매개 변수 추적 가능한 알고리즘을 얻어 여러 [26]매개 변수를 결합했던 이전 솔루션을 개선합니다.

컴퓨터 토폴로지에서 Burton & Downey(2014)는 MSO에서2 임의의 고정 차원보다 계량화할 수 있는 유계 차원의 단순 복합체에 대한 모노딕 2차 논리의 형태로 Courcelle의 정리를 확장한다.결과적으로, 그들은 다지관이 이중 그래프가 작은 삼각 [27]측량(퇴화 단순화를 회피)을 가지고 있을 때, 3-매니폴드의 특정 양자 불변량을 계산하는 방법과 이산 모스 이론의 특정 문제를 효율적으로 해결하는 방법을 보여준다.

쿠셀의 정리에 기초한 방법은 데이터베이스 이론,[28] 지식 표현 및 추론,[29] 오토마타 이론,[30] 모델 확인에도 적용되어 [31]왔다.

레퍼런스

  1. ^ 를 클릭합니다Eger, Steffen (2008), Regular Languages, Tree Width, and Courcelle's Theorem: An Introduction, VDM Publishing, ISBN 9783639076332.
  2. ^ 를 클릭합니다Courcelle, Bruno; Engelfriet, Joost (2012), Graph Structure and Monadic Second-Order Logic: A Language-Theoretic Approach (PDF), Encyclopedia of Mathematics and its Applications, vol. 138, Cambridge University Press, ISBN 9781139644006, Zbl 1257.68006.
  3. ^ 를 클릭합니다Downey, Rodney G.; Fellows, Michael R. (2013), "Chapter 13: Courcelle's theorem", Fundamentals of parameterized complexity, Texts in Computer Science, London: Springer, pp. 265–278, CiteSeerX 10.1.1.456.2729, doi:10.1007/978-1-4471-5559-1, ISBN 978-1-4471-5558-4, MR 3154461, S2CID 23517218.
  4. ^ a b Courcelle, Bruno (1990), "The monadic second-order logic of graphs. I. Recognizable sets of finite graphs", Information and Computation, 85 (1): 12–75, doi:10.1016/0890-5401(90)90043-H, MR 1042649, Zbl 0722.03008
  5. ^ 를 클릭합니다Borie, Richard B.; Parker, R. Gary; Tovey, Craig A. (1992), "Automatic generation of linear-time algorithms from predicate calculus descriptions of problems on recursively constructed graph families", Algorithmica, 7 (5–6): 555–581, doi:10.1007/BF01758777, MR 1154588, S2CID 22623740.
  6. ^ a b 를 클릭합니다Kneis, Joachim; Langer, Alexander (2009), "A practical approach to Courcelle's theorem", Electronic Notes in Theoretical Computer Science, 251: 65–81, doi:10.1016/j.entcs.2009.08.028.
  7. ^ 를 클릭합니다Lampis, Michael (2010), "Algorithmic meta-theorems for restrictions of treewidth", in de Berg, Mark; Meyer, Ulrich (eds.), Proc. 18th Annual European Symposium on Algorithms, Lecture Notes in Computer Science, vol. 6346, Springer, pp. 549–560, doi:10.1007/978-3-642-15775-2_47, Zbl 1287.68078.
  8. ^ a b 를 클릭합니다Courcelle, B.; Makowsky, J. A.; Rotics, U. (2000), "Linear time solvable optimization problems on graphs of bounded clique-width", Theory of Computing Systems, 33 (2): 125–150, CiteSeerX 10.1.1.414.1845, doi:10.1007/s002249910009, MR 1739644, S2CID 15402031, Zbl 1009.68102.
  9. ^ 를 클릭합니다Oum, Sang-il; Seymour, Paul (2006), "Approximating clique-width and branch-width", Journal of Combinatorial Theory, Series B, 96 (4): 514–528, doi:10.1016/j.jctb.2005.10.006, MR 2232389.
  10. ^ Courcelle & Engelfriet(2012), 제안 5.13, 페이지 338.
  11. ^ a b 를 클릭합니다Arnborg, Stefan; Lagergren, Jens; Seese, Detlef (1991), "Easy problems for tree-decomposable graphs", Journal of Algorithms, 12 (2): 308–340, CiteSeerX 10.1.1.12.2544, doi:10.1016/0196-6774(91)90006-K, MR 1105479.
  12. ^ 를 클릭합니다Elberfeld, Michael; Jakoby, Andreas; Tantau, Till (October 2010), "Logspace Versions of the Theorems of Bodlaender and Courcelle" (PDF), Proc. 51st Annual IEEE Symposium on Foundations of Computer Science (FOCS 2010), pp. 143–152, doi:10.1109/FOCS.2010.21, S2CID 1820251.
  13. ^ 다우니 & 펠로우즈 (2013), 정리 13.1.1, 페이지 266.
  14. ^ 다우니 & 펠로우즈 (2013), 섹션 10.5: 보드렌더의 정리, 페이지 195–203.
  15. ^ 다우니 & 펠로우즈 (2013), 섹션 12.6: 트리 오토마타, 페이지 237–247.
  16. ^ 를 클릭합니다Frick, Markus; Grohe, Martin (2004), "The complexity of first-order and monadic second-order logic revisited", Annals of Pure and Applied Logic, 130 (1–3): 3–31, doi:10.1016/j.apal.2004.01.007, MR 2092847.
  17. ^ 를 클릭합니다Lapoire, Denis (1998), "Recognizability equals monadic second-order definability for sets of graphs of bounded tree-width", STACS 98: 15th Annual Symposium on Theoretical Aspects of Computer Science Paris, France, February 27, 1998, Proceedings, pp. 618–628, Bibcode:1998LNCS.1373..618L, CiteSeerX 10.1.1.22.7805, doi:10.1007/bfb0028596.
  18. ^ 를 클릭합니다Courcelle, B.; Engelfriet., J. (2012), "Graph Structure and Monadic Second Order Logic -- A Language-Theoretic Approach", Encyclopedia of mathematics and its applications, vol. 138, Cambridge University Press.
  19. ^ a b 를 클릭합니다Jaffke, Lars; Bodlaender, Hans L. (2015), MSOL-definability equals recognizability for Halin graphs and bounded degree k-outerplanar graphs, arXiv:1503.01604, Bibcode:2015arXiv150301604J.
  20. ^ 를 클릭합니다Kaller, D. (2000), "Definability equals recognizability of partial 3-trees and k-connected partial k-trees", Algorithmica, 27 (3): 348–381, doi:10.1007/s004530010024, S2CID 39798483.
  21. ^ 를 클릭합니다Bojańczyk, Mikołaj; Pilipczuk, Michał (2016), "Definability equals recognizability for graphs of bounded treewidth", Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2016), pp. 407–416, arXiv:1605.03045, doi:10.1145/2933575.2934508, S2CID 1213054.
  22. ^ 를 클릭합니다Seese, D. (1991), "The structure of the models of decidable monadic theories of graphs", Annals of Pure and Applied Logic, 53 (2): 169–195, doi:10.1016/0168-0072(91)90054-P, MR 1114848.
  23. ^ 를 클릭합니다Courcelle, Bruno; Oum, Sang-il (2007), "Vertex-minors, monadic second-order logic, and a conjecture by Seese" (PDF), Journal of Combinatorial Theory, Series B, 97 (1): 91–126, doi:10.1016/j.jctb.2006.04.003, MR 2278126.
  24. ^ 를 클릭합니다Grohe, Martin (2001), "Computing crossing numbers in quadratic time", Proceedings of the Thirty-Third Annual ACM Symposium on Theory of Computing (STOC '01), pp. 231–236, arXiv:cs/0009010, doi:10.1145/380752.380805, S2CID 724544.
  25. ^ 를 클릭합니다Kawarabayashi, Ken-ichi; Reed, Bruce (2007), "Computing crossing number in linear time", Proceedings of the Thirty-Ninth Annual ACM Symposium on Theory of Computing (STOC '07), pp. 382–390, doi:10.1145/1250790.1250848, S2CID 13000831.
  26. ^ 를 클릭합니다Gottlob, Georg; Lee, Stephanie Tien (2007), "A logical approach to multicut problems", Information Processing Letters, 103 (4): 136–141, doi:10.1016/j.ipl.2007.03.005, MR 2330167.
  27. ^ 짧은 커뮤니케이션, 국제 수학자 콩그레스, 2014Burton, Benjamin A.; Downey, Rodney G. (2014), Courcelle's theorem for triangulations, arXiv:1403.2926, Bibcode:2014arXiv1403.2926B.
  28. ^ 를 클릭합니다Grohe, Martin; Mariño, Julian (1999), "Definability and descriptive complexity on databases of bounded tree-width", Database Theory — ICDT'99: 7th International Conference Jerusalem, Israel, January 10–12, 1999, Proceedings, Lecture Notes in Computer Science, vol. 1540, pp. 70–82, CiteSeerX 10.1.1.52.2984, doi:10.1007/3-540-49257-7_6.
  29. ^ 를 클릭합니다Gottlob, Georg; Pichler, Reinhard; Wei, Fang (January 2010), "Bounded treewidth as a key to tractability of knowledge representation and reasoning", Artificial Intelligence, 174 (1): 105–132, doi:10.1016/j.artint.2009.10.003.
  30. ^ Madhusudan, P.; Parlato, Gennaro (2011), "The Tree Width of Auxiliary Storage", Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL '11) (PDF), SIGPLAN Notices, vol. 46, pp. 283–294, doi:10.1145/1926385.1926419, S2CID 6976816
  31. ^ 를 클릭합니다Obdržálek, Jan (2003), "Fast mu-calculus model checking when tree-width is bounded", Computer Aided Verification: 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, Lecture Notes in Computer Science, vol. 2725, pp. 80–92, CiteSeerX 10.1.1.2.4843, doi:10.1007/978-3-540-45069-6_7.