Consistency-Driven Neuro-Symbolic SAT Ensemble

Neural networks have recently emerged as a third paradigm for Boolean satisfiability (SAT) solving, alongside complete and stochastic local-search solvers, with independently trained models offering complementary predictions on the same formula, yet frequently disagreeing on the assignments they produce. To date, no ensemble method has been developed for aggregating the outputs of multiple neural SAT solvers, and a naive application of classical ensemble techniques would only reduce this disagreement to scalar per-variable metrics such as vote counts, discarding the relational structure between variables that is essential for constructing a consistent satisfying assignment. We present cdNSE, a new consistency-driven ensemble method for neuro-symbolic SAT solvers. We develop a mathematical framework to characterize consistency among solver outputs, capturing both agreement on variable assignments and on relationships between variables. These equivalence relations allow us to group variables where the ensemble shows consistent voting, which significantly reduces the search space for local search. We benchmark cdNSE against eleven fusion-based and ten learning-based methods on $123$ instances from six SATLIB datasets. cdNSE improves the solve rate by a relative improvement of $14.1\%$ over the strongest baseline and requires $27.1\%$ fewer flips to find a solution. When we increase the flip-budget for the local search engine, cdNSE achieves a $91.1\%$ solve rate, compared to $83.7\%$ for the strongest baseline method.