Learning How to Cube

TL;DR

This paper demonstrates that transformer-based models can learn effective cubing heuristics for SAT solving, outperforming some symbolic methods through a novel neuro-symbolic training framework.

Contribution

Introduces a neuro-symbolic post-training framework with MCTS-based data curation and preference optimization for SAT cubing heuristics in transformers.

Findings

A 4B-parameter model achieves pass@5 score of 53 on SAT benchmarks.

Supervised fine-tuning improves performance from 46 to 51, DPO adds 2 more benchmarks.

Transformers can effectively learn cubing decisions traditionally dominated by symbolic methods.

Abstract

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.