Mierzenie losowości wzorów CNF

12

Powszechnie wiadomo, że formuły CNF można z grubsza podzielić na 2 szerokie klasy: losowe i strukturalne. Strukturalne formuły CNF, w przeciwieństwie do losowych formuł CNF, wykazują pewien porządek, pokazując wzorce, które prawdopodobnie nie wystąpią przypadkowo. Można jednak znaleźć formuły strukturalne wykazujące pewien stopień losowości (tzn. Niektóre określone grupy klauzul wydają się znacznie mniej ustrukturyzowane niż inne), a także formuły losowe z pewną słabą formą struktury (tj. Niektóre określone grupy klauzul wydają się mniej losowe niż inne ). Stąd wydaje się, że losowość formuły nie jest tylko faktem tak / nie.

Niech będzie funkcją, która biorąc pod uwagę wzór CNF , zwraca rzeczywistą wartość z zakresu od do włącznie: oznacza formułę o czystej strukturze, podczas gdy oznacza czystą przypadkową formułę.F Fr:F[0,1]FF0101

Zastanawiam się, czy ktoś kiedykolwiek próbował wymyślić taki . Oczywiście wartość zwracana przez byłaby (przynajmniej taka jest moja intencja) tylko praktycznym pomiarem według pewnych rozsądnych kryteriów, a nie solidną teoretyczną prawdą.rr

Interesuje mnie również to, czy ktoś kiedykolwiek zdefiniował i przestudiował jakikolwiek wskaźnik statystyczny, który można zastosować w definicji lub w określeniu innych użytecznych ogólnych właściwości formuły. Przez wskaźnik statystyczny rozumiem coś takiego:r

  1. HCV (uderzenie liczba wariancji)

    Niech jest funkcją, ponieważ zmienna , zwraca liczbę razy większej pojawia się w . Niech będzie zbiorem zmiennych wykorzystywanych w . Niech będzie AHC (średnia liczba ). HCV jest zdefiniowany następująco: hF:NNvjNvjFVFh¯F=1|V|vjVhF(vj)

    HVC=1|V|vjV(hF(vj)h¯F)2

    W przypadkowych przypadkach HCV jest bardzo niski (wszystkie zmienne są wymieniane prawie tyle samo razy), podczas gdy w strukturalnych przypadkach tak nie jest (niektóre zmienne są używane bardzo często, a inne nie, tj. Istnieją „klastry użytkowania” ).

  2. AID (średni stopień zanieczyszczenia)

    Niech będzie liczbą przypadków, gdy wystąpi dodatnio, i niech liczbę razy, gdy wystąpi ujemna. Niech będzie funkcją, która przy zmiennej zwraca swój identyfikator (stopień zanieczyszczenia). Funkcja jest zdefiniowana następująco: . Zmienne występujące w połowie razy dodatnie, a w połowie razy ujemne mają maksymalny stopień zanieczyszczenia, podczas gdy zmienne występujące zawsze dodatnie lub zawsze ujemne (tj. Czyste literały) mają minimalny stopień zanieczyszczenia. AID jest po prostu zdefiniowany w następujący sposób: hF+(vj)vjhF(vj)i:N[0,1]vjVi(vj)i(vj)=2min(hF+(vj),hF(vj))hF(vj)

    AID=1|V|vjVi(vj)

    W przypadkowych przypadkach (przynajmniej w tych generowanych przez negowanie zmiennych z prawdopodobieństwem ), AID jest prawie równy , podczas gdy w instancjach strukturalnych jest zwykle daleki od .0.511

  3. IDV (wariancja stopnia zanieczyszczenia)

    IDV jest bardziej niezawodnym wskaźnikiem niż sam AID, ponieważ uwzględnia przypadkowe wystąpienia generowane przez negowanie zmiennych o prawdopodobieństwie innym niż . Jest zdefiniowany jako: W przypadkowych przypadkach IDV wynosi (ponieważ każda zmienna jest zanegowana z tym samym prawdopodobieństwem), podczas gdy w instancjach strukturalnych jest daleki od . 0.5

    IDV=1|V|vjV(i(vj)AID)2

    00

Motywacje

  1. Aby lepiej zrozumieć, jak działają formuły CNF, jak można zmierzyć ich losowość / strukturę, jeśli inne użyteczne ogólne właściwości można by wywnioskować, patrząc na ich wskaźniki statystyczne, czy i jak takie wskaźniki można by wykorzystać do przyspieszenia wyszukiwania.
  2. Zastanawiam się, czy o satysfakcji (a nawet liczbie rozwiązań) wzoru CNF można wnioskować po prostu sprytnie manipulując jego wskaźnikami statystycznymi.

pytania

  1. Czy ktoś kiedykolwiek zaproponował sposób pomiaru losowości formuły CNF?
  2. Czy ktoś kiedykolwiek zaproponował jakiś wskaźnik statystyczny, który można by wykorzystać do badania, a nawet do mechanicznego wnioskowania przydatnych ogólnych właściwości formuły CNF?
Giorgio Camerani
źródło
1
zobacz artykuł w tej odpowiedzi ( cstheory.stackexchange.com/questions/4321/… ). Może dać ci wskazówkę, jak zdefiniować taki r
Marcos Villagra
1
prawdopodobnie istotna dyskusja na temat pomiaru losowości ciągów bitów mathoverflow.net/questions/37518/…
Jarosław
Mogę ci tyle powiedzieć, odkąd sam nad tym pracuję. Jeśli weźmiesz pod uwagę SAT, formuły dla 1 i 2 są wykładnicze. Z drugiej strony dla k-SAT wzory na 1 i 2 są wielomianowe. Odnosi się to do mojej PRECYZYJNEJ DEFINICJI LOSOWEGO PYTANIA K-SAT, na którą nikt nie chce odpowiedzieć.
Tayfun Zapłać
@Geekster: Czy chciałbyś tu udzielić odpowiedzi?
Hsien-Chih Chang 張顯 之
@Geekster: Co rozumiesz przez „... formuły 1 i 2 są wykładnicze” ?
Giorgio Camerani,

Odpowiedzi:

3

Proponuję pożyczyć intuicję fizyki, że struktury „mniej losowe” są bardziej symetryczne. Symetria dla CNF to dowolna transformacja zmiennych, która utrzymuje niezmienność funkcji. Według tych kryteriów funkcje 3 zmiennych, takich jak

x1x2x3.

lub powiedzmy

(x1x2¬x3)(x1¬x2x3)(¬x1x2x3)(¬x1¬x2¬x3).

są mniej przypadkowe niż, powiedzmy

(x1x2¬x3)(x1¬x2x3)(¬x1¬x2x3).

Ogólnie rzecz biorąc, zdefiniowanie pojęcia „losowego” na strukturach skończonych jest trudne. Historycznie wypróbowywano go na ciągach binarnych, które są prawdopodobnie najprostszymi strukturami skończonymi. Na przykład intuicyjnie sekwencja 01010101 jest „mniej losowa” niż, powiedzmy, 01001110. Szybko jednak zorientowano się, że nie ma spójnej formalnej definicji skończonej losowej sekwencji! Dlatego należy być sceptycznym wobec wszelkich naiwnych prób określenia miary losowości dla dowolnej skończonej struktury.

Tegiri Nenashi
źródło
Całkowicie zgadzam się z intuicją: „struktura oznacza obecność symetrii, podczas gdy przypadkowość oznacza brak symetrii” . Odwołujesz się do symetrii składniowych (podczas gdy symetrie semantyczne to te, które zmieniają funkcję, ale pozostawiają niezmienioną przestrzeń rozwiązania). Zawsze byłem przekonany, że kluczem są symetrie.
Giorgio Camerani
1
@Walter: Idea symetrii jest raczej próbą wykorzystania algebry niż algorytmów: złożoność algorytmu jest miarą, która wymyka się spójnej definicji obiektów skończonych. Ale potem musimy przypisać miarę złożoności każdemu elementowi do grupy (na przykład transformacja, która neguje pojedynczą zmienną, jest prostsza niż ta, która neguje dwie zmienne) - wydaje się, że wystarczy
przesunąć