The Impact of Entropy and Solution Density on Selected SAT Heuristics.

We present a new characterization of propositional formulas called , which approximates the freedom we have in assigning the variables. Like several other such measures (e.g., back-door and back-door-key variables), it is computationally expensive to compute. Nevertheless, for small and medium-size satisfiable formulas, it enables us to study the effect of this freedom on the impact of various SAT heuristics, following up on a recent study by C. Oh (Oh, SAT'15, , 307-323). Oh's findings were that the expected success of various heuristics depends on whether the input formula is satisfiable or not. With entropy, and also with the measure of , we are able to refine these findings for the case of satisfiable formulas. Specifically, we found empirically that satisfiable formulas with small entropy "behave" similarly to unsatisfiable formulas.