Icketerministisk begränsningslogik

Inom teoretisk datavetenskap är nondeterministisk begränsningslogik ett kombinatoriskt system där en orientering ges till kanterna av en vägd oriktad graf , med förbehåll för vissa begränsningar. Man kan ändra denna orientering genom steg där en enda kant vänds, med samma begränsningar. Begränsningslogikproblemet och dess varianter har visat sig vara PSPACE-komplett för att avgöra om det finns en sekvens av drag som vänder på en specificerad kant och är mycket användbara för att visa olika spel och pussel är PSPACE-hårda eller PSPACE-kompletta .

Detta är en form av reversibel logik genom att varje sekvens av kantorienteringsändringar kan ångras. Hårdheten i detta problem har använts för att bevisa att många spel och pussel har hög spelkomplexitet .

Begränsningsgrafer

En OCH-grind i begränsningslogik. Eftersom nodens minsta in-grad är 2, kan den övre kanten vara ute om och bara om de två nedre kanterna är in.

Exempel på en begränsningsgraf.

I den enklaste versionen av icke-deterministisk begränsningslogik har varje kant av en oriktad graf vikt antingen en eller två. (Vikterna kan också representeras grafiskt genom att rita kanter av vikt ett som röda och kanter av vikt två som blå.) Grafen måste vara en kubisk graf : varje vertex faller in mot tre kanter, och dessutom ska varje vertex vara infallande till ett jämnt antal röda kanter.

Kanterna måste vara orienterade på ett sådant sätt att minst två viktenheter är orienterade mot varje vertex: det måste finnas antingen minst en inkommande blå kant eller minst två inkommande röda kanter. En orientering kan ändras i steg där en enda kant vänds om, med respekt för dessa begränsningar.

Mer allmänna former av icke-deterministisk begränsningslogik tillåter en större variation av kantvikter, fler kanter per vertex och olika trösklar för hur mycket inkommande vikt varje vertex måste ha. En graf med ett system av kantvikter och vertextrösklar kallas en begränsningsgraf . Det begränsade fallet där kantvikterna alla är en eller två, hörnen kräver två enheter av inkommande vikt, och hörnen alla har tre infallande kanter med ett jämnt antal röda kanter, kallas och/eller begränsningsgrafer .

Anledningen till namn- och/eller begränsningsgraferna är att de två möjliga typerna av vertex i en och/eller begränsningsgraf beter sig på vissa sätt som en AND-grind och OR-grind i boolesk logik . En vertex med två röda kanter och en blå kant beter sig som en OCH-grind genom att den kräver att båda röda kanterna pekar inåt innan den blå kanten kan fås att peka utåt. En vertex med tre blå kanter beter sig som en ELLER-grind, med två av dess kanter betecknade som ingångar och den tredje som en utgång, genom att den kräver att minst en ingångskant pekar inåt innan utgångskanten kan fås att peka utåt.

Vanligtvis definieras problem med begränsningslogik kring att hitta giltiga konfigurationer av begränsningsgrafer. Begränsningsgrafer är oriktade grafer med två typer av kanter:

• röda kanter med vikt $1$
• blå kanter med vikt $2$

Vi använder begränsningsgrafer som beräkningsmodeller, där vi tänker på hela grafen som en maskin. En konfiguration av maskinen består av grafen tillsammans med en specifik orientering av dess kanter. Vi kallar en konfiguration giltig, om den uppfyller inflödesbegränsningen: varje vertex måste ha en inkommande vikt på minst $2$ . Med andra ord, summan av vikterna av kanterna som går in i en given vertex måste vara minst $2$ mer än summan av vikterna av kanterna som lämnar vertexen.

Vi definierar också en rörelse i en begränsningsgraf som åtgärden att vända orienteringen av en kant, så att den resulterande konfigurationen fortfarande är giltig.

Formell definition av problemet med Constraint logic

Anta att vi får en begränsningsgraf, en startkonfiguration och en slutkonfiguration. Det här problemet frågar om det finns en sekvens av giltiga drag som flyttar den från startkonfigurationen till slutkonfigurationen. Detta problem är PSPACE-Complete för 3-reguljära eller max-graders 3-grafer. Minskningen följer av QSAT och beskrivs nedan.

Varianter

Plan icke-deterministisk begränsningslogik

Ovanstående problem är PSPACE-Complete även om begränsningsgrafen är plan , dvs nej grafen kan ritas på ett sätt så att inga två kanter korsar varandra. Denna minskning följer av Planar QSAT .

Kantvändning

Detta problem är ett specialfall av det föregående. Den frågar, givet en begränsningsgraf, om det är möjligt att vända en specificerad kant med en sekvens av giltiga drag. Observera att detta kan göras genom en sekvens av giltiga drag så länge som det sista giltiga draget vänder på den önskade kanten. Detta problem har också visat sig vara PSPACE-Complete för 3-vanliga eller max-graders 3-grafer.

Tillfredsställelse av begränsningsdiagram

Detta problem frågar om det finns en orientering av kanterna som uppfyller inflödesbegränsningarna givet en oriktad graf $G$ . Detta problem har visat sig vara NP-Complete.

Hårda problem

Följande problem, på och/eller begränsningsgrafer och deras orienteringar, är PSPACE-kompletta:

• Givet en orientering och en specificerad kant e , testa om det finns en sekvens av steg från den givna orienteringen som så småningom vänder kant e .
• Testa om en orientering kan ändras till en annan genom en sekvens av steg.
• Givet två kanter e och f med specificerade riktningar, testa om det finns två orienteringar för hela grafen, en med den specificerade riktningen på e och den andra har den specificerade riktningen på f , som kan omvandlas till varandra genom en sekvens av steg .

Beviset på att dessa problem är svåra innebär en minskning från kvantifierade booleska formler , baserade på den logiska tolkningen av och/eller begränsningsgrafer. Det kräver ytterligare prylar för att simulera kvantifierare och för att omvandla signaler som bärs på röda kanter till signaler som bärs på blå kanter (eller vice versa), vilket alla kan åstadkommas genom kombinationer av och-vertices och eller-vertices.

Dessa problem förblir PSPACE-kompletta även för och/eller begränsningsgrafer som bildar plana grafer . Beviset på detta involverar konstruktionen av crossover-prylar som tillåter två oberoende signaler att korsa varandra. Det är också möjligt att införa en ytterligare begränsning, samtidigt som hårdheten hos dessa problem bevaras: varje vertex med tre blå kanter kan krävas för att vara en del av en triangel med en röd kant. En sådan vertex kallas en skyddad eller , och den har egenskapen att det (i valfri giltig orientering av hela grafen) inte är möjligt för båda de blå kanterna i triangeln att vara riktade inåt. Denna begränsning gör det lättare att simulera dessa hörn i hårdhetsreduktioner för andra problem. Dessutom kan begränsningsgraferna krävas för att ha begränsad bandbredd , och problemen på dem kommer fortfarande att förbli PSPACE-kompletta.

Bevis på PSPACE-hårdhet

Minskningen följer av QSAT. För att bädda in en QSAT-formel måste vi skapa AND, OR, NOT, UNIVERSAL, EXISTENTIAL och Converter (för att ändra färg) gadgets i begränsningsgrafen. Idén lyder som följer:

• En OCH-vertex är en vertex så att den har två infallande röda kanter (ingångar) och en blå infallande kant (utgång).
• En ELLER vertex är en vertex så att den har tre infallande blå kanter (två ingångar, en utgång).

De andra prylarna kan också skapas på detta sätt. Hela konstruktionen finns på Erik Demaines hemsida. Den fullständiga konstruktionen förklaras också på ett interaktivt sätt.

Ansökningar

De ursprungliga tillämpningarna av icke-deterministisk begränsningslogik använde den för att bevisa PSPACE-fullständigheten hos glidblockspussel som Rush Hour och Sokoban . För att göra det behöver man bara visa hur man simulerar kanter och kantorienteringar, och hörn, och skyddade eller hörn i dessa pussel.

Icketerministisk begränsningslogik har också använts för att bevisa hårdheten hos omkonfigureringsversioner av klassiska grafoptimeringsproblem, inklusive den oberoende uppsättningen , vertextäckning och dominerande uppsättning , på plana grafer av begränsad bandbredd. I dessa problem måste man ändra en lösning på det givna problemet till en annan, genom att flytta ett hörn åt gången in i eller ut ur lösningsmängden samtidigt som man bibehåller egenskapen att de återstående hörnen hela tiden bildar en lösning.

Omkonfigurering 3SAT

Givet en 3-CNF- formel och två tillfredsställande tilldelningar, frågar detta problem om det är möjligt att hitta en sekvens av steg som tar oss från en uppgift till de andra, där vi i varje steg tillåts vända värdet på en variabel. Detta problem kan visas som PSPACE-komplett via en reduktion från problemet med icke-deterministiska begränsningslogik.

Pussel med glidblock

Detta problem frågar om vi kan nå en önskad konfiguration i ett glidblockspussel givet en initial konfiguration av blocken. Detta problem är PSPACE-komplett, även om rektanglarna är dominostater.

Rusningstid

Detta problem frågar om vi kan nå segervillkoret för rusningspusslet givet en initial konfiguration. Det här problemet är PSPACE-komplett, även om blocken har storleken $1\times 2$ .

Dynamisk kartmärkning

Givet en statisk karta, frågar detta problem om det finns en smidig dynamisk märkning. Detta problem är också PSPACE-komplett.