Jaka jest dokładna definicja Random K-SAT?

Istnieją 4 różne ograniczenia, które możemy mieć, definiując Losowy K-SAT.
1) Całkowita liczba literałów w danych klauzulach to dokładnie K lub AT, w większości K
2) Dany literał może być używany z lub bez zamiany w tej samej klauzuli (A lub A lub A)
3) Daną zmienną można użyć z lub bez zamiany w tej samej klauzuli (A lub ~ A lub ~ A)
4) Danych klauzul można używać z lub bez zamiany w danej formule
Jaka byłaby najbardziej „poprawna” definicja? Jakie są wady i zalety używania tych różnych definicji?

— Tayfun Pay
źródło

Nie sądzę, aby istniała jedna powszechnie akceptowana definicja.

— Tsuyoshi Ito,

Jeszcze innym wyborem, jaki możesz zrobić, jest to, czy wybrać stałą liczbę klauzul (z zastąpieniem lub bez), czy wybrać próbkę Poissona (każda klauzula jest dołączana niezależnie z ustalonym prawdopodobieństwem).

— David Eppstein

@Tsuyoshi, Geekster: Zgadzam się z Tsuyoshi, o ile wiem, że Solvery SAT nie potrzebują żadnej definicji Losowego k-SAT, jakiejkolwiek techniki używają (DPLL, wyszukiwanie lokalne, rozpowszechnianie ankiet). Jestem w 100% pewien, że każdy poważny SAT Solver usunie zduplikowane klauzule, klauzule tautologiczne i zduplikowane literały przed rozpoczęciem wyszukiwania. Niektóre solwery usuwają również klauzule częściowe.

— Giorgio Camerani

Nie sądzę, że w obecnej formie istnieje odpowiedź na pytanie, ponieważ żadne definicje nie wydają się „bardziej poprawne” niż inne, a „wady i zalety” prawdopodobnie zależą od tego, do czego chcesz użyć wyników na losowym k-SAT. Głosowałem za jego zamknięciem, ponieważ to nie jest prawdziwe pytanie.

— Tsuyoshi Ito

Wydaje mi się, że pytanie można przekształcić, usunąć „najbardziej poprawną” część i skoncentrować się na wadach i zaletach przy określonych wynikach. (Lub odpowiedź może przejść przez każdy możliwy wynik.) Ponieważ pytanie to jest w pewnym stopniu podobne do pytania o rozcięcie, które wydaje się być w zakresie bez argumentów, osobiście chciałbym, aby pytanie pozostało otwarte.

— Hsien-Chih Chang 張顯之

Odpowiedzi:

$k$

$k$ $k$

Dwa główne modele:

Selman losowa modelka - Powtarzające się klauzula są dozwolone . Kyle podał to miłe odniesienie w komentarzach do swojej odpowiedzi, ale niepoprawnie założył, że model zabronił powtarzania klauzul. Połączona (nieco inna) wersja artykułu zawiera bardziej szczegółowe omówienie modelu losowego w części 3: „Ta metoda generowania pozwala na zduplikowanie klauzul we wzorze ... Jednak w miarę jak N dostaje duże duplikaty, stają się rzadkie, ponieważ generalnie wybierz tylko liniową liczbę klauzul. ”

$m$ $2^k {n \choose k}$

Równoważność miejsc przejścia fazowego :

Jednak przejście fazowe (próg 50% satysfakcji) zachodzi przy tym samym stosunku klauzula-zmienna, niezależnie od tego, który z tych modeli został wybrany z zasadniczo tego powodu, że Selman i in. odnotowano w ich pracy.

$A(n,m,k)$ $(n,m,k)$ $p = 1/(2^k {n \choose k})$ $N = {m \choose 2}$ $A(n,m,k) = p \cdot N = {m \choose 2}/{2^k {n \choose k}}$

$k$ $m = O(2^k n)$ $k \geq 3$ $m = O(2^k n)$

$A(n,m,k) = {m \choose 2}/{2^k {n \choose k}} = O(m^2)/O(n^k) = O(n^2)/O(n^k)$

$k \geq 3$ $\displaystyle \lim_{n \rightarrow \infty} O(n^2)/O(n^k) = 0$ $k$

Bezwstydna autopromocja - omawiam te tematy pokrótce w rozdziale 4.1 mojej pracy magisterskiej .

Losowy QBF

Jak się okazuje, sytuacja jest o wiele bardziej interesująca dla losowych QBF. Jakie są AFAIK, pierwsze trzy artykuły na temat losowego QBF proponowały nowy model losowy, krytykując swojego poprzednika.

Zobacz następujące dokumenty:

Cadoli i in. „Eksperymentalna analiza obliczeniowego kosztu oceny ilościowych formuł boolowskich.” AI * IA 1997
Gent + Walsh „Beyond NP: przejście fazowe QSAT”. AAAI / IAAI 1999
Chen + Interian „Model generowania losowych liczbowych formuł boolowskich”. IJCAI 2005

— Huck Bennett
źródło

[Edytowane dla przejrzystości]

Najczęściej stosowaną definicją w literaturze badawczej jest ta, która wymaga dokładnie k odrębnych zmiennych na klauzulę i bez duplikatów klauzul. Jeśli złagodzisz wyraźne ograniczenie zmiennych, większość istniejących badań nie będzie dla ciebie sensowna, ponieważ twoje wyniki nie będą pasować do ich wyników. Dobrze znane przejście fazowe sat / unsat nastąpi w innym stosunku klauzula-zmienna (jeśli przejście w ogóle istnieje) i nie znajdziesz twardych instancji SAT, których można się spodziewać po literaturze.

— Kyle Jones
źródło

Generowanie problemów z twardą satysfakcją przez Mitchella, Selmana i Levesque. Sekcja 4 opisuje, co nazywają „Random K-SAT”. Artykuł nie mówi o złagodzeniu ograniczeń; który wynika z mojej modyfikacji losowego generatora 3SAT i zasilenia wielu instancji typowym solverem opartym na DPLL.

— Kyle Jones

„Najbardziej poprawną definicją jest ta, która wytwarza przejście fazowe sat / unsat przy około 4,26 klauzul na zmienną dla losowego 3SAT.” Chyba żartujesz.

— Tsuyoshi Ito,

@Tsuyoshi: Chociaż „najbardziej poprawny” to zdecydowanie odcinek, myślę, że argumentem jest to, że ta wersja jest standardowa i jedna z najlepiej zbadanych.

— Huck Bennett,

Dziwnie twierdzisz, że 4,26 to magiczna liczba, która wyróżnia określoną definicję terminu „losowa k-SAT” jako najbardziej poprawną. Jeśli to nie jest żart, nie wiem, co powiedzieć.

— Tsuyoshi Ito,

Nie, twierdzę, że odkrycie przejścia fazowego oraz wszystkie późniejsze badania i prace zgadzają się z domyślną definicją losowej k-SAT, którą podałem. Jeśli użyjesz innej definicji, wiele artykułów nie będzie miało dla ciebie sensu, ponieważ wyniki nie będą pasować do wyników. Jeśli pracujesz na rozwiązaniu SAT, znajdziesz łatwe przypadki, w których każdy powiązany artykuł, który przeczytałem, mówi, że powinieneś znaleźć trudne. Nie ma w tym nic magicznego, tylko ustalona konwencja w tym momencie. Jeśli chcesz zacytować kontrprzykłady, zrób to.

— Kyle Jones,