Dobrze znane klasy wzorów boolowskich, które wymagają wykładniczo długich prób rozdzielczości

W solverach SAT często można znaleźć metody płaszczyzny cięcia, zmienną propagację, odgałęzienie i wiązanie, uczenie się klauzul, inteligentne cofanie, a nawet ręcznie tkaną ludzką heurystykę. Jednak przez dziesięciolecia najlepsze solwery SAT polegały w dużej mierze na technikach sprawdzania rozdzielczości i używają kombinacji innych rzeczy po prostu do pomocy i do bezpośredniego wyszukiwania w stylu rozdzielczości. Oczywiście podejrzewa się, że ŻADNY algorytm nie zdoła rozstrzygnąć kwestii satysfakcji w czasie wielomianowym, przynajmniej w niektórych przypadkach.

W 1985 r. Haken udowodnił w swojej pracy „Nietrwałość rozdzielczości”, że zasada gołębia zakodowana w CNF nie dopuszcza dowodów wielomianowej rozdzielczości. Chociaż dowodzi to czegoś o niemożliwości zastosowania algorytmów opartych na rozdzielczości, daje również kryteria, według których można oceniać najnowocześniejsze solwery - i w rzeczywistości jednym z wielu rozważań, które należy wziąć pod uwagę przy projektowaniu dzisiejszego solvera SAT, jest to, jak prawdopodobnie będzie on działał w znanych „trudnych” przypadkach.

Posiadanie listy klas formuł boolowskich, które potwierdzają wykładniczo dowody rozdzielczości, jest użyteczne w tym sensie, że daje „twarde” formuły do ​​testowania nowych solverów SAT. Jakie prace wykonano przy kompilowaniu takich klas razem? Czy ktoś ma odniesienie zawierające taką listę i odpowiednie dowody? Podaj jedną klasę logicznej formuły dla każdej odpowiedzi.

Trudne przypadki rozwiązania :

1. Wzory Tseitin (wykresy ekspanderów).

2. $m$$n$$n$$m>n$

3. $n$$O(n^{1.5-\epsilon})$$0<\epsilon<1/2$

Dobre, względnie aktualne, badanie techniczne dla dolnej granicy złożoności dowodu, patrz:

Nathan Segerlind: Złożoność dowodów dowodowych. Biuletyn Symbolic Logic 13 (4): 417-481 (2007) dostępny na stronie : http://www.math.ucla.edu/~asl/bsl/1304/1304-001.ps

Istnieje wiele dobrych ankiet i książek na temat złożoności dowodowych zdań, które zawierają takie listy. Wiele systemów próbnych symuluje rozdzielczość p, dlatego trudna jest dla nich dowolna formuła.

Książki:
1. Jan Krajicek, „Arytmetyka ograniczona, logika zdaniowa i teoria złożoności”, 1995
2. Stephen A. Cook i Phoung The Neguyen, „Logiczne podstawy dowodu złożoności”, 2010

Ankiety:
1. Paul Beame i Toniann Pitassi, „Złożoność dowodu dowodowego: przeszłość, teraźniejszość i przyszłość”, 2001 r.
2. Samuel R. Buss, „Złożona arytmetyka i dowodzenie dowodu złożoności”, 1997 r.
3. Alasdair Urquhart, „Złożoność dowody propozycji ”, 1995

Zobacz także te wymienione tutaj i tutaj .

$2n \times 2n$$2\times 1$

Michael Alekhnovich. Problem okaleczonej szachownicy jest wykładniczo trudny do rozwiązania. Theoretical Compututer Science 310 (1-3): 513-525 (2004). http://dx.doi.org/10.1016/S0304-3975(03)00395-5

$n\to (k)^2_2$$k=\lfloor \frac12 \log n \rfloor$$\bigvee_{i,j\in K} x_{i,j}$$\bigvee_{i,j\in K} \neg x_{i,j}$$K\subseteq \{ 1 , \ldots , n \}$$|K| = k$

Na stronie 9 tego opracowania znajduje się konstrukcja autorstwa Groote i Zantema .

Czy DIMACS nie utrzymuje przykładowych zestawów twardych instancji SAT? Nie mogłem go tam znaleźć jedynie pobieżnym wyglądem, ale jeśli wpiszesz „SAT” w polu wyszukiwania, pojawi się wiele trafień, w tym kilka artykułów / rozmów na temat trudnych instancji SAT.