Reproduce “Learning Branching Heuristics for Propositional Model Counting” on OpenResearch

About this paper

Pashootan Vaezipoor, Gil Lederman, Yuhuai Wu, Chris J. Maddison, Roger Grosse, Sanjit A. Seshia, Fahiem Bacchus

Researchers from the University of Toronto, UC Berkeley, and Vector Institute developed Neuro#, a Graph Neural Network-based branching heuristic for exact propositional model counting (#SAT) solvers. This approach, trained with Evolution Strategies, reduced branching steps by up to 613x and achieved wall-clock speedups on large, complex problem instances, demonstrating effective upward generalization from smaller training data.

Key insights

• Learning problem-family-specific heuristics with GNNs and ES can yield superlinear reductions in branching steps and translate into substantial wall-clock speedups on larger, more challenging instances.
• The learned heuristics demonstrate robust upward generalization, effectively performing on instances orders of magnitude larger than those used for training, mitigating the need for costly training on large problems.
• Incorporating specific problem-level features (e.g., a 'time-step' feature in `grid wrld`) can significantly enhance the learned policy's performance by reintroducing structural information lost in generic CNF encoding.

Summary by alphaXiv.