# The impact of Entropy and Solution Density on selected SAT heuristics

## TL;DR

This paper investigates how entropy and solution density of satisfiable formulas influence the effectiveness of SAT heuristics, revealing that these properties can predict heuristic performance and that low-entropy formulas behave like unsatisfiable ones.

## Contribution

It introduces entropy and solution density as predictive properties for SAT heuristics, extending prior work by focusing on satisfiable formulas and their heuristic behavior.

## Key findings

- Entropy and solution density better predict heuristic effectiveness.
- Satisfiable formulas with low entropy behave similarly to unsatisfiable formulas.

## Abstract

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.