2 -tilfredshed - 2-satisfiability

Inden for datalogi er 2-tilfredshed , 2-SAT eller bare 2SAT et beregningsproblem med at tildele værdier til variabler, der hver har to mulige værdier, for at tilfredsstille et system med begrænsninger for variabelpar. Det er et specielt tilfælde af det generelle boolske tilfredshedsproblem , som kan indebære begrænsninger på mere end to variabler og problemer med tilfredshed med tilfredshed , som kan tillade mere end to valgmuligheder for værdien af ​​hver variabel. Men i modsætning til de mere generelle problemer, som er NP-komplette , kan 2-tilfredshed løses på polynomtid .

Forekomster af 2-tilfredshedsproblemet udtrykkes typisk som boolske formler af en særlig type, kaldet konjunktiv normalform (2-CNF) eller Krom-formler . Alternativt kan de udtrykkes som en særlig type rettet graf , implikationsgrafen , der udtrykker variablerne i en forekomst og deres negationer som hjørner i en graf og begrænsninger for par af variabler som rettede kanter. Begge disse slags input kan løses i lineær tid , enten ved en metode baseret på backtracking eller ved at bruge de stærkt forbundne komponenter i implikationsgrafen. Opløsning , en metode til at kombinere par af begrænsninger til at lave yderligere gyldige begrænsninger, fører også til en polynomisk tidsløsning. 2-tilfredshedsproblemerne giver en af ​​to store underklasser af de konjunktive normalformler, der kan løses på polynomisk tid; den anden af ​​de to underklasser er Horn-tilfredshed .

2-tilfredshed kan anvendes til geometri og visualiseringsproblemer, hvor en samling af objekter hver har to potentielle placeringer, og målet er at finde en placering for hvert objekt, der undgår overlapninger med andre objekter. Andre applikationer inkluderer klyngedata for at minimere summen af ​​klyngernes diametre, klasselokaler og sportsplanlægning og gendanne figurer fra oplysninger om deres tværsnit.

I beregningskompleksitetsteori giver 2-tilfredshed et eksempel på et NL-komplet problem, et der kan løses ikke-deterministisk ved hjælp af en logaritmisk lagringsmængde, og som er blandt de sværeste af de problemer, der kan løses i denne ressourcebundne. Sættet af alle løsninger til en 2-tilfredshed-instans kan gives strukturen af ​​en mediangraf , men at tælle disse løsninger er #P-komplet og forventes derfor ikke at have en polynom-tid-løsning. Tilfældige tilfælde gennemgår en skarp faseovergang fra opløselige til uløselige tilfælde, da forholdet mellem begrænsninger og variabler stiger forbi 1, et fænomen formodet, men ikke bevist for mere komplicerede former for tilfredshedsproblemet. En beregningsmæssigt vanskelig variation af 2-tilfredshed, at finde en sandhedstildeling, der maksimerer antallet af tilfredse begrænsninger, har en tilnærmelsesalgoritme, hvis optimalitet afhænger af den unikke spilformodning , og en anden vanskelig variation, der finder en tilfredsstillende opgave, der minimerer antallet af sande variabler, er en vigtig test case for parameteriseret kompleksitet .

Problemfremstillinger

Implikationsgrafen for eksempel 2-tilfredshed-eksempelet vist i dette afsnit.

Et 2-tilfredshedsproblem kan beskrives ved hjælp af et boolsk udtryk med en særlig begrænset form. Det er en konjunktion (en boolsk og operation) af klausuler , hvor hver klausul er en disjunktion (en boolsk eller operation) af to variabler eller negerede variabler. Variablerne eller deres negativer i denne formel er kendt som bogstavelige . For eksempel er følgende formel i konjunktiv normal form med syv variabler, elleve klausuler og 22 bogstaver:

2-tilfredshedsproblemet er at finde en sandhedstildeling til disse variabler, der gør hele formlen sand. En sådan opgave vælger, om hver af variablerne skal være sande eller falske, så mindst én bogstavelig i hver klausul bliver sand. For udtrykket vist ovenfor er en mulig tilfredsstillende opgave den, der sætter alle syv variabler til sand. Hver klausul har mindst en ikke-negeret variabel, så denne opgave opfylder alle klausuler. Der er også 15 andre måder at indstille alle variablerne på, så formlen bliver sand. Derfor er 2-tilfredshed-instansen, der repræsenteres af dette udtryk, tilfredsstillende.

Formler i denne form er kendt som 2-CNF-formler. "2" i dette navn står for antallet af bogstaver pr. Klausul, og "CNF" står for konjunktiv normal form , en type boolsk udtryk i form af en kombination af disjunktioner. De kaldes også Krom-formler efter arbejde fra UC Davis- matematikeren Melven R. Krom, hvis papir fra 1967 var et af de tidligste værker om 2-tilfredshedsproblemet.

Hver klausul i en 2-CNF-formel svarer logisk til en implikation fra den ene variabel eller den negerede variabel til den anden. For eksempel kan den anden klausul i eksemplet skrives på en af ​​tre ækvivalente måder:

På grund af denne ækvivalens mellem disse forskellige former for operation kan en 2-tilfredshed-instans også skrives i implikativ normal form , hvor vi erstatter hver eller klausul i den konjunktive normale form med de to implikationer, som den er ækvivalent med.

En tredje, mere grafisk måde at beskrive en 2-tilfredshed-instans på er som en implikationsgraf . En implikationsgraf er en rettet graf , hvor der er et toppunkt pr. Variabel eller negeret variabel, og en kant, der forbinder et toppunkt med et andet, når de tilsvarende variabler hænger sammen med en implikation i den implikative normale form af forekomsten. En implikationsgraf skal være en skæv-symmetrisk graf , hvilket betyder, at den har en symmetri, der tager hver variabel til sin negation og vender orienteringen af ​​alle kanterne.

Algoritmer

Flere algoritmer er kendt for at løse 2-tilfredshedsproblemet. Den mest effektive af dem tager lineær tid .

Opløsning og transitiv lukning

Krom (1967) beskrev den følgende polynomiske tidsbeslutningsprocedure til løsning af 2-tilfredshed-forekomster.

Antag, at en 2-tilfredshed-forekomst indeholder to klausuler, der begge bruger den samme variabel x , men at x negeres i den ene klausul og ikke i den anden. Derefter kan de to klausuler kombineres til frembringelse af en tredje klausul, der har de to andre bogstaver i de to klausuler; denne tredje klausul skal også være opfyldt, når de to første klausuler begge er opfyldt. For eksempel kan vi kombinere klausulerne og på denne måde producere klausulen . Hvad angår den implikative form for en 2-CNF-formel, svarer denne regel til at finde to implikationer og , og udlede ved transitivitet en tredje implikation .

Krom skriver, at en formel er konsistent, hvis gentagen anvendelse af denne slutningsregel ikke kan generere både klausulerne og for en variabel . Som han beviser, er en 2-CNF-formel tilfredsstillende, hvis og kun hvis den er konsistent. For hvis en formel ikke er konsistent, er det ikke muligt at tilfredsstille begge de to klausuler og samtidigt. Og hvis det er konsistent, kan formlen udvides ved gentagne gange at tilføje en klausul i formularen eller ad gangen og bevare konsistensen ved hvert trin, indtil den indeholder en sådan klausul for hver variabel. Ved hvert af disse udvidelsestrin kan en af ​​disse to klausuler altid tilføjes, samtidig med at konsistensen bevares, for hvis ikke så kunne den anden klausul genereres ved hjælp af slutningsreglen. Når alle variabler har en klausul af denne form i formlen, kan en tilfredsstillende tildeling af alle variablerne genereres ved at indstille en variabel til sand, hvis formlen indeholder klausulen og indstille den til falsk, hvis formlen indeholder klausulen .

Krom var primært bekymret over fuldstændigheden af systemerne med slutningsregler, snarere end effektiviteten af ​​algoritmer. Imidlertid fører hans metode til en polynomisk tid, der skal løse 2-tilfredshedsproblemer. Ved at gruppere alle de klausuler, der bruger den samme variabel, og anvende slutningsreglen på hvert par af klausuler, er det muligt at finde alle slutninger, der er mulige fra en given 2-CNF-forekomst, og for at teste, om den er konsekvent, i total tid O ( n 3 ) , hvor n er antallet af variabler i forekomsten. Denne formel kommer fra at multiplicere antallet af variabler med O ( n 2 ) antal par af klausuler, der involverer en given variabel, hvortil slutningsreglen kan anvendes. Det er således muligt at afgøre, om en given 2-CNF-instans er tilfredsstillende i tiden O ( n 3 ) . Fordi det at finde en tilfredsstillende opgave ved hjælp af Kroms metode indebærer en sekvens af O ( n ) konsistenskontrol, ville det tage tid O ( n 4 ) . Selv citerer Itai & Shamir (1976) en hurtigere tidsgrænse for O ( n 2 ) for denne algoritme, baseret på mere omhyggelig ordning af dens operationer. Ikke desto mindre blev selv denne mindre tidsbegrænsning stærkt forbedret af de senere lineære tidsalgoritmer fra Even, Itai & Shamir (1976) og Aspvall, Plass & Tarjan (1979) .

Med hensyn til implikationsgrafen for 2-tilfredshed-instansen kan Kroms slutningsregel tolkes som at konstruere den transitive lukning af grafen. Som Cook (1971) bemærker, kan det også ses som et eksempel på Davis -Putnam -algoritmen til løsning af tilfredshedsproblemer ved hjælp af opløsningsprincippet . Dens rigtighed følger af den mere generelle korrekthed af Davis – Putnam -algoritmen. Dens polynomiske tidsbundne følger af, at hvert opløsningstrin øger antallet af klausuler i forekomsten, som er øvre afgrænset af en kvadratisk funktion af antallet af variabler.

Begrænset backtracking

Selv beskriver Itai & Shamir (1976) en teknik, der involverer begrænset backtracking til løsning af problemer med tilfredshedstilfredshed med binære variabler og parvise begrænsninger. De anvender denne teknik til et problem med klasselokalplanlægning, men de observerer også, at det gælder andre problemer, herunder 2-SAT.

Grundidéen med deres tilgang er at bygge en delvis sandhedsopgave, en variabel ad gangen. Visse trin i algoritmerne er "valgpunkter", punkter, hvor en variabel kan gives en af ​​to forskellige sandhedsværdier, og senere trin i algoritmen kan få den til at gå tilbage til et af disse valgpunkter. Dog er det kun det seneste valg, der kan spores tilbage. Alle valg foretaget tidligere end det seneste er permanente.

I første omgang er der ikke noget valgpunkt, og alle variabler er ikke tildelt. Ved hvert trin vælger algoritmen den variabel, hvis værdi skal indstilles, som følger:

  • Hvis der er en klausul, hvis variabler allerede er indstillet, på en måde, der forfalsker klausulen, går algoritmen tilbage til dens seneste valgpunkt, og fortryder de opgaver, den har foretaget siden dette valg, og vender den beslutning, der blev truffet ved det valg, om. Hvis der ikke er noget valgpunkt, eller hvis algoritmen allerede har sporet tilbage over det seneste valgpunkt, afbryder den søgningen og rapporterer, at input 2-CNF-formlen er utilfredsstillende.
  • Hvis der er en klausul, hvor en af ​​klausulens to variabler allerede er angivet, og klausulen stadig kan blive enten sand eller falsk, så er den anden variabel indstillet på en måde, der tvinger klausulen til at blive sand.
  • I det resterende tilfælde er hver klausul enten garanteret til at blive sand, uanset hvordan de resterende variabler tildeles, eller ingen af ​​dens to variabler er blevet tildelt endnu. I dette tilfælde opretter algoritmen et nyt valgpunkt og sætter en hvilken som helst af de ikke -tildelte variabler til en vilkårligt valgt værdi.

Intuitivt følger algoritmen alle inferenskæder efter at have foretaget hvert af sine valg. Dette fører enten til en modsætning og et backtracking -trin, eller hvis der ikke udledes nogen modsigelse, følger det, at valget var et korrekt valg, der førte til en tilfredsstillende opgave. Derfor finder algoritmen enten korrekt en tilfredsstillende opgave, eller den bestemmer korrekt, at input er utilfredsstillende.

Selv et al. beskrev ikke detaljeret, hvordan denne algoritme skal implementeres effektivt. De udtaler kun, at hvert trin i algoritmen (bortset fra backtracking) kan udføres hurtigt ved at "bruge passende datastrukturer for at finde konsekvenserne af enhver beslutning". Nogle input kan dog få algoritmen til at backtrack mange gange, hver gang der udføres mange trin før backtracking, så dens samlede kompleksitet kan være ikke -lineær. For at undgå dette problem ændrer de algoritmen, så den efter at have nået hvert valgpunkt begynder samtidig at teste begge de to tildelinger for variablen, der er angivet på valgpunktet, og bruge lige mange trin på hver af de to opgaver. Så snart testen for en af ​​disse to opgaver ville skabe et andet valgpunkt, standses den anden test, så der på ethvert trin i algoritmen kun er to grene af backtracking -træet, der stadig testes. På denne måde er den samlede tid brugt på at udføre de to tests for en hvilken som helst variabel proportional med antallet af variabler og klausuler i inputformlen, hvis værdier er permanent tildelt. Som et resultat tager algoritmen i alt lineær tid .

Stærkt forbundne komponenter

Aspvall, Plass & Tarjan (1979) fandt en enklere lineær tidsprocedure til løsning af 2-tilfredshed-forekomster, baseret på forestillingen om stærkt forbundne komponenter fra grafteori .

To hjørner i en rettet graf siges at være stærkt forbundet med hinanden, hvis der er en rettet vej fra den ene til den anden og omvendt. Dette er et ækvivalensforhold , og kurvens hjørner kan opdeles i stærkt forbundne komponenter, undersæt, inden for hvilke hver to hjørner er stærkt forbundet. Der er flere effektive lineære tidsalgoritmer til at finde de stærkt forbundne komponenter i en graf baseret på dybde første søgning : Tarjans stærkt forbundne komponentalgoritme og den sti-baserede stærke komponentalgoritme udfører hver en enkelt dybde første søgning. Kosaraju's algoritme udfører to dybdegående første søgninger, men er meget enkel.

Med hensyn til implikationsgrafen tilhører to bogstaver den samme stærkt forbundne komponent, når der eksisterer kæder af implikationer fra den ene bogstavelige til den anden og omvendt. Derfor skal de to bogstaver have den samme værdi i enhver tilfredsstillende tildeling til den givne 2-tilfredshed-instans. Især hvis en variabel og dens negation begge tilhører den samme stærkt forbundne komponent, kan forekomsten ikke opfyldes, fordi det er umuligt at tildele begge disse bogstaver den samme værdi. Som Aspvall et al. viste, er dette en nødvendig og tilstrækkelig betingelse : en 2-CNF-formel er tilfredsstillende, hvis og kun hvis der ikke er en variabel, der tilhører den samme stærkt forbundne komponent som dens negation.

Dette fører straks til en lineær tidsalgoritme til test af tilfredshed af 2-CNF-formler: udfør ganske enkelt en stærk forbindelsesanalyse på implikationsgrafen og kontroller, at hver variabel og dens negation tilhører forskellige komponenter. Som Aspvall et al. viste også, det fører også til en lineær tidsalgoritme til at finde en tilfredsstillende opgave, når en findes. Deres algoritme udfører følgende trin:

  • Konstruer implikationsgrafen for forekomsten, og find dens stærkt forbundne komponenter ved hjælp af en hvilken som helst af de kendte lineære tidsalgoritmer til stærk tilslutningsanalyse.
  • Kontroller, om en stærkt forbundet komponent både indeholder en variabel og dens negation. Rapporter i så fald, at instansen ikke er tilfredsstillende, og stop.
  • Konstruer kondensationen af implikationsgrafen, en mindre graf, der har et toppunkt for hver stærkt forbundet komponent, og en kant fra komponent i til komponent j, når implikationsgrafen indeholder en kant uv,u hører til komponent i og v tilhører komponent j . Kondensationen er automatisk en rettet acyklisk graf, og ligesom implikationsgrafen, den blev dannet fra, er den skæv-symmetrisk .
  • Topologisk ordne kondensens hjørner. I praksis kan dette effektivt opnås som en bivirkning af det foregående trin, da komponenter genereres af Kosaraju's algoritme i topologisk rækkefølge og af Tarjans algoritme i omvendt topologisk rækkefølge.
  • For hver komponent i den omvendte topologiske rækkefølge, hvis dens variabler ikke allerede har sandhedstildelinger, skal du angive alle bogstaverne i komponenten til at være sande. Dette får også alle bogstaverne i den komplementære komponent til at blive indstillet til falsk.

På grund af den omvendte topologiske rækkefølge og skæv-symmetrien, når en bogstav er sat til sand, vil alle bogstaver, der kan nås fra den via en kæde af implikationer, allerede være sat til sand. Symmetrisk, når et bogstaveligt x er sat til falsk, vil alle bogstaver, der fører til det via en kæde af implikationer, allerede selv være blevet indstillet til falsk. Derfor opfylder sandhedsopgaven konstrueret ved denne procedure den givne formel, som også fuldender beviset for korrekthed af den nødvendige og tilstrækkelige betingelse identificeret af Aspvall et al.

Som Aspvall et al. Vis, en lignende procedure, der involverer topologisk bestilling af de stærkt forbundne komponenter i implikationsgrafen, kan også bruges til at evaluere fuldt kvantificerede boolske formler , hvor formlen, der kvantificeres, er en 2-CNF-formel.

Ansøgninger

Konfliktfri placering af geometriske objekter

En række nøjagtige og omtrentlige algoritmer til problemet med automatisk placering af etiketter er baseret på 2-tilfredshed. Dette problem vedrører placering af tekstmærkater på funktionerne i et diagram eller kort. Sættet med mulige placeringer for hver etiket er typisk meget begrænset, ikke kun af selve kortet (hver etiket skal være i nærheden af ​​den funktion, den mærker og må ikke skjule andre funktioner), men af ​​hinanden: hver anden etiket bør undgå overlapning hinanden, for ellers ville de blive ulæselige. Generelt er det et NP-hårdt problem at finde en etiketplacering, der adlyder disse begrænsninger . Men hvis hver funktion kun har to mulige placeringer for sin etiket (f.eks. Strækker sig til venstre og til højre for funktionen), kan etiketplacering muligvis løses på polynomtid. For i dette tilfælde kan man oprette en 2-tilfredshed-forekomst, der har en variabel for hver etiket, og som har en klausul for hvert par etiketter, der kan overlappe hinanden, hvilket forhindrer dem i at blive tildelt overlappende positioner. Hvis etiketterne alle er kongruente rektangler, kan den tilsvarende 2-tilfredshed-instans kun vise sig at have lineært mange begrænsninger, hvilket fører til nær-lineære tidsalgoritmer til at finde en mærkning. Poon, Zhu & Chin (1998) beskriver et kortmærkningsproblem, hvor hver etiket er et rektangel, der kan placeres i en af ​​tre positioner i forhold til et linjesegment, som det mærker: det kan have segmentet som en af ​​siderne, eller det kan være centreret om segmentet. De repræsenterer disse tre positioner ved hjælp af to binære variabler på en sådan måde, at testning af eksistensen af ​​en gyldig mærkning igen bliver et 2-tilfredshedsproblem.

Formann & Wagner (1991) bruger 2-tilfredshed som en del af en tilnærmelsesalgoritme til problemet med at finde firkantede etiketter af størst mulig størrelse for et givet sæt punkter, med den begrænsning, at hver etiket har et af sine hjørner på det punkt, der det mærker. For at finde en mærkning med en given størrelse eliminerer de firkanter, der, hvis de fordobles, vil overlappe et andet punkt, og de fjerner punkter, der kan mærkes på en måde, der umuligt kan overlappe med et andet punkts etiket. De viser, at disse eliminationsregler bevirker, at de resterende punkter kun har to mulige etiketplaceringer pr. Punkt, hvilket gør det muligt at finde en gyldig etiketplacering (hvis en findes) som løsningen på en 2-tilfredshed-instans. Ved at søge efter den største etiketstørrelse, der fører til en løselig 2-tilfredshed-instans, finder de en gyldig etiketplacering, hvis etiketter er mindst halvt så store som den optimale løsning. Det vil sige, at tilnærmelsesforholdet for deres algoritme højst er to. På samme måde, hvis hver etiket er rektangulær og skal placeres på en sådan måde, at det punkt, den mærker, er et sted langs dens nederste kant, så ved hjælp af 2-tilfredshed at finde den største etiketstørrelse, til hvilken der er en løsning, hvor hver etiket har punkt på et nederste hjørne fører til et tilnærmelsesforhold på højst to.

Lignende anvendelser af 2-tilfredshed er blevet foretaget for andre geometriske placeringsproblemer. På toppunkterne i graftegning , hvis toppunktsplaceringerne er faste, og hver kant skal tegnes som en cirkelbue med en af ​​to mulige placeringer (f.eks. Som et buediagram ), er problemet med at vælge hvilken bue der skal bruges til hver kant for at undgå krydsninger er et 2-tilfredshedsproblem med en variabel for hver kant og en begrænsning for hvert par placeringer, der ville føre til en krydsning. I dette tilfælde er det imidlertid muligt at fremskynde løsningen sammenlignet med en algoritme, der bygger og derefter søger efter en eksplicit fremstilling af implikationsgrafen, ved at søge grafen implicit . I VLSI integreret kredsløbsdesign, hvis en samling moduler skal forbindes med ledninger, der hver især kan bøje højst én gang, er der igen to mulige ruter for ledningerne og problemet med at vælge, hvilken af ​​disse to ruter der skal bruges, i sådanne en måde, hvorpå alle ledninger kan dirigeres i et enkelt lag af kredsløbet, kan løses som en 2-tilfredshed-instans.

Boros et al. (1999) overvejer et andet VLSI-designproblem: spørgsmålet om, hvorvidt hvert modul i et kredsløbsdesign skal spejlvendes. Denne spejlvendning efterlader modulets operationer uændret, men det ændrer rækkefølgen af ​​de punkter, hvor input- og output -signaler fra modulet forbinder til det, og ændrer muligvis, hvor godt modulet passer ind i resten af ​​designet. Boros et al. overvej en forenklet version af problemet, hvor modulerne allerede er placeret langs en enkelt lineær kanal, hvor ledningerne mellem modulerne skal dirigeres, og der er en fast grænse for kanalens densitet (det maksimale antal signaler, der skal passere gennem ethvert tværsnit af kanalen). De observerer, at denne version af problemet kan blive løst som en 2-tilfredshed-instans, hvor begrænsningerne relaterer orienteringen af ​​modulpar, der er direkte på tværs af kanalen fra hinanden. Som en konsekvens kan den optimale densitet også beregnes effektivt ved at udføre en binær søgning, hvor hvert trin involverer løsningen af ​​en 2-tilfredshed-instans.

Dataklynge

En måde at samle et sæt datapunkter i et metrisk rum i to klynger er at vælge klyngerne på en sådan måde, at summen af klyngernes diametre minimeres , hvor diameteren af ​​en enkelt klynge er den største afstand mellem enhver to af dens punkter. Dette foretrækkes frem for at minimere den maksimale klyngestørrelse, hvilket kan føre til, at meget lignende punkter tildeles forskellige klynger. Hvis måldiametrene for de to klynger kendes, kan en klynge, der opnår disse mål, findes ved at løse en 2-tilfredshed-instans. Forekomsten har en variabel pr. Punkt, der angiver, om det punkt tilhører den første eller den anden klynge. Når to punkter er for langt fra hinanden til at begge kan tilhøre den samme klynge, tilføjes en klausul til instansen, der forhindrer denne tildeling.

Den samme metode kan også bruges som en underrutine, når de enkelte klyngediametre er ukendte. For at teste, om en given sum af diametre kan opnås uden at kende de enkelte klyngediametre, kan man prøve alle maksimale par måldiametre, der højst optræder den givne sum, der repræsenterer hvert par diametre som en 2-tilfredshed-instans og bruger en 2-tilfredshed algoritme til at afgøre, om det par kan realiseres ved en klynge. For at finde den optimale sum af diametre kan man udføre en binær søgning, hvor hvert trin er en gennemførlighedstest af denne type. Den samme fremgangsmåde fungerer også for at finde klynger, der optimerer andre kombinationer end summer af klyngediametre, og som bruger vilkårlige forskellighedstal (frem for afstande i et metrisk rum) til at måle størrelsen af ​​en klynge. Tiden for denne algoritme domineres af tiden til at løse en sekvens af 2-tilfredshed-forekomster, der er tæt forbundet med hinanden, og Ramnath (2004) viser, hvordan man kan løse disse relaterede forekomster hurtigere, end hvis de blev løst uafhængigt af hver andre, hvilket fører til en samlet tidsbinding af O ( n 3 ) for sum-of-diameters clustering problem.

Planlægning

Selv, Itai & Shamir (1976) overveje en model af klasseværelset planlægning, hvor et sæt af n lærere skal planlægges til at undervise hver af m kohorter af studerende. Antallet af timer om ugen, som læreren tilbringer med kohorten , beskrives ved indtastning af en matrix, der er givet som input til problemet, og hver lærer har også et sæt timer, hvor han eller hun kan planlægges. Som de viser, er problemet NP-komplet , selv når hver lærer højst har tre ledige timer, men det kan løses som et eksempel på 2-tilfredshed, når hver lærer kun har to ledige timer. (Lærere med kun en enkelt tilgængelig time kan let elimineres fra problemet.) I dette problem svarer hver variabel til en time, som læreren skal bruge med kohorte , opgaven til variablen angiver, om den time er den første eller den anden af lærerens ledige timer, og der er en 2-tilfredshedsklausul, der forhindrer enhver konflikt af en af ​​to typer: to kohorter tildelt en lærer på samme tid som hinanden, eller en kohorte tildelt to lærere på samme tid.

Miyashiro & Matsui (2005) anvender 2-tilfredshed på et problem med sportsplanlægning, hvor parringerne af en round-robin turnering allerede er valgt, og kampene skal tildeles holdenes stadioner. I dette problem er det ønskeligt at skifte hjemme- og udekampe i det omfang det er muligt, så man undgår "pauser", hvor et hold spiller to hjemmekampe i træk eller to udekampe i træk. Højst to hold kan helt undgå pauser, der skifter mellem hjemmekampe og udekampe; intet andet hold kan have den samme hjemme-ude-plan som disse to, for så ville det være ude af stand til at spille det hold, som det havde det samme skema med. Derfor har et optimalt skema to brudløse hold og en enkelt pause for hvert andet hold. Når et af de brudløse hold er valgt, kan man oprette et 2-tilfredshedsproblem, hvor hver variabel repræsenterer hjemme-ude-opgaven for et enkelt hold i et enkelt spil, og begrænsningerne håndhæver de egenskaber, at to hold har en konsekvent tildeling for deres spil, at hvert hold højst har en pause før og højst en pause efter kampen med det brudløse hold, og at intet hold har to pauser. Derfor kan testning af, om en tidsplan indrømmer en løsning med det optimale antal pauser, gøres ved at løse et lineært antal 2-tilfredshedsproblemer, en for hvert valg af det brudløse team. En lignende teknik gør det også muligt at finde skemaer, hvor hvert hold har en enkelt pause, og maksimere snarere end at minimere antallet af pauser (for at reducere den samlede kilometertal, der er rejst af holdene).

Diskret tomografi

Eksempel på at et nonogram -puslespil bliver løst.

Tomografi er processen med at gendanne former fra deres tværsnit. I diskret tomografi , en forenklet version af problemet, der ofte er blevet undersøgt, er formen, der skal genoprettes, en polyomino (en delmængde af firkanterne i det todimensionale firkantede gitter ), og tværsnittene giver samlet information om sætene af firkanter i individuelle rækker og kolonner i gitteret. For eksempel i de populære nonogram -gåder, også kendt som maling med tal eller tallerkener, repræsenterer det sæt firkanter, der skal bestemmes, de mørke pixels i et binært billede , og det input, der er givet til puslespilleren, fortæller ham eller hende, hvor mange på hinanden følgende blokke af mørke pixels, der skal medtages i hver række eller kolonne i billedet, og hvor lang hver af disse blokke skal være. I andre former for digital tomografi gives endnu mindre information om hver række eller kolonne: kun det samlede antal firkanter, frem for antallet og længden af ​​firkantblokkene. En ækvivalent version af problemet er, at vi skal gendanne en given 0-1-matrix givet kun summen af ​​værdierne i hver række og i hver kolonne i matrixen.

Selvom der findes polynomiske tidsalgoritmer til at finde en matrix, der har givet række- og kolonnesummer, kan løsningen være langt fra unik: enhver submatrix i form af en 2 × 2 identitetsmatrix kan suppleres uden at påvirke løsningens rigtighed. Derfor har forskere søgt efter begrænsninger for den form, der skal rekonstrueres, og som kan bruges til at begrænse løsningsrummet. For eksempel kan man antage, at formen er forbundet; Test af om der findes en tilsluttet løsning er imidlertid NP-komplet. En endnu mere begrænset version, der er lettere at løse, er, at formen er ortogonalt konveks : med en enkelt sammenhængende blok af firkanter i hver række og kolonne. Forbedring af flere tidligere løsninger viste Chrobak & Dürr (1999) , hvordan man effektivt rekonstruerer forbundne ortogonalt konvekse former ved hjælp af 2-SAT. Ideen med deres løsning er at gætte indekserne på rækker, der indeholder cellerne længst til højre og højre i den form, der skal rekonstrueres, og derefter oprette et 2-tilfredshedsproblem, der tester, om der findes en form i overensstemmelse med disse gæt og med den givne række- og kolonnesummer. De bruger fire variabler med 2 tilfredshed for hver firkant, der kan være en del af den givne form, en til at angive, om den tilhører hver af fire mulige "hjørneområder" i formen, og de bruger begrænsninger, der tvinger disse områder til at være uensartede, at have de ønskede former, at danne en samlet form med sammenhængende rækker og kolonner og at have de ønskede række- og kolonnesummer. Deres algoritme tager tid O ( m 3 n ), hvor m er den mindste af inputformens to dimensioner og n er den største af de to dimensioner. Den samme metode blev senere udvidet til ortogonalt konvekse former, der kun kunne forbindes diagonalt i stedet for at kræve ortogonal forbindelse.

En del af en løsning til fuld nonogram-gåder, Batenburg og Kosters ( 2008 , 2009 ) brugte 2-tilfredshed til at kombinere information indhentet fra flere andre heuristikker . I betragtning af en delvis løsning på puslespillet bruger de dynamisk programmering inden for hver række eller kolonne til at afgøre, om begrænsningerne i den pågældende række eller kolonne tvinger nogen af ​​dens firkanter til at være hvide eller sorte, og om to firkanter i den samme række eller kolonne kan være forbundet med en implikationsrelation. De forvandler også nonogrammet til et problem med digital tomografi ved at erstatte sekvensen af ​​bloklængder i hver række og kolonne med dets sum og bruge en maksimal flowformulering til at afgøre, om dette digitale tomografiproblem, der kombinerer alle rækker og kolonner, har nogen firkanter, hvis tilstand kan bestemmes eller firkantpar, der kan forbindes ved en implikationsrelation. Hvis en af ​​disse to heuristikker bestemmer værdien af ​​en af ​​firkanterne, er den inkluderet i delopløsningen, og de samme beregninger gentages. Men hvis begge heuristik ikke formår at indstille nogen firkanter, kombineres de implikationer, de begge finder, til et 2-tilfredshedsproblem, og en 2-tilfredshed-løsning bruges til at finde firkanter, hvis værdi er fastsat af problemet, hvorefter proceduren er igen gentaget. Denne procedure lykkes måske eller måske ikke med at finde en løsning, men den kører garanteret i polynomisk tid. Batenburg og Kosters rapporterer, at selvom de fleste avispuslespil ikke har brug for sin fulde kraft, er både denne procedure og en mere kraftfuld, men langsommere procedure, der kombinerer denne 2-tilfredshedsmetode med den begrænsede backtracking af Even, Itai & Shamir (1976) betydeligt mere effektiv end den dynamiske programmering og flowheuristik uden 2-tilfredshed, når den anvendes på vanskeligere tilfældigt genererede nonogrammer.

Renamable Horn tilfredshed

Ved siden af ​​2-tilfredshed er den anden store underklasse af tilfredshedsproblemer, der kan løses i polynomtid, Horn-tilfredshed . I denne klasse af tilfredshedsproblemer er input igen en formel i konjunktiv normal form. Det kan have vilkårligt mange bogstaver pr. Klausul, men højst en positiv bogstavelig. Lewis (1978) fandt en generalisering af denne klasse, omdøbt Horn-tilfredshed , der stadig kan løses på polynomisk tid ved hjælp af en hjælpefunktion med 2 tilfredshed. En formel kan omdøbe Horn, når det er muligt at sætte det i Horn -form ved at erstatte nogle variabler med deres negationer. For at gøre dette opretter Lewis en 2-tilfredshed-forekomst med en variabel for hver variabel i den omdøbelige Horn-forekomst, hvor variablerne med 2-tilfredshed angiver, om de tilsvarende omdøbelige Horn-variabler skal negeres eller ej. For at producere en Horn -forekomst bør der ikke være to variabler, der vises i den samme klausul i den omdøbelige Horn -forekomst, positivt i denne klausul; denne begrænsning på et par variabler er en 2-tilfredshedsbegrænsning. Ved at finde en tilfredsstillende opgave til den resulterende 2-tilfredshed-instans viser Lewis, hvordan man omdanner enhver omdøbelig Horn-forekomst til en Horn-forekomst i polynomtid. Ved at opdele lange klausuler i flere mindre klausuler og anvende en lineær 2-tilfredshedsalgoritme, er det muligt at reducere dette til lineær tid.

Andre applikationer

2-tilfredshed er også blevet anvendt på problemer med at genkende ikke-styrede grafer, der kan opdeles i et uafhængigt sæt og et lille antal komplette topartige undergrafer , der udleder forretningsforhold mellem autonome undersystemer på internettet og rekonstruktion af evolutionære træer .

Kompleksitet og udvidelser

NL-fuldstændighed

En ikke-bestemmende algoritme til at afgøre, om en 2-tilfredshed-forekomst ikke er tilfredsstillende, ved kun at bruge en logaritmisk mængde skrivbar hukommelse, er let at beskrive: vælg ganske enkelt (ikke-deterministisk) en variabel v og søg (ikke-bestemmende) efter en kæde af implikationer, der fører fra v til dens negation og derefter tilbage til v . Hvis der findes en sådan kæde, kan forekomsten ikke være tilfredsstillende. Ved Immerman – Szelepcsényi-sætningen er det også i et ikke-bestemmende logrum muligt at verificere, at en tilfredsstillende 2-tilfredshed-instans er tilfredsstillende.

2-tilfredshed er NL-komplet , hvilket betyder, at det er et af de "hårdeste" eller "mest udtryksfulde" problemer i kompleksitetsklassen NL af problemer, der kan løses ubestemmeligt i logaritmisk rum. Fuldstændighed betyder her, at en deterministisk Turing-maskine, der kun bruger logaritmisk rum, kan forvandle ethvert andet problem i NL til et tilsvarende 2-tilfredshedsproblem. Analogt med lignende resultater for den mere velkendte kompleksitetsklasse NP tillader denne transformation sammen med Immerman – Szelepcsényi-sætningen ethvert problem i NL at blive repræsenteret som en andenordens logikformel med et enkelt eksistentielt kvantificeret prædikat med klausuler begrænset til længde 2. Sådanne formler er kendt som SO-Krom. På samme måde kan den implikative normale form udtrykkes i første ordens logik med tilføjelse af en operator til transitiv lukning .

Sættet med alle løsninger

Den mediane graf repræsenterer alle løsninger til eksempel 2-opfyldelighed eksempel hvis konsekvenser kurve er vist ovenfor.

Sættet af alle løsninger til en 2-tilfredshed-instans har strukturen af ​​en mediangraf , hvor en kant svarer til operationen for at vende værdierne for et sæt variabler, der alle er begrænset til at være ens eller ulige med hinanden. Især ved at følge kanter på denne måde kan man komme fra enhver løsning til enhver anden løsning. Omvendt kan enhver mediangraf repræsenteres som et sæt af løsninger på en 2-tilfredshed-instans på denne måde. Medianen for alle tre løsninger dannes ved at indstille hver variabel til den værdi, den har i størstedelen af de tre løsninger. Denne median danner altid en anden løsning på instansen.

Feder (1994) beskriver en algoritme til effektivt at liste alle løsninger til en given 2-tilfredshed-instans og til at løse flere relaterede problemer. Der findes også algoritmer til at finde to tilfredsstillende opgaver, der har den maksimale Hamming -afstand fra hinanden.

Tæller antallet af tilfredsstillende opgaver

#2SAT er problemet med at tælle antallet af tilfredsstillende opgaver til en given 2-CNF-formel. Dette tælleproblem er #P-komplet , hvilket indebærer, at det ikke kan løses i polynomtid, medmindre P = NP . Desuden er der ikke noget fuldt polynomisk randomiseret tilnærmingsskema for #2SAT, medmindre NP = RP, og dette gælder endda, når input er begrænset til monotone 2-CNF-formler, dvs. 2-CNF-formler, hvor hver bogstavelig er en positiv forekomst af en variabel .

Den hurtigste kendte algoritme til beregning af det nøjagtige antal tilfredsstillende tildelinger til en 2SAT -formel kører i tide .

Tilfældige 2-tilfredshed tilfælde

Man kan tilfældigt danne en 2-tilfredshed-instans for et givet antal n af variabler og m af klausuler ved at vælge hver klausul ensartet tilfældigt fra sættet af alle mulige to-variabelklausuler. Når m er lille i forhold til n , vil en sådan forekomst sandsynligvis være tilfredsstillende, men større værdier af m har mindre sandsynlighed for at være tilfredse. Mere præcist, hvis m / n er fastsat som en konstant α ≠ 1, har sandsynligheden for tilfredshed tendens til en grænse, når n går til uendeligt: ​​hvis α <1, er grænsen en, mens hvis α> 1, er grænsen nul . Således udviser problemet en faseovergang ved α = 1.

Maksimal-2-tilfredshed

I problemet med maksimum-2-tilfredshed ( MAX-2-SAT ) er input en formel i konjunktiv normal form med to bogstaver pr. Klausul, og opgaven er at bestemme det maksimale antal klausuler, der samtidigt kan opfyldes af en opgave . Ligesom det mere generelle problem med maksimal tilfredshed , er MAX-2-SAT NP-hård . Beviset er ved reduktion fra 3SAT .

Ved at formulere MAX-2-SAT som et problem med at finde et snit (det vil sige en opdeling af hjørnerne i to undergrupper) maksimere antallet af kanter, der har et slutpunkt i det første delsæt og et slutpunkt i det andet, i en graf relateret til implikationsgrafen og anvendelse af semidefinite programmeringsmetoder til dette snitproblem, er det muligt i polynomisk tid at finde en omtrentlig løsning, der opfylder mindst 0,940 ... gange det optimale antal klausuler. En afbalanceret MAX 2-SAT-forekomst er en forekomst af MAX 2-SAT, hvor hver variabel optræder positivt og negativt med samme vægt. Til dette problem har Austrin forbedret tilnærmelsesforholdet til .

Hvis den unikke formodning om spil er sand, er det umuligt at tilnærme MAX 2-SAT, balanceret eller ej, med en tilnærmelse konstant bedre end 0,943 ... i polynomtid. Under den svagere antagelse, at P ≠ NP , er problemet kun kendt for at være utilnærmeligt inden for en konstant bedre end 21/22 = 0,95454 ...

Forskellige forfattere har også undersøgt eksponentielle værst tænkelige tidsgrænser for nøjagtig løsning af MAX-2-SAT-forekomster.

Vægtet-2-tilfredshed

I det vægtede 2 -tilfredshedsproblem ( W2SAT ) er input en -variable 2SAT -forekomst og et helt tal k , og problemet er at afgøre, om der findes en tilfredsstillende tildeling, hvor nøjagtigt k af variablerne er sande.

W2SAT -problemet omfatter som et specielt tilfælde vertex -dækningsproblemet med at finde et sæt k -hjørner, der sammen rører alle kanterne af en given uorienteret graf. For enhver given forekomst af vertex -dækningsproblemet kan man konstruere et ækvivalent W2SAT -problem med en variabel for hvert toppunkt i en graf. Hver kant uv i grafen kan repræsenteres af en 2SAT -klausul uv, der kun kan opfyldes ved at inkludere enten u eller v blandt løsningens sande variabler. Derefter koder de tilfredsstillende forekomster af den resulterende 2SAT -formel løsninger på toppunktdækningsproblemet, og der er en tilfredsstillende tildeling med k sande variabler, hvis og kun hvis der er et toppunktdækning med k -hjørner. Derfor er W2SAT ligesom toppunktdæksel NP-komplet .

Desuden giver W2SAT i parameteriseret kompleksitet et naturligt W [1]-komplet problem, hvilket indebærer, at W2SAT ikke kan behandles med fast parameter, medmindre dette gælder for alle problemer i W [1] . Det vil sige, at det er usandsynligt, at der findes en algoritme til W2SAT, hvis driftstid har form f ( k ) · n O (1) . Endnu stærkere kan W2SAT ikke løses i tid n o ( k ), medmindre den eksponentielle tidshypotese fejler.

Kvantificerede boolske formler

Udover at finde den første polynom-tidsalgoritme til 2-tilfredshed, formulerede Krom (1967) også problemet med at evaluere fuldt kvantificerede boolske formler , hvor formlen, der kvantificeres, er en 2-CNF-formel. 2-tilfredshedsproblemet er det særlige tilfælde af dette kvantificerede 2-CNF-problem, hvor alle kvantificatorer er eksistentielle . Krom udviklede også en effektiv beslutningsprocedure for disse formler. Aspvall, Plass & Tarjan (1979) viste, at det kan løses i lineær tid ved en udvidelse af deres teknik med stærkt forbundne komponenter og topologisk orden.

Mange værdsatte logikker

2-tilfredshedsproblemet kan også anmodes om forslag til mangeværdige logikker . Algoritmerne er normalt ikke lineære, og for nogle logikker er problemet endda NP-komplet. Se Hähnle ( 2001 , 2003 ) for undersøgelser.

Referencer