# Learning Branching Heuristics for Propositional Model Counting

arXiv: https://arxiv.org/abs/2007.03204 · HTML: https://mlsanity.com/paper/2007.03204/

## Key facts

- Cited by 9 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 7 Jul 2020.

## Built on by (most cited first, 9 of 9)

- [Combinatorial optimization and reasoning with graph neural networks](https://mlsanity.com/paper/2102.09544/) (2021)
- [LTL2Action: Generalizing LTL Instructions for Multi-Task RL](https://mlsanity.com/paper/2102.06858/) (2021)
- [LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning](https://mlsanity.com/paper/2101.06223/) (2021)
- [Augment with Care: Contrastive Learning for Combinatorial Problems](https://mlsanity.com/paper/2202.08396/) (2022)
- [NSNet: A General Neural Probabilistic Framework for Satisfiability Problems](https://mlsanity.com/paper/2211.03880/) (2022)
- [General Method for Solving Four Types of SAT Problems](https://mlsanity.com/paper/2312.16423/) (2023)
- [UNSAT Solver Synthesis via Monte Carlo Forest Search](https://mlsanity.com/paper/2211.12581/) (2022)
- [torchmSAT: A GPU-Accelerated Approximation To The Maximum Satisfiability Problem](https://mlsanity.com/paper/2402.03640/) (2024)
- [Attn-JGNN: Attention Enhanced Join-Graph Neural Networks](https://mlsanity.com/paper/2510.15583/) (2025)

## Abstract (arXiv)

Propositional model counting, or #SAT, is the problem of computing the number of satisfying assignments of a Boolean formula. Many problems from different application areas, including many discrete probabilistic inference problems, can be translated into model counting problems to be solved by #SAT solvers. Exact #SAT solvers, however, are often not scalable to industrial size instances. In this paper, we present Neuro#, an approach for learning branching heuristics to improve the performance of exact #SAT solvers on instances from a given family of problems. We experimentally show that our method reduces the step count on similarly distributed held-out instances and generalizes to much larger instances from the same problem family. It is able to achieve these results on a number of different problem families having very different structures. In addition to step count improvements, Neuro# can also achieve orders of magnitude wall-clock speedups over the vanilla solver on larger instances in some problem families, despite the runtime overhead of querying the model.