Czy najlepsze solwery SAT mogą uwzględniać liczby łatwe?

Nowoczesne solwery SAT bardzo dobrze rozwiązują wiele rzeczywistych przykładów instancji SAT. Wiemy jednak, jak generować trudne: na przykład użyj redukcji z faktoringu do SAT i podaj liczby RSA jako dane wejściowe.

Rodzi to pytanie: co jeśli wezmę prosty przykład faktoringu. Zamiast brać dwóch dużych liczb pierwszych, na bitów, co jeśli wziąć doskonałą o bitów i głównego Q w bitów, niech i kodowanie jako instancja SAT. $n/2$ $p$ $\log n$ $n/\log n$ $N = pq$ $\mathrm{FACTOR}(N)$ $N$ byłby liczbą łatwą do uwzględnienia za pomocą metod wyszukiwania z użyciem siły lub sita, ponieważ jeden z czynników jest tak mały; czy nowoczesny solver SAT z pewną standardową redukcją z faktoringu do SAT również odbiera tę strukturę?

Czy górny współczynnik solverów gdzie szybko? $N = pq$ $|p| = \log n$

— Artem Kaznatcheev
źródło

Istnieją inne, znacznie prostsze przypadki, o których wiemy, że obecnych algorytmów nie można rozwiązać w czasie podwykładniczym. Algorytmy te nie są w stanie policzyć (prawie wszystkie z nich są ulepszeniami DPLL, które odpowiadają systemowi dowodowego propozycji Resolution).

Niestety takie przykłady są niezadowalającymi przypadkami. Pytanie o znalezienie naturalnie zadowalających twardych instancji dla tych algorytmów jest interesującym problemem badawczym (Russeell Impagliazzo wspomniał o tym podczas warsztatów dotyczących złożoności dowodu w zeszłym roku w Banff). Istnieją zadowalające przypadki, o których wiemy, że algorytmy źle się psują, jeśli takie istnieją, ale nie są one bardzo naturalne (są oparte na formułach wyrażających poprawność algorytmów).

Jeśli chodzi o faktoring, jeśli wielkość liczb jest niewielka (np. Logarytmiczna, jak w twoim przypadku, tzn. Liczby podane są w postaci jednoargumentowej), to teoretycznie nie ma wyniku, który wskazywałby, że nie można rozwiązać za pomocą obecnych algorytmów, i w rzeczywistości możemy napisać prosty algorytmy wielomianowe uwzględniające te liczby. Tak więc, czy dany program do rozwiązywania problemów SAT może je rozwiązać, może zależeć od konkretnego algorytmu.

— Kaveh
źródło

\log N

$\log N$

N / \log N

$N/\log N$

@Artem, każda dolna złożoność dowodu dla Rozdzielczości dałaby przykład, weźmy na przykład zasadę gołębiej dziury. Można łatwo wyodrębnić dowód rozdzielczości (odrzucenia) dla niezadowalającej instancji z obliczeń tych algorytmów w tej instancji. Nathan Segerlind z 2007 roku przeprowadził miłą ankietę, w której IIRC obejmuje to między innymi. Daj mi znać, jeśli go nie ma, a znajdę inne odniesienie.

— Kaveh

@Artem, myślę, że argument działa również w przypadku, gdy tylko jedna z liczb jest logarytmiczna, tzn. Możemy rozwiązać go w czasie wielomianowym, przeglądając wszystkie małe liczby, aby sprawdzić, czy jedna z nich jest czynnikiem iloczynu.

— Kaveh

@Kaven tak, dlatego zrobiłem jedną z wielkości logarytmicznych. Wyjaśniam to w pytaniu. Po prostu nie chcę odpowiedzi, która zakłada jednoznaczną reprezentację, jak sugerował twój trzeci akapit. Później przyjrzę się Segerlind. Jeszcze raz dziękuję za komentarz: D.

— Artem Kaznatcheev

@Artem, nie ma za co. :) (użyłem jednoskładnikowa, bo zakłada, że oba numery są małe i stosowany jest jednoskładnikowa do czynienia z faktem, że wielkość powinna być wykładniczy w nich, alternatywnie można po prostu pad, aby były duże.)

— Kaveh