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:

1. 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").

2. 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$.

3. 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

1. 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.
2. 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

1. Did anyone ever proposed a way to measure the randomness of a CNF formula?
2. 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?
• see the paper in this answer (cstheory.stackexchange.com/questions/4321/…). It could give you a tip on how to define such r – Marcos Villagra Feb 1 '11 at 0:54
• possibly relevant discussion on measuring randomness of bit-strings mathoverflow.net/questions/37518/… – Yaroslav Bulatov Feb 1 '11 at 3:25
• I can tell you this much since I have been working on this by myself for a while. If you consider SAT, the formulas for 1 & 2 are exponential. On the other hand for k-SAT the formulas for 1 & 2 are polynomial. This relates to my PRECISE DEFINITION OF RANDOM K-SAT QUESTION, which no one seems to want to answer. – Tayfun Pay Feb 1 '11 at 22:35
• @Geekster: Would you like to provide an answer here? – Hsien-Chih Chang 張顯之 Feb 2 '11 at 4:37
• @Geekster: What do you mean with "...the formulas for 1 & 2 are exponential"? – Giorgio Camerani Feb 2 '11 at 8:34

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.

• I totally agree with the intuition "structure means presence of symmetries, whereas randomness means absence of symmetries". You refer to syntactic symmetries (whereas semantic symmetries are those changing the function but leaving the solution space unaltered). I've been always convinced that symmetries are the key. – Giorgio Camerani Feb 2 '11 at 8:48
• @Walter: The idea of symmetries is an attempt to leverage algebra rather than algorithms: algorithmic complexity is a measure that defies consistent definition for finite objects. But then we have to assign complexity measure to each element a group (for example, transformation that negates a single variable is simpler than the one that negates two)-- this feels like just pushing the problem around... – Tegiri Nenashi Feb 2 '11 at 17:15