Correlations between Horn fractions, satisfiability and solver performance for fixed density random 3-CNF instances

An enhanced concept of sub-optimal reverse Horn fraction of a CNF-formula was introduced in 18]. It was shown that this fraction is very useful in effectively (almost) separating 3-colorable random graphs with fixed node-edge density from the non-3-colorable ones. A correlation between this enhanced sub-optimal reverse Horn fraction and satisfiability of random 3-SAT instances with a fixed density was observed. In this paper, we present experimental evidence that this correlation scales to larger-sized instances and that it extends to solver performances as well, both of complete and incomplete solvers. Furthermore, we give a motivation for various phases in the algorithm aHS, establishing the enhanced sub-optimal reverse Horn fraction, and we present clear evidence for the fact that the observed correlations are stronger than correlations between satisfiability and sub-optimal MAXSAT-fractions established similarly to the enhanced sub-optimal reverse Horn fraction. The latter observation is noteworthy because the correlation between satisfiability and the optimal MAXSAT-fraction is obviously 100%. AMS subject classification 90C05, 03B99, 68Q01, 68W01