Messung der Zufälligkeit von CNF-Formeln

Es ist allgemein bekannt, dass CNF-Formeln grob in zwei breite Klassen unterteilt werden können: Zufalls- und Strukturformeln. Strukturierte CNF-Formeln weisen im Gegensatz zu zufälligen CNF-Formeln eine bestimmte Reihenfolge auf und zeigen Muster, die wahrscheinlich nicht zufällig auftreten. Man kann jedoch strukturierte Formeln finden, die einen gewissen Grad an Zufälligkeit aufweisen (dh bestimmte Gruppen von Klauseln scheinen viel weniger strukturiert zu sein als andere), sowie zufällige Formeln mit einer schwachen Form der Struktur (dh bestimmte Gruppen von Klauseln scheinen weniger zufällig zu sein als andere) ). Daher scheint die Zufälligkeit einer Formel nicht nur eine Ja / Nein-Tatsache zu sein.

Sei $r: \mathcal{F} \rightarrow [0,1]$ eine Funktion, die bei einer CNF-Formel $F \in \mathcal{F}$ einen reellen Wert zwischen $0$ und $1$ einschließlich zurückgibt : bedeutet eine rein strukturierte Formel, während eine rein zufällige Formel bedeutet.$0$$1$

Ich frage mich, ob jemand jemals versucht hat, ein solches zu erfinden . Natürlich wäre der von Wert (zumindest ist dies meine Absicht) nur eine praktische Messung nach vernünftigen Kriterien und keine solide theoretische Wahrheit.$r$$r$

Mich interessiert auch, ob jemand jemals einen statistischen Indikator definiert und untersucht hat, der zur Definition von oder zur Bestimmung anderer nützlicher Gesamteigenschaften einer Formel verwendet werden kann. Mit statistischem Indikator meine ich so etwas:$r$

1. HCV (Hit Count Varianz)
   
   Sei eine Funktion, die bei gegebener Variablen die zurückgibt, mit der in . Sei die Menge der in verwendeten Variablen . Sei der AHC (Average Hit Count). Das HCV ist wie folgt definiert: v j ≤ N v j F V F ≤ h F = $h_F: \mathbb{N} \rightarrow \mathbb{N}$$v_j \in \mathbb{N}$$v_j$$F$$V$$F$HVC=$\bar{h}_F = \frac{1}{|V|} \sum_{v_j \in V}{h_F(v_j)}$
   
   $HVC = \frac{1}{|V|} \sum_{v_j \in V}{(h_F(v_j) - \bar{h}_F)^2}$
   
   In zufälligen Fällen ist das HCV sehr niedrig (alle Variablen werden fast gleich oft erwähnt), während es in strukturierten Fällen nicht der Fall ist (einige Variablen werden sehr häufig verwendet und andere nicht, dh es gibt "Nutzungscluster"). ).
   
   
2. AID (Average Impurity Degree)
   
   Sei die mit der positiv auftritt, und sei die der es negativ auftritt. Sei eine Funktion, die bei einer Variablen ihre ID (Verunreinigungsgrad) zurückgibt. Die Funktion ist wie folgt definiert: . Diejenigen Variablen, die zur Hälfte positiv und zur Hälfte negativ sind, haben einen maximalen Verunreinigungsgrad, während die Variablen, die immer positiv oder immer negativ sind (dh reine Literale), einen minimalen Verunreinigungsgrad haben. Die AID ist einfach wie folgt definiert: v j h - F ( v j ) i : N → [ 0 , 1 ] v j ∈ V i ( v j ) i ( v j ) = 2 ⋅ m i n ( H + F ( v j ) , h - F ( v j$h_F^{+}(v_j)$$v_j$$h_F^{-}(v_j)$$i: \mathbb{N} \rightarrow [0,1]$$v_j \in V$$i(v_j)$$i(v_j) = 2 \cdot \frac{min(h_F^{+}(v_j), h_F^{-}(v_j))}{h_F(v_j)}$
   
   $AID = \frac{1}{|V|} \sum_{v_j \in V}{i(v_j)}$
   
   In zufälligen Fällen (zumindest in Fällen, in denen Variablen mit einer Wahrscheinlichkeit von negiert werden ) ist die AID fast gleich in strukturierten Fällen ist es normalerweise weit von .$0.5$$1$$1$
   
   
3. IDV (Impurity Degree Variance)
   
   Das IDV ist ein robusterer Indikator als das AID allein, da es zufällige Instanzen berücksichtigt, die durch Negieren von Variablen mit einer Wahrscheinlichkeit von weniger als generiert werden . Es ist definiert als: In zufälligen Fällen ist die IDV (weil jede Variable negiert ist mit der gleichen Wahrscheinlichkeit), während es in strukturierten Fällen weit von . $0.5$
   
   $IDV = \frac{1}{|V|} \sum_{v_j \in V}{(i(v_j) - AID)^2}$
   
   $0$$0$

Motivationen

1. Um besser zu verstehen, wie CNF-Formeln funktionieren, wie ihre Zufälligkeit / Struktur gemessen werden könnte, ob andere nützliche Gesamteigenschaften durch Betrachtung ihrer statistischen Indikatoren abgeleitet werden könnten und wie solche Indikatoren verwendet werden könnten, um die Suche zu beschleunigen.
2. Ich frage mich, ob die Erfüllbarkeit (oder sogar die Anzahl der Lösungen) einer CNF-Formel durch eine clevere Manipulation ihrer statistischen Indikatoren abgeleitet werden kann.

Fragen

1. Hat jemand jemals einen Weg vorgeschlagen, um die Zufälligkeit einer CNF-Formel zu messen?
2. Hat jemand jemals einen statistischen Indikator vorgeschlagen, mit dem nützliche Gesamteigenschaften einer CNF-Formel untersucht oder sogar mechanisch abgeleitet werden können?

Ich schlage vor, die Intuition der Physik zu übernehmen, dass "weniger zufällige" Strukturen symmetrischer sind. Die Symmetrie für CNF ist eine Transformation der Variablen, die die Funktion unveränderlich hält. Nach diesen Kriterien können Funktionen von 3 Variablen wie

$\displaystyle x_{1} \vee x_{2} \vee x_{3} .$

oder sagen wir

$\displaystyle(x_{1} \vee x_{2} \vee \neg x_{3}) \wedge (x_{1} \vee \neg x_{2} \vee x_{3}) \wedge (\neg x_{1} \vee x_{2} \vee x_{3}) \wedge (\neg x_{1} \vee \neg x_{2} \vee \neg x_{3}).$

sind weniger zufällig als, sagen wir

$\displaystyle(x_{1} \vee x_{2} \vee \neg x_{3}) \wedge (x_{1} \vee \neg x_{2} \vee x_{3}) \wedge (\neg x_{1} \vee \neg x_{2} \vee x_{3}) .$

Im Allgemeinen ist es eine Herausforderung, ein Konzept der "Zufälligkeit" für endliche Strukturen zu definieren. Historisch wurde es an binären Sequenzen versucht, die wohl die einfachsten endlichen Strukturen sind. Beispielsweise ist eine Sequenz 01010101 intuitiv "weniger zufällig" als beispielsweise 01001110. Es wurde jedoch schnell erkannt, dass es keine konsistente formale Definition einer endlichen Zufallssequenz gibt! Daher muss man naiven Versuchen, ein Zufallsmaß für eine endliche Struktur zu definieren, skeptisch gegenüberstehen.