Streamlining Variational Inference for Constraint Satisfaction Problems
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.
The article proposes a method for adding streamlining constraints in the survey propagation procedure, which improves its performance on random k-SAT problems. In line with classical survey propagation, they use a message passing procedure to compute approximate marginal. However instead of using the marginal to set single variables in the decimation process as previously done in survey propagation, the authors propose to add constraints based upon multiple variables. Iterating this procedure, more highly constrained problems are produced, which can then be solved by a downstream solver. The authors show that this idea improved upon a state-of-the-art survey propagation solver.  The article is well written, presents a novel and effective idea that I expect to see used in future SAT-competitions. While perhaps needed for the target audience of NIPS, I personally find the background section where previous algorithms are presented a bit too long. A substantial part of the paper is dedicated to the background that the reader could have easily been directed to by citations.   I have reviewed this paper at UAI 2017. I voted for acceptance at that time, and I am still leaning towards accepting this paper. One reviewer at UAI 2017 raised highly valid points, which is that incorrect and highly imprecise claims are made in several parts of the paper. I am very glad to see that the authors at least made some effort in revising these overclaiming statements. For example, now the authors only claim that their solvers outperform decimation-only solvers for random k-SAT instances in the abstract, instead of saying outperforming all solvers.  There are still a few places that I am going to bring authors’ attention. In particular, the authors should not make an implication that their method is analogous to streamlining random constraints in model counting, as in [2, 3, 14]. Agreed with reviewer 2 from UAI 2017, I think the contexts are entirely different, and the counting approaches in [2, 3, 14] simply cannot work with very short constraints, such as length-2 constraints used in this paper. I really think the authors should revise their statements in the third paragraph of the introduction.   Once this paper is converted to NIPS style, Figure 2 becomes way too small. Please enlarge the fonts in Figure 2. In addition, below are my detailed comments from UAI 2017.  On the technical side, there are a few directions that are not explored as much as would be ideal. First, the streamlining clauses are added based on the two most polarized variables. As an alternative, we can define a slightly different message passing algorithm which computes the marginal of the disjunction of all pairwise variables. Then we add streamlining constraints based on the pairwise marginal, instead of selecting the two most polarized variables assuming the independence. Will this be a better method?  The algorithmic design choices of section 3.3 could have been motivated more clearly. In particular, it would be interesting to plot how different choices affect the performance. Secondly, the constraints are just added to a single solver which is treated like a black box. To make the case of generality for the method, it would be preferable to use more solvers or have a metric of success that doesn’t depend on the selected black-box solver.   There are also a few presentation details that should be addressed. In section 3.3 the reader is directed to a theorem 1 which does not exist, I assume that it is supposed to be proposition 1. It is assumed that the three rows of figure 3 related to the same run - that could however be made clearer in the caption. In the introduction, only very recent work related to the phase transition of k-SAT is referred to. It would be good to cite several original publications.