The impact of Entropy and Solution Density on selected SAT heuristics
This work provides incremental insights for SAT solver developers by linking formula properties to heuristic performance.
The study investigated how entropy and solution density of satisfiable SAT formulas predict the effectiveness of key heuristics, finding that these properties better explain heuristic impact and that satisfiable formulas with low entropy behave like unsatisfiable ones.
In a recent article [Oh'15], Oh examined the impact of various key heuristics (e.g., deletion strategy, restart policy, decay factor, database reduction) in competitive SAT solvers. His key findings are that their expected success depends on whether the input formula is satisfiable or not. To further investigate these findings, we focused on two properties of satisfiable formulas: the entropy of the formula, which approximates the freedom we have in assigning the variables, and the solution density, which is the number of solutions divided by the search space. We found that both predict better the effect of these heuristics, and that satisfiable formulas with small entropy `behave' similarly to unsatisfiable formulas.