Streamlining constraints for random k-SAT

Several competitive algorithms for random k-SAT are based on survey propagation, a variational inference scheme used to obtain approximate marginals. These marginals are used to inform branching decisions during search; however, survey propagation marginals are approximate and this can lead to contradictions. 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-only solvers for random k-SAT 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.