# Learning How to Cube

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

## Key facts

- No citing papers in the map yet (data through 7 Oct 2026).
- Placed in Process reward models for reasoning, one of 10 directions in LLM alignment / RLHF / preference optimisation.
- Builds on 14 of its 42 references that are in the map.
- First posted on arXiv 15 May 2026.

## Placed in

- LLM alignment / RLHF / preference optimisation / [Process reward models for reasoning](https://mlsanity.com/alignment/process-reward-models-for-reasoning/)

## Builds on (most cited first, 14 of 14)

- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Direct Preference Optimization: Your Language Model is Secretly a Reward Model](https://mlsanity.com/paper/2305.18290/) (2023)
- [Efficient Memory Management for Large Language Model Serving with PagedAttention](https://mlsanity.com/paper/2309.06180/) (2023)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Scaling LLM Test-Time Compute Optimally can be More Effective than Scaling Model Parameters](https://mlsanity.com/paper/2408.03314/) (2024)
- [Learning a SAT Solver from Single-Bit Supervision](https://mlsanity.com/paper/1802.03685/) (2018)
- [SatLM: Satisfiability-Aided Language Models Using Declarative Prompting](https://mlsanity.com/paper/2305.09656/) (2023)
- [Guiding High-Performance SAT Solvers with Unsat-Core Predictions](https://mlsanity.com/paper/1903.04671/) (2019)
- [Can Transformers Reason Logically? A Study in SAT Solving](https://mlsanity.com/paper/2410.07432/) (2024)
- [GraSS: Combining Graph Neural Networks with Expert Knowledge for SAT Solver Selection](https://mlsanity.com/paper/2405.11024/) (2024)
- [Community Structure in Industrial SAT Instances](https://mlsanity.com/paper/1606.03329/) (2016)
- [UNSAT Solver Synthesis via Monte Carlo Forest Search](https://mlsanity.com/paper/2211.12581/) (2022)
- [AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problems](https://mlsanity.com/paper/2401.13770/) (2024)
- [Global Benchmark Database](https://mlsanity.com/paper/2405.10045/) (2024)

## Abstract (arXiv)

Despite the effectiveness of Cube-and-Conquer (C&C) for solving challenging Boolean Satisfiability (SAT) problems, no prior work has shown that transformer-based models can learn effective cubing heuristics. We introduce a neuro-symbolic post-training framework for this task. We design an MCTS-based data curation pipeline that uses symbolic heuristics to explore splitting decisions over SAT competition formulas, producing preference data grounded in solver statistics and augmented with reasoning traces from a teacher model. Our two-stage post-training, supervised fine-tuning (SFT) followed by direct preference optimization (DPO), enables a 4B-parameter model to achieve a pass@5 score of 53 on 100 SAT competition benchmarks, surpassing frontier LLMs such as Claude-Sonnet-4 (50) and matching the best symbolic heuristic (53). Ablations show that SFT alone improves pass@5 from 46 to 51, with DPO adding 2 additional benchmarks; an entropy/agreement ablation on realized first-cube decisions further shows that SFT, not DPO, accounts for the root-level decision diversity that produces complementary per-run coverage over deterministic symbolic methods. This demonstrates that transformers can be trained to make effective cubing decisions in a domain traditionally dominated by symbolic methods.