Czy były jakieś badania nad SAT powyżej progu satysfakcji?

25

Dobrze znaną cechą instancji SAT jest stosunek liczby klauzul do liczby zmiennych , tj. Iloraz . Dla każdego istnieje wartość progowa st \ dla , większość instancji jest zadowalająca, a dla większość instancji jest niezadowalająca. Przeprowadzono wiele badań dotyczących problemów, w których , oraz problemów z wystarczająco małym , $k$ $m$ $n$ $\rho = m/n$ $k$ $\alpha$ $\rho \ll \alpha$ $\rho \gg \alpha$ $\rho \ll \alpha$ $\rho$ $k$ -SAT staje się rozwiązywalny w czasie wielomianowym. Zobacz na przykład artykuł ankiety Dimitris Achlioptas z Podręcznika satysfakcji ( PDF ).

Zastanawiam się, czy jakakolwiek praca została wykonana w innym kierunku (gdzie ), np. Czy możemy w jakiś sposób przekształcić problem z CNF na DNF w tym przypadku, aby go szybko rozwiązać. $\rho \gg \alpha$

Zasadniczo, co wiadomo na temat SAT gdzie ? $\rho = m/n \gg \alpha$

cc.complexity-theory sat random-k-sat phase-transition Matt Groff
źródło

10

Warto zauważyć, że jest funkcją .

α

$\alpha$

k

$k$

Huck Bennett,

czy może być jakaś transformacja, która pokazuje jakąś symetrię między dwoma regionami po obu „stronach” punktu przejścia? wydaje się prawdopodobne. w każdym razie pytanie jest dość szerokie w tym sensie, że istnieje wiele empirycznych / teoretycznych badań punktu przejściowego, które nie koncentrują się tak bardzo na jednej „stronie” czy drugiej…

dniu

26

Tak, było. Moshe Vardi niedawno wygłosił ankietę na warsztatach BIRS Theoretical Fundations of Applied SAT Solving :

Moshe Vardi, Przejścia fazowe i złożoność obliczeniowa , 2014.

(Moshe przedstawia wykres swojego eksperymentu nieco po minucie 14:30 w swoim przemówieniu powyżej).

Niech oznacza stosunek klauzuli. Gdy wartość wzrasta powyżej progu, problem staje się łatwiejszy dla istniejących solverów SAT, ale nie tak łatwy, jak przed osiągnięciem progu. Trudność wzrasta, gdy zbliżamy się do progu od dołu. Po progu problem staje się łatwiejszy w porównaniu do progu, ale spadek trudności jest znacznie mniej gwałtowny. $\rho$ $\rho$

Niech oznacza trudność problemu wrt do (w ich eksperymencie jest medianą czasu działania GRASP w losowych instancjach 3SAT ze współczynnikiem klauzuli ). Moshe sugeruje, że zmienia się w następujący sposób: $T_\rho(n)$ $n$ $T_\rho(n)$ $\rho$ $T_\rho(n)$

$\rho \ll$ próg: jest wielomianem w , $T_\rho(n)$ $n$
$\rho$ jest blisko progu: jest wykładnicze w , $T_\rho(n)$ $n$
$\rho \gg$ próg: pozostaje wykładniczo w ale wykładnik maleje wraz ze wzrostem . $T_\rho(n)$ $n$ $\rho$

Kaveh
źródło

1

Należy zauważyć, że powyższe wyniki są wynikami eksperymentalnymi (od około 2000) przy użyciu określonego solvera SAT (GRASP). Ale teoretycznie wiadomo, że dla wystarczająco dużego (powiedzmy ) nawet rozdzielczość ma małe obalenie o niezadowolenie. I, jak pisał wcześniej Jan Johannsem, obalenie 3-SAT jest łatwe (w przeciętnym przypadku) już wtedy, gdy .

ρ

$\rho$

Ω (n)

$\Omega(n)$

ρ = Ω (\sqrt{n})

$\rho=\Omega(\sqrt{n})$

Iddo Tzameret,

19

Istnieją co najmniej dwie linie badań dotyczące losowego dla formuł o stosunku klauzula / zmienna większym niż próg satysfakcji: $k\text-\mathsf{SAT}$

Dla takich wzorów wykazano dolne granice długości obalenia w rozdzielczości i mocniejsze systemy dowodu zdania, poczynając od artykułu „ Wiele trudnych przykładów rozdzielczości ” Chvátala i Szemerédiego. Te dolne granice rozdzielczości oznaczają dolne granice czasu działania solverów SAT opartych na DPLL i CDCL. Najsilniejsze dolne granice są dla rachunku wielomianowego, ze względu na Ben-Sassona i Impagliazzo .
W przypadku takich wzorów istnieją wydajne algorytmy deterministyczne do potwierdzania niezadowolenia, tj. Algorytmy, które albo wypisują „UNSAT”, albo „Nie wiem”, gdzie odpowiedź „UNSAT” musi być poprawna i musi wypisać „UNSAT” na niezadowalające formuły o wysokim prawdopodobieństwie. Najsilniejsze wyniki w tym kierunku zawdzięczają Feige i Ofek .

Jan Johannsen
źródło

Być może warto zauważyć, że Chvátal / Szemerédi pokazują, że losowa formuła SAT z jest niezadowalająca. Feige i Ofek podają algorytm spektralny, gdy . Pozostaje więc przerwa między a której prawie każda formuła jest niezadowalająca, ale nie wiemy, jak zdecydować, że tak jest.

k

$k$

m / n \geq c_{1}

$m/n \ge c_1$

m / n \geq c_{2} n^{1 / 2}

$m/n \ge c_2n^{1/2}$

\sqrt{n}

$\sqrt{n}$

c_{1} n

$c_1n$

c_{2} n^{3 / 2}

$c_2n^{3/2}$

András Salamon

2

tutaj jest starsze, ale istotne badanie / kąt wiodącego eksperta.

Ostrze noża Walsh 1998

$\kappa$

$\kappa$ $\kappa$

$m/n \gg\alpha$

vzn
źródło

z drugiej strony przypuszczalnie możliwe jest generowanie pojedynczych „twardych” wystąpień o dowolnym m / n „wymiarze”, po prostu są one statystycznie mniej prawdopodobne poza przejściem fazowym „P-NP-P”.

dniu

Czy były jakieś badania nad SAT powyżej progu satysfakcji?

Odpowiedzi: