W artykule „KOMPLEKSOWOŚĆ PROBLEMÓW Z ZADOWOLENIEM” Tomasza J. Schaefera autor wspomniał, że
This raises the intriguing possibility of computer-assisted NP-completeness proofs. Once the researcher has established the basic framework for simulating conjunctions of clauses, the relational complexity could be explored with the help of a computer. The computer would be instructed to randomly generate various input configurations and test whether the defined relation was non-affine, non-bijunctive, etc.
Oczywiście jest to ograniczenie:
The fruitfulness of such an approach remains to be proved: the enumeration of the elements of a relation on lO or 15 variables is Surely not a light computational task.
Jestem tego ciekawa
- Czy istnieją dalsze badania w celu opracowania koncepcji „komputerowych dowodów kompletności NP”? Co jest najnowocześniejsze (może być specyficzne dla lub )? Skoro Schaefer zaproponował pomysł „komputerowego” dowodu kompletności NP (przynajmniej dla obniżek z ), czy oznacza to, że istnieją pewne ogólne zasady / struktury leżące u podstaw tych obniżek (dla tych z \ textf { 3SAT} lub \ text {3-Partition} )? Jeśli tak, jakie one są? 3-partycja SAT 3SAT 3-partycja
- Czy ktoś ma doświadczenie w sprawdzaniu kompletności NP za pomocą komputerowego asystenta? Czy ktoś może wymyślić sztuczny przykład?
Odpowiedzi:
Jeśli chodzi o pytaniu 2, istnieją co najmniej dwa przykłady dowodów -completeness które obejmują komputerowo asystenta.NP
Erickson i Ruskey przedstawili wspomagany komputerowo dowód, że pokrycie Domino Tatami jest NP-kompletne. Dali wielomianowe skrócenie czasu od płaskiego 3-SAT do pokrycia domina tatami. Solver SAT (Minisat) został użyty do automatyzacji odkrywania gadżetów w redukcji. Żadna inna dowód -completeness jest znany.NP
Ruepp Holzer i okazało się, że ołówek puzzle Kakuro jest -Complete. Niektóre części N P dowodu -completeness były generowane automatycznie za pomocą nasyconego-solver (ponownie Minisat).NP NP
źródło
W tym artykule wykazałem, że jeśli dla niektórych istnieje wykres z maksymalnym stopniem k i wytrzymałością krawędzi chromatycznej ściśle wyższą niż k , to Θ p 2- kompletne decyduje, czy wytrzymałość krawędzi chromatycznej wynosi co najwyżej k . Takie wykresy były znane dla k > 3 i przeprowadziłem wyszukiwanie komputerowe, aby znaleźć odpowiedni wykres 12- odwrotny dla k = 3 .k≥3 k k Θp2 k k>3 12 k=3
Złożoność siły chromatycznej i wytrzymałości krawędzi chromatycznej. Złożoność obliczeniowa, 14 (4): 308–340, 2006
źródło
Z powyższego komentarza:
Użyłem biblioteki Choco Java do programowania ograniczeń, aby sprawdzić poprawność działania gadżetów użytych do udowodnienia kompletności NP następujących łamigłówek: Układanka Binarna, Namioty, Układanka z ruchomą kostką bez wolnych komórek, Sieć. Nie miałem jeszcze czasu na ich opublikowanie, ale projekty artykułów są dostępne na moim blogu.
Zastosowana technika jest podobna: wszystkie te łamigłówki można modelować jako wykres siatki, w którym każdy węzeł może zawierać inny element (np. W łamigłówce binarnej elementy to: pusta komórka, stała 0, stała 1, 0, 1), reguły układanki dopuszcza lub zabrania niektórych (lokalnych) konfiguracji (np. w układankach binarnych dozwolone są nie więcej niż dwa lub 1 s obok siebie lub poniżej siebie). Następnie, aby udowodnić kompletność NP, wystarczy zbudować kwadratowy gadżet n × n, który symuluje:0 1 n×n
(A) brama logiczna (AND + OR) i linki, jeśli chcemy użyć PLANAR SAT jako problemu źródłowego NPC; lub
(B) węzeł stopnia 3, w którym jednocześnie można aktywować dokładnie 1 wejście i 1 wyjście, jeśli chcemy użyć CYKLU HAMILTONII na wykresach siatki jako problemu źródłowego NPC (zauważ, że w tym przypadku musi istnieć inny warunek, który wymusza „połączoną ścieżkę”).
W obu przypadkach korzystamy z początkowej konfiguracji, która ustala granice gadżetów (aby zabronić niepożądanych interakcji) i zezwalamy na interakcję między dwoma sąsiadującymi gadżetami tylko poprzez centralny element (lub grupę elementów). Konfiguracja takiego elementu centralnego powinna reprezentować wartość logiczną w przypadku (A) lub przejście w przypadku (B).
Na przykład, aby modelować AND:
W tym momencie, aby sprawdzić gadżet za pomocą solwera SAT (lepiej użyć CPL) wystarczy wdrożyć reguły układanki, a następnie sprawdzić satysfakcję, gdy A, B, C przyjmą wszystkie możliwe kombinacje wartości; i sprawdź, czy są one zgodne z pożądanym zachowaniem. Na przykład w przypadku AND we wszystkich prawidłowych (zadowalających) konfiguracjach gadżetów, w których C jest prawdziwe (C reprezentuje wartość logiczną true), zarówno A, jak i B muszą być prawdziwe.
Jeśli gadżety są bardzo skomplikowane (np. W układance Rolling Cube), myślę, że jest to jedyny sposób, aby upewnić się, że działają poprawnie (i że dowód NPC jest poprawny).
źródło
Zrobiłem to samo - wspomagany komputerowo dowód kompletności NP - w mojej pracy licencjackiej!
Zła część - jest po rosyjsku i nie została przetłumaczona na angielski. http://is.ifmo.ru/diploma-theses/_dvorkin_bachelor.pdf
Pracowałem z bramkami logicznymi w problemach 2D. Plan jest następujący:
Kod jest dostępny przy okazji: https://code.google.com/p/metadynamic-programming/
W ten sposób, dzięki pracy ręcznej tylko przy projektowaniu drutu i kodowaniu reguł konkretnego problemu 2D, byłem w stanie udowodnić kompletność NP:
źródło
pytający wskazał, że jest w porządku z szerszą interpretacją wypowiedzi Schaefera w odpowiedzi. przypadkowo zbieram linki do bloga na pobliski temat i napiszę tutaj.
oryginalne oświadczenie (sekcja 7 p225) jest jasne w swoich zamiarach, co ilustruje przykład całkowitej redukcji NP z 2 idealnie dopasowanych kolorów do 7.1 z użyciem „dychotomii” 2.1.
biorąc ogólnie rzecz biorąc, można zauważyć, że te ogólne pomysły rozwinęły się i zostały zbadane w wielu obszarach badań od czasu tych rozważań / „pomysłów na nasiona” z 1978 r., prowadzących do całych dużych gałęzi i programów badawczych, wciąż trwających, z których żaden nie istniał w prawie żadnej formie w momencie pisania pracy Schaefersa. 1 st jeden ogólny pomysł jest empiryczna Analiza NP właściwości wykończenia za pomocą generatorów przykład / rozwiązują / analizatorów .
największym obszarem badawczym, który się tu pojawił, są przypadkowe instancje SAT i analiza wydajności solvera SAT na nich, która doprowadziła do odkrycia punktu przejściowego w połowie lat 90., później wykazano, że ma głębokie powiązania z fizyką statystyczną i pozornie wszechobecny / nieodłączny / fundamentalny aspekt / charakterystyka wszystkich problemów NP całkowitych. w tej dziedzinie jest bardzo dużo artykułów, a teraz kilka książek. patrz np. Informacje, fizyka i obliczenia Mezard / Montanari
Rozkładanie problemów związanych z satysfakcją lub Korzystanie z wykresów w celu uzyskania lepszego wglądu w problemy dotyczące satysfakcji , Herwig 2006 (83pp). jest to nieco nowatorskie podejście w innych opublikowanych badaniach, które analizują strukturę grafu klauzul zmiennych w wygenerowanych instancjach SAT i analizują ich strukturę / mierniki w celu znalezienia korelacji z twardością.
można przyjmować trudne do przewidzenia problemy i kodować je jako instancje SAT, a następnie badać ich strukturę lub uruchamiać na nich solwery SAT i obserwować dynamiczne zachowanie solverów SAT. nie jest łatwo dowiedzieć się, kiedy to zrobiono 1., ale wczesny przypadek dotyczy faktoringu, prawdopodobnie w połowie lat 90. XX wieku, a te przypadki pojawiły się w konkursach na solver DIMACS SAT. niestety w tym czasie niekoniecznie było to rozpatrywane oddzielnie oddzielnie publikowane wyniki badań. są aluzje w kilku artykułach SAT.
patrz np. Satisfy This: Próba rozwiązania Prime Factorization za pomocą Solisfiable Solvers autorstwa Stefana Schoenmackersa, Anny Cavender, a także cs.se pytanie redukujące problem faktoryzacji liczb całkowitych do NP problemu pełnego i (są też inne powiązane / rozproszone (T) pytania o stos CS to).
2 nd inny nowoczesny ogólna idea / seed nieodłącznym Schaefers starego rachunku jest atakowanie twardych algorytmiczne lub matematycznych problemów w ogóle poprzez przekształcenie ich do instancji SAT, i za pomocą off-the-shelf (ale state-of-the-art) rozwiązują SAT (tj Rozwiązania SAT można uznać ogólnie za dosłownie jeden z najwcześniejszych przypadków w logice / matematyce zautomatyzowanego komputerowego twierdzenia, w którym rozwiązania formuły SAT są podobne do „twierdzeń”, choć wprawdzie współczesne powody mogły się nieco zmienić). sukcesy na tym froncie.
problemem Erdos rozbieżności związane z granicami na losowych spacerów jest bardzo trudne i postęp był ograniczony z analitycznym podejściem, a powieść / bez precedensu, empiryczne podejście SAT został niedawno podjęte w celu osiągnięcia pewnych kluczowych wyników na pokrewnym problemem otwartym, obchodzone przez wielu jako prawdziwy przełom. atak SAT na hipotezę rozbieżności Erdosa Konev, Lisitsa
badania nad optymalnymi sieciami sortowania sięgają dziesięcioleci i istnieją naturalne problemy z otwarciem na minimalnych rozmiarach sieci w celu posortowania określonej liczby elementów. w ciągu ostatnich kilku lat nastąpił znaczny postęp w konwersji tych instancji na SAT i uruchamianiu na nich standardowych solverów. Nowe ograniczenia w optymalnych sieciach sortujących Ehlers, Müller, cytuje także inne ostatnie prace.
źródło