  Several algorithms for solving constraint satisfaction problems are based on
survey propagation, a variational inference scheme used to obtain approximate
marginal probability estimates for variable assignments. These marginals
correspond to how frequently each variable is set to true among satisfying
assignments, and are used to inform branching decisions during search; however,
marginal estimates obtained via survey propagation are approximate and can be
self-contradictory. We introduce a more general branching strategy based on
streamlining constraints, which sidestep hard assignments to variables. We show
that streamlined solvers consistently outperform decimation-based solvers on
random k-SAT instances for several problem sizes, shrinking the gap between
empirical performance and theoretical limits of satisfiability by 16.3% on
average for k=3,4,5,6.
