Графиктердің логикасы - Logic of graphs

Математикалық өрістерінде графтар теориясы және ақырғы модельдер теориясы, графиктердің логикасы формальды сипаттамаларымен айналысады графиктің қасиеттері формулаларын қолдана отырып математикалық логика. Бұл формулаларда қолдануға болатын логикалық операция түрлерінің бірнеше вариациялары бар. Графиктердің бірінші ретті логикасы формулаларға қатысты, оларда айнымалылар мен предикаттар графтың жекелеген шыңдары мен шеттеріне қатысты, ал монадикалық екінші ретті графикалық логика шыңдар мен шеттер жиынтығы бойынша сандық анықтауға мүмкіндік береді. Негізделген логика ең аз нүкте операторлары шыңдар кортеждеріне қарағанда жалпы предикаттарға мүмкіндік береді, бірақ бұл предикаттарды тек тіркелген нүктелік операторлар арқылы құруға болады, олардың қуатын бірінші ретті және монадалық екінші ретті арасындағы орташа деңгейге дейін шектейді.

Сөйлем кейбір графиктер үшін дұрыс, ал басқалары үшін жалған болуы мүмкін; график айтылады модель , жазылған , егер шыңдары мен сабақтастық қатынасына қатысты . Алгоритмдік есебі модельді тексеру берілген графиктің берілген сөйлемді модельдеуін тексеруге қатысты. Алгоритмдік есебі қанағаттанушылық берілген сөйлемді модельдейтін графиктің бар-жоғын тексеруге қатысты.Модельді тексеру де, қанықтылық та қиын болғанымен, бірнеше алгоритмдік мета-теоремалар осылайша көрсетілген қасиеттерді графиктің маңызды кластары үшін тиімді тексеруге болатындығын көрсетеді.

Графикалық логикадағы зерттеудің басқа тақырыптарына а. Ықтималдығын зерттеу кіреді кездейсоқ график логиканың белгілі бір түрінде көрсетілген қасиетке ие және үшін деректерді қысу бірегей графикамен модельденетін логикалық формулаларды табуға негізделген.

Бірінші тапсырыс

Көрсетілген график графиктің субографиясы ретінде пайда болады егер, және тек егер. формуласын қанағаттандырады .

Ішінде бірінші ретті логика графтардың қасиеттері, графикалық қасиеті, айнымалылары графиканы білдіретін сандық логикалық формула түрінде көрсетіледі төбелер, бірге предикаттар теңдік пен көршілестік тестілеу үшін.

Мысалдар

Мысалы, графиктегі шарт жоқ оқшауланған шыңдар сөйлеммен білдірілуі мүмкін

қайда белгісі екі төбенің арасындағы бағытталмаған көршілес қатынасты көрсетеді. Бұл сөйлемді әр шыңға арналған мағына ретінде түсіндіруге болады тағы бір шың бар іргелес .[1]

The субографиялық изоморфизм мәселесі бекітілген субграф үшін H ма деп сұрайды H үлкен графиктің субографиясы ретінде пайда болады G. Ол шыңдардың бар екендігін білдіретін сөйлеммен көрінуі мүмкін (әрбір шыңы үшін бір H) әрбір жиегі үшін H, сәйкес төбелер жұбы іргелес орналасқан; суретті қараңыз. Ерекше жағдай ретінде клика проблемасы (бекітілген клик өлшемі үшін) барлық іргелес жатқан клик өлшеміне тең бірқатар шыңдардың бар екендігі туралы сөйлеммен білдірілуі мүмкін.

Аксиомалар

Қарапайым үшін бағытталмаған графиктер, графиктердің бірінші ретті теориясына аксиомалар

(графикте ешнәрсе болмауы керек ілмектер ), және
(шеттері бағытталмаған).[2]

Сияқты графиканың басқа түрлері бағытталған графиктер, әр түрлі аксиомалар мен логикалық тұжырымдарды қамтуы мүмкін мультиграф қасиеттер үшін шыңдар мен шеттер үшін жеке айнымалылар қажет.

Нөлдік заң

The Радо график, әрдайым ақырлы графиктерге сәйкес келетін бірінші ретті сөйлемдерді модельдейтін шексіз график

Глебски және басқалар. (1969) және тәуелсіз,Фагин (1976) дәлелденген а нөл-бір заң бірінші ретті графикалық логика үшін; Фагиннің дәлелі қолданды ықшамдылық теоремасы. Осы нәтижеге сәйкес әрбір бірінші ретті сөйлем не әрдайым дерлік шын немесе әрқашан жалған кездейсоқ графиктер ішінде Erdős – Renii моделі. Яғни, рұқсат етіңіз S тіркелген бірінші ретті сөйлем болып, кездейсоқтықты таңдаңыз n-текс сызбасы Gn жиынындағы барлық графиктер арасында біркелкі кездейсоқ n белгіленген шыңдар. Содан кейін ретінде n ықтималдығы шексіздікке ұмтылады Gn модельдер S не нөлге, не бірге бейім болады:

Сонымен қатар, нақты шексіз график бар Радо график R, сондықтан Радо графигі бойынша модельденген сөйлемдер кездейсоқ ақырлы графикамен модельдеу ықтималдығы біреуіне бейім болатын сөйлемдер болады:

Әрбір шеті басқаларына тәуелсіз ықтималдығы бар енгізілген кездейсоқ графиктер үшін бірдей нәтиже шығады, ықтималдықтары бірдей сөйлемдер нөлге немесе бірге ұмтылады.

The есептеу күрделілігі берілген сөйлемнің нөлге немесе біреуіне бейім болу ықтималдығын анықтау: мәселе осында PSPACE аяқталды.[3]Егер графиктің бірінші ретті қасиетінің кездейсоқ графиктердің біреуіне ұмтылу ықтималдығы болса, онда барлығын тізуге болады n-қасиетті модельдейтін вертикстік графиктер көпмүшелік кешігу (функциясы ретінде n) бір графикке.[2]

Ұқсас талдауды біркелкі емес кездейсоқ графиктер үшін жүргізуге болады, мұнда жиекті қосу ықтималдығы шыңдар санының функциясы болып табылады және шетін қосу немесе алып тастау туралы шешім барлық шеттерге бірдей ықтималдықпен дербес қабылданады. Алайда, бұл графиктер үшін жағдай күрделене түседі, бұл жағдайда бірінші ретті қасиеттің бір немесе бірнеше шегі болуы мүмкін, мысалы, шеті қосу ықтималдығы табалдырықтан шектелген болса, берілген қасиеттің ықтималдығы нөлге немесе бірге ұмтылады. Бұл табалдырықтар ешқашан қисынсыз күш бола алмайды n, сондықтан жиектің қосылу ықтималдығы иррационал күш болатын кездейсоқ графиктер біркелкі кездейсоқ графиктер үшін заңға ұқсас нөлдік заңға бағынады. Ұқсас нөлдік-бір заң шектерді қосу ықтималдығы бар өте сирек кездейсоқ графиктер үшін қолданылады nc бірге c > 1, әзірше c емес суперпартикулярлық қатынас.[4] Егер c суперпартикуляр болса, берілген қасиеттің болу ықтималдығы нөлге немесе бірге тең емес шекті деңгейге ұмтылуы мүмкін, бірақ бұл шекті тиімді есептеуге болады.[5] Шексіз көп шегі бар бірінші ретті сөйлемдер бар.[6]

Параметрленген күрделілік

Егер бірінші ретті сөйлемге кіретін болса к нақты айнымалылар, содан кейін ол сипаттайтын қасиетті графиктер арқылы тексеруге болады n барлығын тексеру арқылы шыңдар к-шыңдар; Алайда, бұл өрескел күш іздеу алгоритм уақытты алып, әсіресе тиімді емес O(nк).Графтың берілген бірінші ретті сөйлемді модельдейтінін тексеру мәселесі ерекше жағдайлар ретінде субографиялық изоморфизм мәселесі (онда сөйлемде тұрақты подграфы бар графиктер сипатталған) және клика проблемасы (онда сөйлемде белгіленген көлемдегі толық ішкі графикасы бар графиктер сипатталған). Кликалық мәселе қиын Ж (1), тұрғысынан қиын мәселелер иерархиясының бірінші деңгейі параметрленген күрделілік. Демек, жұмыс уақыты форманы алатын алгоритмнің тұрақты параметрлері болуы мүмкін емес O(f(кnc) функция үшін f және тұрақты c тәуелді емес к және n.[7]Неғұрлым күшті болса, егер экспоненциалды уақыт гипотезасы шындық, содан кейін модельді тексеру және бірінші ретті тексеру міндетті түрде қуатына пропорционалды уақытты алады n оның дәрежесі пропорционалды к.[8]

Шектелген графиктер кластарында бірінші ретті сөйлемдерді модельдік тексеру әлдеқайда тиімді болуы мүмкін. Атап айтқанда, бірінші ретті сөйлем ретінде көрінетін әрбір графикалық қасиеттерді тексеруге болады сызықтық уақыт графиктері үшін шектелген кеңею. Бұл барлық графиктер таяз кәмелетке толмағандар болып табылады сирек графиктер, минордың тереңдігі функциясымен шектелген шеттер мен төбелердің арақатынасымен. Тіпті тұтастай алғанда, бірінші ретті модельдерді тексеру сызықтық уақытта тығыз графиктер үшін жүргізілуі мүмкін, графиктердің сыныптары үшін, мүмкін тереңдікте, ең болмағанда бір тыйым салынған таяз минор болады. Керісінше, егер модельді тексеру графиканың кез-келген тұқым қуалайтын отбасы үшін тұрақты параметр болып табылса, бұл отбасы еш жерде тығыз болмауы керек.[9]

Мәліметтерді сығу және графикалық изоморфизм

Бірінші реттік сөйлем S графиктер логикасында графикті анықтайды дейді G егер G модельдейтін жалғыз граф S. Әр график кем дегенде бір сөйлеммен анықталуы мүмкін; мысалы, анықтауға болады n-текс сызбасы G сөйлем арқылы n + 1 айнымалылар, графиктің әр шыңы үшін біреуі және тағы біреуі шыңның болмау шартын белгілеу үшін n графиктің шыңдары. Сөйлемнің қосымша сөйлемдерін екі шыңның екі айнымалысының тең болмауын қамтамасыз ету үшін қолдануға болады G бар, және шекаралас емес шыңдардың жұбы арасында шекара болмайды G. Алайда, кейбір графиктер үшін графиканы анықтайтын едәуір қысқа формулалар бар.[10]

Бірнеше әр түрлі графикалық инварианттар берілген графиканы анықтайтын қарапайым сөйлемдерден (әр түрлі қарапайымдылық өлшемдерімен) анықтауға болады. Атап айтқанда логикалық тереңдік графиктің кванторлардың ұя салудың минималды деңгейі ретінде анықталады ( сандық дәреже ) графикті анықтайтын сөйлемде.[11] Жоғарыда келтірілген сөйлем оның барлық айнымалыларының кванторларын орналастырады, сондықтан оның логикалық тереңдігі бар n + 1. The логикалық ені график - бұл оны анықтайтын сөйлемдегі айнымалылардың минималды саны.[11] Жоғарыда көрсетілген сөйлемде айнымалылардың бұл саны тағы да болады n + 1. Логикалық тереңдігі де, логикалық ені де терминдермен шектелуі мүмкін кеңдік берілген графиктің.[12] Логикалық ұзындық, ұқсас түрде, графикті сипаттайтын ең қысқа формуланың ұзындығы ретінде анықталады.[11] Жоғарыда сипатталған сөйлемде ұзындық төбелер санының квадратына пропорционалды, бірақ кез-келген графикті оның жиектерінің санына пропорционалды формуламен анықтауға болады.

Барлық ағаштарды және көптеген графиктерді тек екі айнымалысы бар бірінші реттік сөйлемдермен сипаттауға болады, бірақ предикаттарды санау арқылы кеңейтеді. Осы логикадағы сөйлемдермен тұрақты айнымалылардың тұрақты санымен сипаттауға болатын графиктер үшін а табуға болады графикалық канонизация көпмүшелік уақытта (көпмүшенің көрсеткіші айнымалылар санына тең). Канонизацияларды салыстыру арқылы шешуге болады графикалық изоморфизм мәселесі көпмүшелік уақыттағы осы графиктер үшін.[13]

Қанағаттанушылық

Бұл шешілмейтін берілген бірінші ретті сөйлемді ақырғы бағытталмаған график арқылы жүзеге асыруға бола ма.[14]

Бірінші ретті сөйлемдер бар, олар шексіз графиктермен модельденеді, бірақ кез-келген ақырлы графикамен емес. Мысалы, дәл бір шыңына ие болу қасиеті дәрежесі біреуі, барлық басқа шыңдар дәл екі дәрежеге ие, бірінші реттік сөйлеммен көрсетілуі мүмкін. Ол шексіз модельденеді сәуле, бірақ Эйлерді бұзады қол алысу леммасы ақырлы графиктер үшін. Алайда, бұл теріс шешімнен Entscheidungsproblem (бойынша Алонзо шіркеуі және Алан Тьюринг 1930 ж.) шектеулі графтар үшін бірінші ретті сөйлемдердің қанағаттанушылығы шешілмейтін болып қалады. Сондай-ақ барлық графиктер үшін бірінші ретті сөйлемдер мен ақырлы графиктерге қатысты, бірақ кейбір шексіз графтар үшін жалған сөйлемдер арасындағы айырмашылықты шешуге болмайды.[15]

Бекітілген нүкте

Ең аз нүкте графиктердің негізделген логикасы графиктің бірінші ретті логикасын арнайы тіркелген нүктелік операторлармен анықталған предикаттарға жол беру арқылы кеңейтеді, олар предикатты предикаттың мәндерін сол предикаттың басқа мәндерімен байланыстыратын формуланың бекітілген нүктесі ретінде анықтайды. Мысалы, егер - бұл екі шыңның берілген графиктегі жолмен байланыстылығын анықтайтын предикат формуланың ең аз бекітілген нүктесі болып табылады

яғни формула (импликацияға айналдыру үшін) бұрмаланған мағынаға айналады және ол үшін ақиқат шыңдардың жұптары сол формуланың кез-келген басқа бекітілген нүктесі ақиқат болатын шыңдар жұбының жиынтығы болып табылады. Кем дегенде бекітілген нүктелік логикада анықталатын формуланың оң жағы ең төменгі қозғалмайтын нүктені жақсы анықталған етіп жасау үшін предикатты тек оң жағынан қолдануы керек (яғни, әрбір көрініс терістіктің жұп санына енуі керек). вариант, инфляциялық тұрақты нүктенің логикасы, формула монотонды болмауы керек, бірақ алынған тұрақты нүкте жалған предикаттан басталатын анықтаушы формуладан алынған салдарды бірнеше рет қолдану нәтижесінде алынған нәтиже ретінде анықталады. - анықталған предикаттар, мүмкін, бірақ қосымша анықтамалық қуат бермейді, осы тәсілдердің бірінде анықталған предикатты кейіннен верти кортежіне қолдануға болады ces үлкен логикалық формуланың бөлігі ретінде.[16]

Белгіленген нүктелік логика және осы логиканың кеңейтімдері, сонымен қатар мәні 0-ден бастап шыңдар санына дейінгі айнымалыларды бүтін санауға мүмкіндік береді. сипаттама күрделілігі логикалық сипаттамасын беруге тырысады шешім қабылдау проблемалары шешуге болатын графикалық теорияда көпмүшелік уақыт. Логикалық формуланың қозғалмайтын нүктесін полиномдық уақытта, алгоритм арқылы предикат ақиқат болатын мәндер жиынтығына тіркелген нүктеге жеткенге дейін бірнеше рет қосатын алгоритм арқылы салуға болады, сондықтан графиктің осы логикадағы формуланы модельдеуі мүмкін бе? әрқашан көпмүшелік уақытта шешіледі. Уақыт графигінің кез-келген полиномдық қасиетін тек тұрақты нүктелер мен санауды қолданатын логикадағы формула бойынша модельдеу мүмкін емес.[17][18] Алайда, графиктердің кейбір арнайы кластары үшін полиномдық уақыт қасиеттері санаумен бекітілген нүктелік логикада көрінетін қасиеттермен бірдей. Оларға кездейсоқ графиктер,[17][19] аралық графиктер,[17][20] және (логикалық өрнегі арқылы граф құрылымының теоремасы ) сипатталатын графиктердің әр класы тыйым салынған кәмелетке толмағандар.[17]

Екінші тәртіп

Ішінде монадалық екінші ретті логика графиктердің айнымалылары төрт түрге дейінгі объектілерді бейнелейді: шыңдар, шеттер, шыңдар жиектері және жиектер жиынтығы. Монадалық екінші ретті графикалық логиканың екі негізгі вариациясы бар: MSO1 онда тек шыңдар мен шыңдар жиынтығына айнымалыларға рұқсат етіледі және MSO2 онда барлық төрт түрдегі айнымалыларға рұқсат етілген. Бұл айнымалылардың предикаттарына теңдікті тексеру, мүшелікке тестілеу және шыңның жиілігі (егер шыңның да, жиектің де айнымалыларына рұқсат берілсе) немесе шыңдар жұбы арасындағы көршілестік жатады (егер шыңның айнымалыларына ғана рұқсат етілсе). Анықтамадағы қосымша ауытқулар модульдік санау предикаттары сияқты қосымша предикаттарға мүмкіндік береді.

Мысалдар

Мысал ретінде қосылым бағытталмаған графикті MSO-да көрсетуге болады1 өйткені, шыңдардың екі бос емес екі жиынға бөлінуі үшін, бір ішкі жиыннан екіншісіне өту мүмкіндігі бар. Шыңдардың бөлімі ішкі жиынтықта сипатталуы мүмкін S Бөлімнің бір жағындағы шыңдар, және әрбір осындай жиын тривиальды бөлімді сипаттауы керек (біреуі сол немесе басқа жағы бос болады) немесе шетінен өту керек. Яғни, график MSO-ны модельдеген кезде қосылады1 формула

Алайда, қосылымды бірінші ретті графикалық логикада да, экзистенциалды MSO-да да білдіруге болмайды1 ( фрагмент КММ1 онда барлық орнатылған кванторлар экзистенциалды және сөйлемнің басында кездеседі) және тіпті экзистенциалды MSO2.[21]

Гамильтондылық МСО-да көрсетілуі мүмкін2 барлық шыңдарда байланыстырылған 2-тұрақты графикті құрайтын жиектер жиынтығының болуы, жоғарыда көрсетілген байланыспен және 2-заңдылықпен әр шыңда екі, бірақ үш емес шеттердің түсуі ретінде көрсетілген. Алайда Гамильтондылық MSO-да көрінбейді1, өйткені MSO1 ажырата алмайды толық екі жақты графиктер теңдестірілмеген толық екі жақты графиктерден (олар жоқ) екі партияның екі жағында бірдей төбелер бар (олар гамильтондық).[22]

MSO анықтамасына кірмегенімен2, бағдарлар бағытталмаған графиктерді бейнелейтін техникамен ұсынуға болады Тремо ағаштары. Бұл бағдарлармен байланысты басқа графикалық қасиеттерді де көрсетуге мүмкіндік береді.[23]

Курсель теоремасы

Сәйкес Курсель теоремасы, әрбір тіркелген КММ2 қасиетін сызықтық уақытта шектелген графиктер бойынша тексеруге болады кеңдік және әрбір тіркелген КММ1 қасиетін сызықтық уақытта шектелген графиктер бойынша тексеруге болады ені.[24] Бұл нәтиженің шектелген кеңдік графиктері үшін нұсқасын да енгізуге болады логарифмдік кеңістік.[25] Бұл нәтиженің қосымшаларына есептеу үшін алгоритм тіркелген параметрлі параметр кіреді қиылысу нөмірі график.[26]

Сис теоремасы

The қанағаттану проблемасы монадалық екінші ретті логиканың формуласы үшін формула дұрыс болатын кем дегенде бір графтың бар-жоғын анықтау мүмкіндігі бар (мүмкін графиктердің шектеулі отбасында). Еркін графикалық отбасылар және ерікті формулалар үшін бұл мәселе туындайды шешілмейтін. Алайда, МСО-ның қанағаттанушылығы2 формулалар шектеулі кеңдік графикасы үшін шешімді, ал МСО-ның қанағаттылығы1 формулалар шектеулі ендік графиктері үшін шешімді. Дәлелдемеге Курсель теоремасын қолданып, қасиетті тексере алатын автоматты құру керек, содан кейін автоматты қабылдауға болатын графиктің бар-жоғын анықтау керек.

Ішінара әңгіме ретінде, Seese (1991) Графиктер отбасы шешілетін MSO болған сайын дәлелдеді2 қанағаттану проблемасы, отбасының ені шектелген болуы керек. Дәлел Робертсон мен Сеймурдың шексіз ені бар графтар отбасыларының ерікті түрде үлкен екендігі туралы теоремасына негізделген. тор кәмелетке толмағандар. Сис сонымен қатар графиканың әр отбасы шешімді MSO бар деп болжады1 қанағаттанушылық проблемасының ені шектеулі болуы керек; бұл дәлелденген жоқ, бірақ MSO-ны кеңейтетін болжамның әлсіреуі1 модульдік санаудың предикаттары бар.[27]

Ескертулер

  1. ^ Спенсер (2001), 1.2 бөлім, «Бірінші ретті теория дегеніміз не?», 15-17 бет.
  2. ^ а б Голдберг (1993).
  3. ^ Гранджен (1983).
  4. ^ Shelah & Spencer (1988); Спенсер (2001).
  5. ^ Линч (1992).
  6. ^ Спенсер (1990).
  7. ^ Дауни және стипендиаттар (1995).
  8. ^ Чен және басқалар. (2006).
  9. ^ Нешетил және Оссона де Мендес (2012), 18.3 Subgraph изоморфизм мәселесі және бульдік сұраулар, 400–401 б .; Dvořák, Kráľ & Thomas (2010); Grohe, Kreutzer & Siebertz (2014).
  10. ^ Пихурко, Спенсер және Вербицкий (2006).
  11. ^ а б c Пихурко және Вербицкий (2011).
  12. ^ Вербицкий (2005).
  13. ^ Иммерман және Ландер (1990).
  14. ^ Парис (2014) бұл шешілмейтін нәтиже белгілі болғанын және оны соған жатқызатынын жазады Трахтенброт (1950) ақырлы құрылымдардың жалпы кластары үшін бірінші ретті қанағаттанушылықтың шешілмейтіндігі туралы.
  15. ^ Лавров (1963).
  16. ^ Grohe (2017), 23-27 б.
  17. ^ а б c г. Grohe (2017), 50-51 б.
  18. ^ Кай, Фюрер және Иммерман (1992).
  19. ^ Гелла, Колайтис және Луосто (1996).
  20. ^ Laubner (2010).
  21. ^ Фагин, Стокмейер және Варди (1995).
  22. ^ Курсель және Энгельфриет (2012); Либкин (2004), Қорытынды 7.24, 126–127 бб.
  23. ^ Курсель (1996).
  24. ^ Курсель және Энгельфриет (2012).
  25. ^ Элберфельд, Якоби және Тантау (2010).
  26. ^ Grohe (2001); Kawarabayashi & Reed (2007).
  27. ^ Курсель және Оум (2007).

Әдебиеттер тізімі