Prosty przypadek SAT, który nie jest łatwy do rozpoznania drzewa

Czy istnieje naturalna klasa formuł CNF - najlepiej taka, która była wcześniej badana w literaturze - o następujących właściwościach:$C$

• jest łatwym przypadkiem SAT, takim jak np. Horn lub 2-CNF, tj. Członkostwo w C można badać w czasie wielomianowym, a wzory F ∈ C można badać pod kątem satysfakcji w czasie wielomianowym.$C$$C$$F\in C$
• Niezadowalające wzory nie są znane z krótkich (wielkości wielomianowych) odrzuceń przypominających drzewa. Jeszcze lepiej byłoby: istnieją niezadowalające wzory w C, dla których znana jest super-wielomianowa dolna granica rozdzielczości drzewiastej.$F\in C$$C$
• Z drugiej strony wiadomo , że niezadowalające formuły w mają krótkie proofy w jakimś silniejszym systemie proof, np. W rozdzielczości typu dag lub w jeszcze silniejszym systemie.$C$

nie powinien być zbyt rzadki, a więc zawierają wiele formuł z n zmiennych dla każdego (lub co najmniej przez większość wartości) n ∈ N . Powinien być również nietrywialny w tym sensie, że zawiera zarówno satysfakcjonujące, jak i niezadowalające formuły.$C$$n$$n\in \mathbb{N}$

Znaczenie powinno mieć następujące podejście do rozwiązywania arbitralnej formuły CNF : znajdź częściowe przypisanie α, a resztkowa formuła F α znajduje się w C , a następnie zastosuj algorytm wielomianowy dla formuł w C do F α . Dlatego chciałbym uzyskać inne odpowiedzi oprócz całkowicie odmiennych ograniczeń od obecnie akceptowanej odpowiedzi, ponieważ uważam, że rzadko zdarza się, aby dowolna formuła stała się zupełnie innym ograniczeniem po zastosowaniu ograniczenia.$F$$\alpha$$F\alpha$$C$$C$$F\alpha$

Wygląda na to, że interesują Cię różne ograniczenia (a twoje ostatnie zdanie jest na dobrej drodze). Są to nietrywialne przypadki zasady szufladki, w których liczba gołębi niekoniecznie jest większa niż liczba dziur, a ponadto niektóre gołębie mogą zostać wykluczone z niektórych dziur.

Różnorodne ograniczenia można ustalić, dopasowując w czasie wielomianowym niskiego rzędu.

• Jean-Charles Régin, Algorytm filtrujący dla ograniczeń różnic w CSP , AAAI 1994, 362–367.
• DE Knuth i A. Raghunathan, Problem kompatybilnych przedstawicieli , SIAM J. Discrete Math. 5 422–427, 1992. doi: 10.1137 / 0405033

Kiedy wyrażane są różne ograniczenia (przy użyciu jednego z kilku kodowań) jako instancje SAT, wówczas uczenie się klauzul opartych na konflikcie zwykle szybko znajduje rozwiązanie, jeśli takie istnieje. Jednak czysta rozdzielczość dla PHP musi zbudować superpolinomalnie duży zestaw klauzul, aby pokazać, że instancja jest niezadowalająca. Ta granica wyraźnie dotyczy tego bardziej ogólnego problemu. Z drugiej strony, pamiętaj, że kodowanie Cooka w PHP pozwala na odrzucenie wielomianowej rozszerzonej rozdzielczości.

• SA Cook, Krótki dowód na zasadę gołębia przy użyciu rozszerzonej rozdzielczości , SIGACT News 8 28–32, 1976. doi: 10.1145 / 1008335.1008338

Ostatnie prace w tym kierunku to Rozdział 5 pracy Sergi Oliva , który stanowił podstawę artykułu z Alberto Atseriasem na CCC 2013.

Oczekuję, że znasz klasyczny wynik Cooka, więc może chciałeś ograniczyć moc systemu dowodowego w trzecim stanie?

Nie jestem pewien, dlaczego wymagałoby to również formuł sat, ale jest kilka artykułów na temat rozdzielenia rozdzielczości ogólnej od drzewa, np. [1]. Wydaje mi się, że tego właśnie chcesz.

[1] Ben-Sasson, Eli, Russell Impagliazzo i Avi Wigderson. „Niemal optymalne rozdzielenie rozdzielczości drzewiastej i ogólnej.” Combinatorica 24.4 (2004): 585–603.

Możesz być zainteresowany formułami SAT z małą (logarytmiczną) „przepustowością” lub „treewidth”. Te formuły są rekurencyjnie partycjonowane w taki sposób, że granica komunikacji między partycjami jest niewielka, a zatem do ich rozwiązania można zastosować numeryczne podejście do programowania dynamicznego. Temat był popularny w latach dziewięćdziesiątych. Kiedyś policzyłem dokładnie liczbę cykli hamiltonowskich na małym wykresie szerokości 24 000 wierzchołków, więc problemy #P przy małej szerokości są również do rozwiązania. Bodlaender jest ważnym punktem odniesienia.

ten następujący artykuł wydaje się zbliżony do tego, co jest wymagane w pewien sposób (jeśli nie pasuje, być może JJ może wyjaśnić, dlaczego). pytanie chce wykluczyć instancje PHP (szufladki) na podstawie braku obu formuł prawda / fałsz, ale (jak cytowano w innych odpowiedziach) PHP jest jednym z najlepiej zbadanych przypadków / generatorów instancji od strony teorii i ma zawsze był generatorem zarówno satysfakcjonujących / niezadowalających formuł, chociaż satysfakcjonujące formuły są mniej podkreślane / badane.

${^m_n}$$m$$n$$m>n$$m \leq n$

• Rozdzielczość przypominająca drzewo jest wielobiegunowo wolniejsza niż rozdzielczość podobna do DAG dla zasady Pigeonhole (1999) autorstwa Kazuo Iwamy, Shuichi Miyazaki

innym podejściem byłoby pójście pod bardziej empirycznym kątem i po prostu generowanie losowych instancji (prawdopodobnie wokół łatwego, trudnego, łatwego do osiągnięcia w 50% punktu przejścia) i filtrowanie ich w celu spełnienia podanych kryteriów. wymagałoby to implementacji rozdzielczości drzewa / rozdzielczości DAG lub „silniejszych systemów”.