Логика графиков - Logic of graphs

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

Предложение может быть верным для одних графиков и ложным для других; граф называется модельным , записывается , если верно для вершин и отношения смежности графа . Алгоритмическая проблема проверки модели касается проверки того, моделирует ли данный граф данное предложение. Алгоритмическая проблема выполнимости касается проверки того, существует ли граф, моделирующий данное предложение. Хотя проверка модели и выполнимость в целом сложны, несколько основных алгоритмических мета-теорем показывают, что свойства, выраженные таким образом, могут быть эффективно протестированы для важных классов графов. ${\ displaystyle S}$${\ displaystyle G}$ ${\ displaystyle S}$${\ displaystyle G \ models S}$${\ displaystyle S}$${\ displaystyle G}$

Другие темы исследований в области логики графов включают исследования вероятности того, что случайный граф имеет свойство, заданное в рамках определенного типа логики, и методы сжатия данных, основанные на поиске логических предложений, которые моделируются уникальным графом.

Первый заказ

Показанный здесь граф появляется как подграф неориентированного графа тогда и только тогда, когда моделирует предложение .${\ displaystyle G}$${\ displaystyle G}$${\ displaystyle \ exists x_ {1}, x_ {2}, x_ {3}, x_ {4}.}$ ${\ displaystyle x_ {1} \ sim x_ {2}}$ ${\ displaystyle \ land}$ ${\ displaystyle x_ {2} \ sim x_ {3}}$ ${\ displaystyle \ land}$ ${\ displaystyle x_ {3} \ sim x_ {1}}$ ${\ displaystyle \ land}$ ${\ displaystyle x_ {3} \ sim x_ {4}}$ ${\ displaystyle \ land}$ ${\ displaystyle x_ {1} \ neq x_ {4}}$ ${\ displaystyle \ land}$ ${\ displaystyle x_ {2} \ neq x_ {4}}$

В логике графов первого порядка свойство графа выражается как количественное логическое предложение, переменные которого представляют вершины графа , с предикатами для проверки равенства и смежности.

Примеры

Например, условие, что граф не имеет изолированных вершин, может быть выражено предложением

${\ Displaystyle \ forall и \ существует v (и \ сим v)}$

где символ указывает на неориентированное отношение смежности между двумя вершинами. Это предложение можно интерпретировать как означающее, что для каждой вершины есть другая вершина, которая смежна . ${\ displaystyle \ sim}$${\ displaystyle u}$${\ displaystyle v}$${\ displaystyle u}$

Проблема подграфа изоморфизма для фиксированного подграфа H спрашивает , может ли Н появляется в качестве подграфа большего графа G . Это может быть выражено предложением, в котором говорится о существовании вершин (по одной для каждой вершины H ) таких, что для каждого ребра H соответствующая пара переменных представляет смежные вершины, и такие, что для каждой оставшейся пары вершин H , соответствующая пара переменных представляет различные вершины; см. иллюстрацию. В качестве особого случая проблема клики (для фиксированного размера клики) может быть выражена предложением, в котором говорится о существовании числа вершин, равного размеру клики, все из которых являются смежными.

Аксиомы

Для простых неориентированных графов теория графов первого порядка включает аксиомы

${\ Displaystyle \ forall и {\ bigl (} \ lnot (и \ сим и) {\ bigr)}}$(граф не может содержать петель ) и

${\ Displaystyle \ forall и \ forall v (и \ sim v \ Rightarrow v \ sim u)}$ (края неориентированные).

Другие типы графов, такие как ориентированные графы , могут включать другие аксиомы, а логические формулировки свойств мультиграфов требуют специальной обработки, такой как наличие нескольких отношений ребер или отдельных переменных для вершин и ребер.

Закон нуля или единицы

Граф Радо , бесконечный граф, который моделирует в точности предложения первого порядка, которые почти всегда верны для конечных графов.

Glebski et al. (1969) и, независимо, Фэгин (1976) доказали закон нуля или единицы для логики графов первого порядка; В доказательстве Феджина использовалась теорема компактности . Согласно этому результату каждое предложение первого порядка либо почти всегда истинно, либо почти всегда ложно для случайных графов в модели Эрдеша – Реньи . То есть, пусть S будет фиксированным предложением первого порядка, и выберите случайный граф G _{n с} n- вершинами равномерно случайным образом среди всех графов на множестве n помеченных вершин. Тогда в пределе, когда n стремится к бесконечности, вероятность того, что G _n моделей S будет стремиться либо к нулю, либо к единице:

${\ displaystyle \ lim _ {n \ to \ infty} \ operatorname {Pr} [G_ {n} \ models S] \ in \ {0,1 \}.}$

Более того, существует конкретный бесконечный граф, граф Радо R , такой, что предложения, моделируемые графом Радо, являются именно теми, для которых вероятность моделирования случайным конечным графом стремится к единице:

${\ displaystyle R \ models S \ quad \ Longleftrightarrow \ quad \ lim _ {n \ to \ infty} \ operatorname {Pr} [G_ {n} \ models S] = 1.}$

Для случайных графов, в которых каждое ребро включено независимо от других с фиксированной вероятностью, верен тот же результат, с теми же предложениями, имеющими вероятности, стремящиеся к нулю или к единице.

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

Аналогичный анализ может быть выполнен для неоднородных случайных графов, где вероятность включения ребра является функцией количества вершин и где решение о включении или исключении ребра принимается независимо с равной вероятностью для всех ребер. Однако для этих графиков ситуация более сложная. В этом случае свойство первого порядка может иметь один или несколько порогов, так что, когда вероятность включения края ограничена от порога, тогда вероятность наличия данного свойства стремится к нулю или единице. Эти пороги никогда не могут быть иррациональной степенью n , поэтому случайные графы, в которых вероятность включения ребер является иррациональной степенью, подчиняются закону нуля или единицы, аналогичному закону для равномерно случайных графов. Похожий закон нуля или единицы выполняется для очень разреженных случайных графов, которые имеют вероятность включения ребер n ^{- c} с c  > 1 , если c не является суперпредметным отношением . Если c является сверхчастичным, вероятность наличия данного свойства может стремиться к пределу, который не равен нулю или единице, но этот предел можно эффективно вычислить. Существуют предложения первого порядка, у которых бесконечно много порогов.

Параметризованная сложность

Если предложение первого порядка включает k различных переменных, то свойство, которое оно описывает, можно проверить на графах из n вершин, исследуя все k -наборы вершин; однако этот алгоритм поиска методом грубой силы не особенно эффективен и требует времени O ( n ^k ) . Проблема проверки того, моделирует ли граф данное предложение первого порядка, включает в качестве частных случаев проблему изоморфизма подграфов (в которой предложение описывает графы, содержащие фиксированный подграф) и проблему клики (в которой предложение описывает графы, содержащие полные подграфы фиксированного размера). Проблема клики сложна для W (1) , первого уровня иерархии сложных проблем с точки зрения параметризованной сложности . Следовательно, маловероятно иметь управляемый алгоритм с фиксированными параметрами, время работы которого принимает форму O ( f ( k )  n ^c ) для функции f и константы c, которые не зависят от k и n . Более того, если гипотеза экспоненциального времени верна, то поиск кликов и проверка модели первого порядка обязательно потребуют времени, пропорционального степени n , показатель степени которой пропорционален k .

На ограниченных классах графов проверка моделей предложений первого порядка может быть намного более эффективной. В частности, каждое свойство графа, выражаемое как предложение первого порядка, может быть проверено за линейное время для графов ограниченного расширения . Это графы, в которых все мелкие миноры являются разреженными графами с отношением ребер к вершинам, ограниченным функцией глубины минора. В более общем смысле, проверка модели первого порядка может выполняться за почти линейное время для нигде не плотных графов, классов графов, для которых на каждой возможной глубине есть по крайней мере один запрещенный мелкий второстепенный. И наоборот, если проверка модели является управляемой с фиксированными параметрами для любого наследственного семейства графов, это семейство должно быть нигде не плотным.

Сжатие данных и изоморфизм графов

Первого порядка предложение S в логике графов называется определить граф G , если G является единственным , что граф модели S . Каждый граф может быть определен по крайней мере одним предложением; например, можно определить граф G с n вершинами с помощью предложения с n  + 1 переменными, по одной для каждой вершины графа, и еще одним, чтобы установить условие, что нет вершины, кроме n вершин графа. Дополнительные пункты в предложении могут быть использованы , чтобы гарантировать , что никакие две переменные вершины не равны, что каждое ребро G присутствует, и ни одно ребро не существует между парой несмежных вершин G . Однако для некоторых графов существуют значительно более короткие предложения, определяющие граф.

Несколько различных инвариантов графов могут быть определены из простейших предложений (с разными мерами простоты), которые определяют данный граф. В частности, логическая глубина графа определяется как минимальный уровень вложенности кванторов ( ранг кванторов ) в предложение, определяющее граф. Вышеупомянутое предложение содержит кванторы для всех своих переменных, поэтому оно имеет логическую глубину n  + 1 . Логическая ширина графа минимальное число переменных в предложении , который определяет его. В предложении, приведенном выше, это количество переменных снова равно n  + 1 . И логическая глубина, и логическая ширина могут быть ограничены в терминах ширины дерева данного графа. Логическая длина, аналогично, определяется как длина самого короткого предложения, описывающего граф. Описанное выше предложение имеет длину, пропорциональную квадрату количества вершин, но можно определить любой граф с помощью предложения, длина которого пропорциональна количеству его ребер.

Все деревья и большинство графов можно описать предложениями первого порядка только с двумя переменными, но расширенными за счет подсчета предикатов. Для графов, которые могут быть описаны предложениями в этой логике с фиксированным постоянным числом переменных, можно найти канонизацию графа за полиномиальное время (с показателем полинома, равным количеству переменных). Сравнивая канонизации, можно решить проблему изоморфизма графов для этих графов за полиномиальное время.

Удовлетворенность

Это неразрешимое ли данный первый порядок предложение может быть реализовано с помощью конечного неориентированного графа.

Существуют предложения первого порядка, моделируемые бесконечными графами, но не конечными. Например, свойство иметь ровно одну вершину степени один, а все остальные вершины имеют степень ровно два, может быть выражено предложением первого порядка. Он моделируется бесконечным лучом , но нарушает лемму Эйлера о подтверждении связи для конечных графов. Однако из отрицательного решения Entscheidungsproblem ( Алонзо Чёрча и Алана Тьюринга в 1930-х годах) следует, что выполнимость предложений первого порядка для графов, которые не ограничены конечностью, остается неразрешимой. Также неразрешимо различать предложения первого порядка, истинные для всех графов, и предложения, истинные для конечных графов, но ложные для некоторых бесконечных графов.

Фиксированная точка

Логика графов, основанная на наименьшей фиксированной точке, расширяет логику графов первого порядка, позволяя предикатам определяться специальными операторами с фиксированной точкой, которые определяют предикат как фиксированную точку формулы, которая связывает значения предиката с другими значениями того же предиката. . Например, если это предикат, который определяет, соединены ли две вершины путем в данном графе, то это наименьшая фиксированная точка формулы ${\ Displaystyle С (и, v)}$${\ displaystyle C}$

${\ Displaystyle C (U, v) \ leftarrow {\ Bigl (} (u = v) \ vee \ exists w {\ bigl (} C (u, w) \ клин w \ sim v {\ bigr)} {\ Bigr)}.}$

Здесь фиксированная точка означает, что истинность правой части формулы подразумевает истинность левой части (как предполагает обратная стрелка импликации). Наименьшая фиксация означает, что пары вершин, для которых истинно, являются подмножеством пар вершин, для которых истинна любая другая фиксированная точка той же формулы. В логике наименьшей фиксированной точки правая часть определяющей формулы должна использовать предикат только положительно (то есть каждое появление должно быть вложено в четное число отрицаний), чтобы сделать наименьшую фиксированную точку хорошо определенной. В эквивалентном варианте, инфляционной логике с фиксированной точкой, формула не обязательно должна быть монотонной, но результирующая фиксированная точка определяется как полученная путем многократного применения импликаций, полученных из определяющей формулы, начиная с предиката «все ложные». Другие варианты, допускающие отрицательные импликации или несколько одновременно определенных предикатов, также возможны, но не обеспечивают дополнительной определяющей силы. Предикат, определенный одним из этих способов, затем может быть применен к кортежу вершин как часть более крупного логического предложения. ${\ displaystyle C}$

Логика с фиксированной точкой и расширения этой логики, которые также позволяют подсчитывать целочисленные переменные, значения которых варьируются от 0 до числа вершин, использовались в описательной сложности в попытке обеспечить логическое описание проблем принятия решений в теории графов, которые могут быть решены. за полиномиальное время . Фиксированная точка логической формулы может быть построена за полиномиальное время с помощью алгоритма, который многократно добавляет кортежи к набору значений, для которых предикат истинен, до достижения фиксированной точки, поэтому решение о том, моделирует ли граф предложение в этой логике, может всегда решаться за полиномиальное время. Не каждое свойство графа с полиномиальным временем можно смоделировать с помощью предложения в логике, использующей только фиксированные точки и подсчет. Однако для некоторых специальных классов графов свойства полиномиального времени такие же, как свойства, выражаемые в логике с фиксированной точкой со счетом. К ним относятся случайные графы, интервальные графы и (посредством логического выражения теоремы о структуре графа ) каждый класс графов, характеризующийся запрещенными минорами .

Второго порядка

В монадической логике графов второго порядка переменные представляют объекты до четырех типов: вершины, ребра, наборы вершин и наборы ребер. Существует два основных варианта логики монадического графа второго порядка: MSO _1, в котором разрешены только вершины и переменные набора вершин, и MSO _2, в котором разрешены все четыре типа переменных. Предикаты для этих переменных включают проверку на равенство, проверку принадлежности и либо инцидентность вершины-ребра (если разрешены как вершинные, так и реберные переменные), либо смежность между парами вершин (если разрешены только вершинные переменные). Дополнительные варианты определения позволяют использовать дополнительные предикаты, такие как предикаты модульного подсчета.

Примеры

В качестве примера, связность неориентированного графа может быть выражена в MSO ₁ как утверждение, что для каждого разделения вершин на два непустых подмножества существует ребро от одного подмножества к другому. Разбиение вершин можно описать подмножеством S вершин на одной стороне раздела, и каждое такое подмножество должно либо описывать тривиальное разделение (в котором одна или другая сторона пуста), либо пересекаться ребром. То есть, граф связное , когда он моделирует MSO ₁ предложение

${\ Displaystyle \ forall S {\ Bigl (} \ forall x (x \ in S) \ vee \ forall y {\ bigl (} \ lnot (y \ in S) {\ bigr)} \ vee \ существует x \ существует y {\ bigl (} x \ in S \ wedge \ lnot (y \ in S) \ wedge x \ sim y {\ bigr)} {\ Bigr)}.}$

Однако связность не может быть выражена ни в логике графа первого порядка, ни в экзистенциальном MSO ₁ ( фрагмент MSO _1, в котором все квантификаторы набора существуют в начале предложения) или даже в экзистенциальном MSO ₂ .

Гамильтоничность может быть выражена в MSO ₂ наличием набора ребер, которые образуют связный 2-регулярный граф на всех вершинах, со связностью, выраженной, как указано выше, и 2-регулярностью, выраженной как наличие двух, но не трех различных ребер на каждой. вершина. Однако гамильтоничность не выражается в MSO ₁ , потому что MSO ₁ не может отличить полные двудольные графы с равным числом вершин на каждой стороне двудольного графа (которые являются гамильтоновыми) от несбалансированных полных двудольных графов (которые не являются).

Хотя это и не является частью определения MSO ₂ , ориентации неориентированных графов могут быть представлены с помощью техники, включающей деревья Тремо . Это позволяет также выразить другие свойства графа, включая ориентации.

Теорема Курселя

Согласно теореме Курселя , каждое фиксированное свойство MSO ₂ можно проверить за линейное время на графах с ограниченной шириной дерева , а каждое фиксированное свойство MSO ₁ можно проверить за линейное время на графах ограниченной ширины клики . Версия этого результата для графов с ограниченной шириной дерева также может быть реализована в логарифмическом пространстве . Приложения этого результата включают управляемый алгоритм с фиксированными параметрами для вычисления числа пересечений графа.

Теорема Сизе

Проблема выполнимости для предложения монадической логики второго порядка - это проблема определения, существует ли хотя бы один граф (возможно, в пределах ограниченного семейства графов), для которого предложение истинно. Для произвольных семейств графов и произвольных предложений эта проблема неразрешима . Однако выполнимость предложений MSO ₂ разрешима для графов ограниченной ширины дерева, а выполнимость предложений MSO ₁ разрешима для графов ограниченной ширины клики. Доказательство включает использование теоремы Курселя для создания автомата, который может проверить свойство, а затем исследование автомата, чтобы определить, есть ли какой-либо граф, который он может принять.

В качестве частичного обращения Seese (1991) доказал, что всякий раз, когда семейство графов имеет разрешимую проблему выполнимости MSO ₂ , семейство должно иметь ограниченную древовидную ширину. Доказательство основано на теореме Робертсона и Сеймура о том, что семейства графов с неограниченной шириной дерева имеют сколь угодно большие сеточные миноры . Зее также предположил, что каждое семейство графов с разрешимой проблемой выполнимости MSO ₁ должно иметь ограниченную ширину клики; это не было доказано, но ослабление гипотезы о расширении MSO ₁ с помощью модульных предикатов подсчета верно.

Примечания

использованная литература