On the imbalance of distributions of solutions of CNF formulas and its impact on satisfiability solvers
Ewald Speckenmeyer, Max Böhm, Peter Heusch · DIMACS series in discrete mathematics and theoretical computer science · 1997
Let F be Boolean formulas in conjunctive normal form with n variables, r clauses, every clause has length s.We show that if F is split into two subformulas F v and F v by setting v true and false in F , then the expected number of solutions of one of the two subformulas F v and F v is signi cantly higher than that in the other subformula, when dealing with classes of formulas where the great majority of formulas is satis able.We discuss practical consequences of this result.