NIPS 2018
Sun Dec 2nd through Sat the 8th, 2018 at Palais des Congrès de Montréal
Paper ID: 6749 Streamlining Variational Inference for Constraint Satisfaction Problems

### Reviewer 1

The work proposes the use of streamlining in the context of survey inspired decimation algorithms---a main approach alongside stochastic local search---for effciiently finding solutions to large satisfiable random instances of the Boolean satisfiability (SAT) problem. The paper is well-written and easy to follow (although some hasty mistakes remain, see below). The proposed approach is shown to improve the state of the art (to some extent) in algorithms for solving random k-SAT instances, especially by showing that streamlining constraints allow for solving instances that a closer to the sat-unsat phase transition point than previously for different values of k. In terms of motivations, while I do find it of interest to develop algorithmic approach which allow for more efficiently finding solutions to the hardest random k-SAT instances, it would be beneficial if the authors would expand the introduction with more motivations for the work. In terms of contributions, the proposal consists essentially of combining previous proposed ideas to obtain further advances (which is of course ok, but slightly lowers the novelty aspects). The proposed changes are not very deep, but the empirical results are quite good and the experiments seem well-performed. I find it especially interesting that the state-of-the-art Dimetheus solver benefits from the proposed idea. More detailed comments: Lines 48-49: The claim is not totally correct; DPLL and CDCL algorithm could in principle easily be made to branch on more complex Boolean combinations, the challenge is more in coming up with effective heuristics for doing this. Line 81: "most" solvers is claiming too much. More traditional stochastic local search is also a n active area of development, and it is not entirely clear which approach currently prevails and when. In fact, the newest results from the SAT Competition will be available in a week or so, and the authors can check the situation and perhaps comment on this in the paper. http://sat2018.forsyte.tuwien.ac.at Line 107-108: reference are broken! Section 3.1: The authors should comment on the claim that increasing length of streamlining constraints is a "straightforward extension". The number of such constraints is exponential in the length, I to me it is not at all evident how to go about choosing from such an exponential set when increasing the length? I wonder if there are more practical reasons for restricting to length 2 ... In the beginning of Section 4.2 it would be good to explicate whether the alpha reached is the best one that has ever been reached, or has this been done before? Line 239: $T$ Many of the plots are semi-unreadable on a black-and-white printout. The resolution of the images should be improved and the plots made larger (or otherwise more readable). As a final comment, I would encourage the authors to submit the solver to the random SAT track of the next edition of the SAT Competitions. AFTER AUTHOR RESPONSE: Thank you for the constructive author response. I maintain my positive view on the work. It will be very interesting to see the results for Sparrow2Riss.

### Reviewer 2

In this work, a new branching strategy for survey propagation is proposed. Specifically, the paper introduce 'streamlining constraint' in place of using decimation, which adds disjunction contraints between subsets of highly magnetized variables. The algorithm is empirically reported to improve existing k-SAT solvers. In overall, the paper was easy to read and idea seemed novel to me. I liked how the extension from decimation to streamline was very simple, but possess the potential to provoke further related works. My only concern on the scheme itself is that adding streamlining constraints will increase the size of problem (as mentioned briefly in paper), and reporting how much the algorithm is slower than just using decimation would make the paper more useful for practical applications. Minor comments: - In algorithmic design choices, it seems rather natural to use memory threshold in place of iteration threshold, since it is a more closely related quantity to our computational resources. For example, one could think of a scheme which combines streamlining and decimation by adding streamlining constraint whenever memory is possible, and using decimation otherwise. - In context of MAP inference in undirected graphical models (GMs), there is a similar scheme that is called 'uprooting and rerooting', which modifies the GM while keeping the MAP assignment invariant. It would be very interesting to see whether if similar scheme is effective in max-product belief propagation for GMs. --- I have read the author's reponse and considered it in my review.