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?