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 ∈ F
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ą.
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:
- 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:
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” ).
- 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:
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 .
- 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 .
Motywacje
- 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.
- 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
- Czy ktoś kiedykolwiek zaproponował sposób pomiaru losowości formuły CNF?
- 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?