Najlepsze górne granice na SAT

43

W innym wątku Joe Fitzsimons zapytał o „najlepsze obecne dolne granice 3SAT”.

Chciałbym pójść w drugą stronę: jakie są najlepsze obecne górne granice 3SAT? Innymi słowy, jaka jest złożoność czasowa najbardziej wydajnego solvera SAT?

W szczególności, czy można sobie wyobrazić algorytm subwykładniczy (a jednak super-wielomianowy) dla SAT?

— MS Dousti
źródło

2

Nie wiem o wynikach analitycznych, ale wyniki eksperymentalne można znaleźć tutaj baldur.iti.uka.de/sat-race-2010/results.html (patrz linki „HTML”)

— Radu GRIGore

1

ten tytuł pytania jest nieco mylący z powodu istnienia tego pytania: cstheory.stackexchange.com/questions/1295/sat-solver-download . Myślę, że możesz sformułować inaczej jako „Best Upper Bounds on SAT”?

— Suresh Venkat,

@Suresh: Pytanie, o którym mówisz, odnosi się do „#SAT”, podczas gdy to pytanie odpowiada SAT. Ponadto pytanie zostało zadane około tydzień później. W każdym razie, czy nadal sugerujesz zmianę tego tytułu?

— MS Dousti,

tak, ponieważ „SAT Solver” to konkretny dobrze znany obiekt - rzeczywista baza kodu do rozwiązywania SAT. Google będzie zdezorientowany i przekieruje osoby szukające kodu tutaj :).

— Suresh Venkat

4

Jeśli chodzi o motywację tego pytania, pomyślałem, że kilka osób wypróbowało solwery SAT w instancjach 17x17. Wydaje się, że jest to granica tego, co można rozwiązać za pomocą solvera SAT. Zamiast tego możesz wypróbować równoległy solver, ale miałem wrażenie, że na podstawie postów Billa Gasarcha będziesz potrzebować dużego wysiłku. Możesz także zastosować solver SMT z odpowiednią teorią lub użyć solvera ograniczającego, który implementuje globalne ograniczenie z wydajnym propagatorem. W każdym z tych przypadków nowym pomysłem byłoby wyrażenie ważnej właściwości, która jest trudna do wykonania przy użyciu klauzul.

— András Salamon,

38

Istnieją dwa rodzaje „najlepszych” solverów SAT, jeden do teorii, drugi do praktyki.

Teoria

Kazuo Iwama, Kazuhisa Seto, Tadashi Takai, Suguru Tamaki, „ Improved Randomized Algorytms for 3-SAT ”, ISAAC 2010.

randomizowany dla 3SAT. $O(1.32113^n)$

Timon Hertli, Robin A. Moser, Dominik Scheder, „ Improving PPSZ for 3-SAT using Critical Variables ”, 2011.

randomizowany dla 3SAT. $O(1.321^n)$

Konstantin Kutzkov, Dominik Scheder, „ Korzystanie z CSP w celu poprawy deterministyczności 3-SAT ”, 2010.

deterministyczne dla 3SAT. $O(1.439^n)$

Ćwiczyć

Sprawdź wyniki konferencji SAT dla każdego roku.

— Tian Liu
źródło

Znalazłem link do Iwama i in. papier . Czy naprawdę najnowszym i najlepszym wynikiem do rozwiązania SAT do tej pory?

O ({1.32113}^{n})

$O(1.32113^n)$

— MS Dousti,

@ Sadeq: Myślę, że tak, ale tylko dla 3-SAT, a nie SAT.

— Tian Liu,

2

Teraz najlepszym algorytmem jest czas autorstwa Timona Hertliego, Robina A. Mosera i Dominika Schedera.

O ({1.321}^{n})

$O(1.321^n)$

— Tian Liu,

10

Kolejna zmiana: w Focs 2011 Timon Hertli ( arxiv.org/abs/1103.2165 ) udowodnił, że PPSZ rozwiązuje algorytm każdy przypadek 3SAT w czasu.

{1.308}^{n}

$1.308^n$

— Ryan Williams

21

Nie znam żadnej zero błędów randomizowanych algorytmów (lub stożek / Eadvice algorytmów,
dla tej sprawy) dla SAT, które mają lepsze niż granice znanych algorytmów deterministycznych,
niezależnie od tego, czy jest tam obiecał być co najwyżej jeden spełniający zadanie.

Derandomizing HSSW Algorytm 3-SAT pokazuje, że

„Problem 3-SAT można rozwiązać deterministycznie w czasie .” $\overset{\sim}{O}(1.3303^n)$

Derandomizacja PPSZ dla Unique-k-SAT pokazuje, że:

„Dla wyjątkowo satysfakcjonującego 3-CNF (odpowiednio 4-CNF) dla zmiennych, zadowalające przypisanie można znaleźć w deterministycznym czasie działania co najwyżej (odpowiednio. ). ” $n$
$O\hspace{.02 in}(1.3071^n)$ $O\hspace{.02 in}(1.4699^n)$

Szybsze i prostsze 3-SAT - Unikalne ograniczenia SAT dla PPSZ Hold w ogóle pokazują, że (pierwotnie wspomniane w komentarzu Ryana )

„Istnieje algorytm losowy dla 3-SAT z
jednostronnym błędem, który działa w czasie .” $O\hspace{.02 in}(1.30704^n)$

„Istnieje algorytm losowy dla 4-SAT z
jednostronnym błędem, który działa w czasie .” $O\hspace{.02 in}(1.46899^n)$

Przełamanie bariery PPSZ dla Unique 3-SAT
twierdzi, że wynik można podsumować następująco:

„Istnieje losowy algorytm dla Unique-3-SAT, taki że dla i rzeczywista liczba, która pozwala, aby środowisko wykonawcze poprzedniego papieru związane z 3-SAT być wyrażone jako , niniejszej pracy jest algorytm działa w czasie . " $\: \epsilon = 1\hspace{-0.03 in}\big/\hspace{-0.06 in}\left(\hspace{-0.03 in}10^{\hspace{.02 in}24}\hspace{-0.04 in}\right) \:$
$S$
$\: O\hspace{-0.04 in}\left(2^{(S+o(1))\cdot n}\right) \:$ $\;$ $\: O\hspace{-0.04 in}\left(2^{(S-\epsilon+o(1))\cdot n}\right)$

— Społeczność
źródło

16

Algorytm Schoeninga jest algorytmem probabilistycznym dla k-SAT z czasem działania , gdzie . Powoduje to algorytmu dla 3SAT, algorytmu dla 4SAT itp. $O(a^n)$ $a = 2(k-1)/k$ $O(1.33334^n)$ $O(1.5^n)$

Algorytm został również (prawie całkowicie) zdegenerowany przez Mosera i Schedera, którzy podają deterministyczny algorytm rozwiązywania czasu działania kSAT gdzie jest taką samą stałą jak poprzednio, a może być dowolnie małym. $O((a+\epsilon)^n)$ $a$ $\epsilon>0$

Uwaga: w tej odpowiedzi duża notacja Oh ukrywa czynniki poli (n). Chciałem użyć notacji , ale nie wyświetla się ona poprawnie. $O^*$

— Robin Kothari
źródło

1

Dlaczego mówisz „prawie całkowicie”? Czy coś przeoczyłem w gazecie?

— András Salamon,

1

Istnieje deterministyczny algorytm dla k-SAT przez osiem osób, więc wybacz mi, że nie wspominałem o nich wszystkich. Oto link: linkinghub.elsevier.com/retrieve/pii/S0304397501001748 . Zatem dla mamy i nie jest tak dobre, jak inne granice dla 3-SAT przedstawione tutaj, ale dla k-SAT jest to najlepsze, o ile wiem.

O ((2 - \frac{2}{k + 1})^{n})

$O((2 - \frac{2}{k + 1})^n)$

k = 3

$k = 3$

O ({1.5}^{n})

$O(1.5^n)$

— Grigory Yaroslavtsev

4

Powiedziałem „prawie całkowicie” tylko po to, aby wskazać, że istnieje czynnik epsilon. Wydaje mi się, że można by oczekiwać, że całkowita derandomizacja osiągnie ten sam czas pracy (czynniki do wielomianu). A może nie można oczekiwać.

— Robin Kothari,

1

@Grigory Yaroslavtsev: Czy algorytm deterministyczny Moser-Scheder dla kSAT, o którym wspominałem, nie jest szybszy niż ten, który zacytowałeś? Czy coś brakuje?

— Robin Kothari,

1

Po prostu martwiłem się tym w waszej notacji, więc rzeczywiście jest szybszy. Wygląda na to, że artykuł pojawił się na arXiv zaledwie kilka dni temu: arxiv.org/PS_cache/arxiv/pdf/1008/1008.4067v1.pdf , więc nic dziwnego, że o tym nie wiedziałem.

ϵ

$\epsilon$

— Grigory Yaroslavtsev

12

Jak już wspomniano, jeśli jesteś zainteresowany teoretycznymi gwarancjami czasu pracy, to pytanie jest duplikatem.

Ale chciałbym zauważyć, że jeśli naprawdę chcesz rozwiązać konkretny problem (jak wspomniany problem kolorowania), myślę, że studiowanie teoretycznych górnych granic nie ma żadnego sensu.

Chociaż chciałeś uniknąć aspektów „inżynieryjnych”, sugeruję, abyś wziął kilka popularnych solverów SAT, wypróbował je i zobaczył, co się stanie (większość z nich może odczytać ten sam format pliku DIMACS, więc łatwo jest wypróbować różne solwery). Możesz mieć zarówno pozytywne, jak i negatywne niespodzianki. Ostatnio miałem rodzinę instancji SAT; garść przykładów z dziesiątkami tysięcy zmiennych i ponad milionem klauzul okazała się łatwa do rozwiązania, podczas gdy pozornie znacznie prostsze instancje z zaledwie setkami zmiennych i tysiącami klauzul były zdecydowanie zbyt trudne dla jakiegokolwiek solwera, którego próbowałem.

— Jukka Suomela
źródło

8

Oprócz podsumowania Jukki, warto również zauważyć, że istnieją dwa główne rodzaje solverów SAT: te oparte na propagacji ankiet, które działają dobrze w przypadkowych instancjach SAT oraz te, które wykorzystują uczenie się klauzul w połączeniu z rozdzielczością jednostek, które zwykle działają dobrze, aby odkryć kombinatoryczną strukturę. Mają one zupełnie inne zachowanie. Najgorsze przypadki dla solverów SAT to zwykle przypadki, które nie są zadowalające, ale gdzie przestrzeń nogoods ma złożoną strukturę, która nie pozwala na wiele przycinania. Niestety przypadki kombinatoryki są tego rodzaju.

— András Salamon

11

Timon Hertli, „ 3-SAT Faster and Prostsze - Unique-SAT Bounds for PPSZ Hold in General ”, FOCS 2011.

deterministyczne dla 3SAT. $O(1.308^n)$

— Kaveh
źródło

Zakładam, że gdy ktoś wymyśli lepszą górną granicę, zacytuje ten artykuł. Cytowano tylko raz ten artykuł, który brzmi: „Algorytm satysfakcji i średnia twardość przypadków dla formuł w oparciu o pełną podstawę binarną”. Wydaje się, że mówią tylko o niektórych typach formuł. Dlatego wydaje się, że jest to jak dotąd najlepsza górna granica.

— Tayfun Zapłać

@TayfunPay: Dolna część mojej odpowiedzi przytacza ten papier.

$\:$

$\;\;\;\;$

@RickyDemer Uhuh! czy to jest lepsze niż to? Notacja nie jest dla mnie tak jasna.

— Tayfun Zapłać

@TayfunPay: Tak, możesz przeszukać dwa dokumenty, jak opisano poniżej. Na stronie 5 ogólnego artykułu 3-SAT podają wartość , zgłaszają czas działania algorytmu PPSZ dla unikalnego k-SAT pod względem i mówią, że mają to samo wiązanie dla ogólnego k-SAT. Na górze strony 11, ten artykuł mówi, że ich algorytm ma takie samo powiązanie jak PPSZ, co oznacza, że nie pokazali niczego więcej niż wspomniałem w poprzednim zdaniu. (ciąg dalszy ...)

$\:$

S_{3}

$S_3$

S_{k}

$S_k$

$\:$

$\hspace{.35 in}$

(... ciąg dalszy) Na stronie 2 unikalnego artykułu 3-SAT podają wartość i twierdzą, że ich algorytm daje granicę lepszą niż o wyraźną wartość wykładniczą . Ponieważ z poprzedniego zdania jest równe z poprzedniego zdania , wiązanie unikalnego papieru 3-SAT jest wykładniczo lepsze niż ogólne wiązanie papieru 3-SAT.

$\:$

S

$S$

2^{S \cdot n}

$2^{S\cdot n}$

$\:$

S

$S$

S_{3}

$S_3$

$\;\;\;$

8

3SAT nie ma algorytmów wykładniczych, chyba że hipoteza wykładniczego czasu jest fałszywa.

Kazuo Iwama, Suguru Tamaki, Ulepszone górne granice dla 3-SAT , 2004.

algorytm losowy z oczekiwanym czasem działania dla 3SAT. $O({1.324}^n)$

Daniel Rolf, Improved Bound for the PPSZ / Schoning-Algorithm for 3-SAT , 2005.

algorytm losowy z oczekiwanym czasem działania dla 3SAT. $O({1.32216}^n)$

— Mohammad Al-Turkistany
źródło

15

Czy to nie tautologia?

— Tsuyoshi Ito,

1

2^{o (n)}

$2^{o(n)}$

Praca Kazuo Iwama i in. (2004) jest nowszy niż Schoeninga (1999). Zastanawiam się, czy dostępne są jeszcze nowsze wyniki.

— MS Dousti,

8

Aby uniknąć możliwości pomyłki, mój ostatni komentarz odnosi się do pierwszego zdania odpowiedzi: „Niemożliwe jest, aby 3SAT dysponował algorytmami wykładniczymi, chyba że hipoteza wykładnicza czasu (ETH) jest fałszywa”. Rozumiem, że czas wykładniczy hipoteza jest samą hipotezą stwierdzającą, że nie ma algorytmu dla 3SAT, którego czas działania jest podwykładniczy (tj. 2 ^ {o (n)}) w liczbie zmiennych.

— Tsuyoshi Ito,

10

I aby uniknąć dalszych nieporozumień, dodam, że kiedy Tsuyoshi opublikował swój komentarz, odpowiedź zawierała tylko jedno zdanie, co czyniło jego komentarz bardzo odpowiednim.

— Robin Kothari,

7

Ten post dotyczy górnych granic SAT. Ten jeden zajmuje najlepszych dolnych granic. Ten link zawiera szczegółowe informacje na temat corocznego konkursu porównującego implementacje solvera SAT, które można pobrać. Dla uproszczenia możesz zacząć od SAT4J , biblioteki opartej na Javie do rozwiązywania problemów SAT.

— Dave Clarke
źródło

Okazuje się, że to pytanie zostało już zadane wcześniej; Po prostu nie widziałem tego, kiedy przeszukiwałem witrynę. Odpowiedź Tian Liu na pytanie dotyczące górnych granic jest dokładnie tym, czego szukałam. Dzięki za linki, Dave!

— Daniel Apon

1

To dowód, że spędzam tu zbyt dużo czasu ;-)

— Dave Clarke

cieszymy się, że to robisz :)

— Suresh Venkat

2

Nie jestem pewien, czy poleciłbym sat4J, nie tylko jest znacznie wolniejszy niż najnowocześniejszy, ale również nieco bardziej złożony. Prawdą jest jednak, że można go łatwo dostosować dzięki strukturze obiektowej. MiniSat jest bardzo ładnie napisany, a 2.2 jest najnowocześniejszy.

— Mikolas

3

Najlepszy algorytm deterministyczny dla 3-SAT ma teraz górną granicę 1.32793 ^ n, patrz https://arxiv.org/abs/1804.07901 autorstwa Sixue Liu. Zasadniczo w tym artykule poprawiono górne granice dla wszystkich k-SAT.

— ON KI Wong
źródło