Measuring the randomness of CNF formulas It's widely known that CNF formulas can be roughly partitioned in 2 broad classes: random vs. structured. Structured CNF formulas, in opposition to random CNF formulas, exhibit some sort of order, showing patterns that are unlikely to happen by chance. However, one may find structured formulas showing some degree of randomness (i.e. certain specific groups of clauses seems much less structured than others), as well as random formulas with some weak form of structure (i.e. certain specific groups of clauses seems less randomic than others). Hence it seems that the randomness of a formula is not just a yes/no fact.

Let $r: \mathcal{F} \rightarrow [0,1]$ be a function that, given a CNF formula $F \in \mathcal{F}$, returns a real value between $0$ and $1$ inclusive: $0$ means a pure structured formula, while $1$ means a pure random formula.

I wonder if someone has ever tried to invent such a $r$. Of course the value returned by $r$ would be (at least this is my intent) just a practical measurement according to some reasonable criteria, rather than a solid theoretical truth.

I'm also interested to know if someone has ever defined and studied any statistical indicator that can be used in the definition of $r$, or in determining other useful overall properties of a formula. By statistical indicator I mean something like that:


HCV (Hit Count Variance)Let $h_F: \mathbb{N} \rightarrow \mathbb{N}$ be a function that, given a variable $v_j \in \mathbb{N}$, returns the number of times $v_j$ appears in $F$. Let $V$ be the set of variables used in $F$. Let $\bar{h}_F = \frac{1}{|V|} \sum_{v_j \in V}{h_F(v_j)}$ be the AHC (Average Hit Count). The HCV is defined as follows:

$HVC = \frac{1}{|V|} \sum_{v_j \in V}{(h_F(v_j) - \bar{h}_F)^2}$

In random instances, the HCV is very low (all variables are mentioned almost the same number of times), while in structured instances it is not (some variables are used very frequently and some others are not, i.e. there are "clusters of usage").
AID (Average Impurity Degree)Let $h_F^{+}(v_j)$ be the number of times $v_j$ occurs positive, and let $h_F^{-}(v_j)$ the number of times it occurs negative. Let $i: \mathbb{N} \rightarrow [0,1]$ be a function that, given a variable $v_j \in V$, returns its ID (Impurity Degree). The function $i(v_j)$ is defined as follows: $i(v_j) = 2 \cdot \frac{min(h_F^{+}(v_j), h_F^{-}(v_j))}{h_F(v_j)}$. Those variables occurring half of the times positive and half of the times negative have maximum Impurity Degree, while those variables occurring always positive or always negative (i.e. pure literals) have minimum Impurity Degree. The AID is simply defined as follows:

$AID = \frac{1}{|V|} \sum_{v_j \in V}{i(v_j)}$

In random instances (at least in those generated by negating variables with probability $0.5$), the AID is almost equal to $1$, while in structured instances it is usually far from $1$.
IDV (Impurity Degree Variance)The IDV is a more robust indicator than the AID alone, since it accounts for random instances generated by negating variables with probability different than $0.5$. It is defined as:

$IDV = \frac{1}{|V|} \sum_{v_j \in V}{(i(v_j) - AID)^2}$
In random instances the IDV is $0$ (because every variable is negated with the same probability), while in structured instances it is far from $0$.



  Motivations
  
  
  To better understand how CNF formulas work, how their randomness/structure could be measured, if other useful overall properties could be inferred by looking at their statistical indicators, if and how such indicators could be used to speed up search. 
  Wonder if the satisfiability (or even the number of solutions) of a CNF formula could be inferred by just cleverly manipulating its statistical indicators.
  
  
  Questions
  
  
  Did anyone ever proposed a way to measure the randomness of a CNF formula?
  Did anyone ever proposed any statistical indicator that can be used to study or even to mechanically infer useful overall properties of a CNF formula?
I suggest to borrow physics intuition that "less random" structures are more symmetric. Symmetry for CNF is any transformation of the variables, that keeps the function invariant. By that criteria, functions of 3 variables such as 

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

or, say, 

$\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}).$ 

are less random than, say 

$\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}) .$ 

In general, defining a concept of "random" on finite structures is challenging. Historically, it was tried on binary sequences, which arguably are the simplest finite structures. For example, intuitively, a sequence 01010101 is "less random" than, say, 01001110. However, it was quickly realized that there is no consistent formal definition of finite random sequence! Therefore, one have to be skeptical of any naive attempts to define a measure of randomness for any finite structure.