Jaka jest korelacja między wysokością a twardością instancji dla losowego 3-SAT?


11

Ten ostatni artykuł z FOCS2013, Strong Backdoors to Bounded Treewidth SAT autorstwa Gaspersa i Szeidera mówi o związku między szerokością wykresu klauzuli SAT a twardością instancji.

W przypadku losowych instancji 3-SAT, tj. Instancji losowo wybranych 3-SAT, jaka jest korelacja między szerokością wykresu klauzulowego a twardością instancji?

„Twardość wystąpienia” może być traktowana jako „trudna dla typowego solwera SAT”, tj. Czas działania.

Szukam odpowiedzi lub odniesień w stylu teoretycznym lub empirycznym. Według mojej wiedzy wydaje się, że nie ma badań empirycznych na ten temat. Wiem, że istnieją nieco inne sposoby budowania grafów klauzul SAT, ale to pytanie nie koncentruje się na rozróżnieniu.

Być może naturalnym, ściśle powiązanym pytaniem jest to, jak szerokość wykresu klauzulowego odnosi się do przejścia fazowego 3-SAT.

Odpowiedzi:


10

Naprawdę nie odpowiedź, ale najbliższe referencje, o których wiem. Dostępne są wyniki dla szerokości gałęzi. Ponadto istnieje co najmniej jedno badanie empiryczne dotyczące szerokości instancji przemysłowych.


7

Zasadniczo nie można oczekiwać, że przypadkowe przypadki SAT ograniczą szerokość, nawet jeśli są łatwe. Oto przykład:

n3)θ(n)3)

rek412)krek1re2)k4k

ttn/2)


dzięki za pomysły. ofc nie spodziewał się, że przypadkowe przypadki ograniczyłyby szerokość; przeciwnie można przypuszczać bez większych trudności. ale jest to parametr liczbowy, który można porównać / skorelować z twardością podobnie jak wiele innych parametrów badanych w badaniach empirycznych punktów przejściowych SAT, i wydaje się, że na podstawie istniejących badań można oczekiwać pewnej zależności lub korelacji.
vzn

@vzn Chodzi mi bardziej o to, że w najpopularniejszych modelach losowych szerokość dachu przechodzi przez dach, zanim instancje staną się trudne obliczeniowo. Z drugiej strony, instancje `` z prawdziwego życia '' prawdopodobnie mają znacznie mniejszą szerokość niż przypadkowe i spodziewam się, że solwery SAT wykorzystają (niektóre) to.
daniello
Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.