Large language models (LLMs) have achieved strong performance in mathematical and logical reasoning, yet they still suffer from the curse of complexity and struggle as problem difficulty increases with the number of constraint interactions and the size of the search space. In contrast, satisfiability solvers such as Z3 provide scalable and verifiable reasoning through constraint solving under formal theories, but lack the flexibility to interpret natural-language problem descriptions. In this work, we propose SAT-RL, a reinforcement-learning (RL) framework that trains LLMs to interact with symbolic solvers through multi-turn tool execution. SAT-RL leverages synthetic data generation with verifiable solutions, supervised warm-up on solver-augmented traces, and solver-grounded reinforcement learning with tool-aware rewards. Experiments show that SAT-RL substantially improves symbolic reasoning with tools on both in-domain and out-of-domain logic tasks. Our code is available on https://github.com/sunjia72/SAT-RL.
Figures & tables
Figure 1: Workflow of the SAT-RL framework. Stage 1 ( left ) illustrates template-based data generation for the SFT phase: tasks and output programs are instantiated with randomized parameters to produce natural-language problems paired with ground-truth solver programs and executable responses. Stage 2 ( right ) illustrates the RL training phase and its reward components.
Resource
Tasks
Controlled Difficulty
Scalable
NP-hardness
Verifier
Solution Program
SAT-Bench ( Wei et al., 2025 )
1
✓
✗
✓
✓
✗
ZebraLogic ( Lin et al., 2025 )
1
✓
✓
✓
✓
✗
FCoReBench ( Mittal et al., 2024 )
40
✓
✓
✗
✗
✗
Enigmata ( Chen et al., 2025 )
36
✓
✓
✓
✓
✗
Synthetic-Logic (Ours)
48
✓
✓
✓
✓
✓
Table 1: Comparison of logical reasoning benchmarks across different features.
Data Type
Count
Total
48
Number of Tasks
16
Number of Queries
3
Primary Task Category
Puzzle Games
5
Program Verification
2
Table 2: Task statistics for Synthetic-Logic. Task types are assigned based on the primary problem structure, and each task is counted under exactly one category.
Dataset / Partition
Train
Test
Total
Synthetic-Logic (SFT)
1,260
139
1,399
SAT-Bench (RL)
1,575
525
2,100
Enigmata (Evaluation)
-
1,901
1,901
Table 3: Sizes of the training and test splits for each dataset.
Figure 2: Training trajectories on SAT-Bench for ReTool and SAT-RL (mean ± population standard deviation across three runs). Left : validation correctness. Right : policy entropy.
Model
Accuracy (%)
Base LLMs
GPT-5.6 Luna
92.0
Claude Sonnet 5
93.0
Claude Haiku 4.5
56.0
Qwen3.5-4B
19.8
Qwen3.5-9B
14.1
Table 4: In-domain Avg@8 test accuracy (%) on the SAT-Bench test set, which contains 525 instances. For trained models, accuracy is reported as the mean ± standard deviation.
Model
Overall
Difficulty
Category
Easy
Medium
Hard
Arithmetic
Graph
Grid
Logic
Sequential
Search
Crypto
Base LLMs
GPT-5.6 Luna
70.9
78.2
68.5
67.1
100.0
74.5
81.4
63.9
57.7
52.2
91.7
Claude Sonnet 5
72.5
72.0
72.3
73.2
100.0
66.8
86.1
75.6
52.0
62.2
86.7
Claude Haiku 4.5
49.7
52.0
49.7
47.8
84.2
44.1
56.6
65.6
26.1
45.0
61.7
Qwen3.5-9B
33.9
47.0
33.2
24.2
70.0
37.3
42.7
45.0
18.4
23.8
15.0
Table 5: Out-of-domain Avg@1 accuracies (%) on the Enigmata test set (1,901 instances), reported overall and across difficulty levels and puzzle categories. Details about the categories are provided in Appendix A .
Setup
Accuracy
Equivalence
SAT-RL
97.2 ± 0.8
94.0 ± 1.7
w/o SFT
54.9 ± 8.4
48.1 ± 6.1
w/o TS
97.0 ± 2.2
93.9 ± 4.3
w/o requiv
91.2 ± 2.0
80.6 ± 3.1
Table 6: In-domain final-answer accuracy and logic-equivalence rate of the encoded formulas (%) on SAT-Bench for Qwen3.5-9B under ablations. “TS” stands for Tool Sampling.
Figure 3: Logic-equivalence trajectories on SAT-Bench. In the “w/o Logic Equivalence” ablation, requiv is computed but excluded from the training reward.
Figure 4: Distribution of symbolic solver usage with tool sampling enabled ( left ) and disabled ( right ).
Appendix figures & tables3 assets
Supplementary material from the paper’s appendix.
Appendix
Data Type
Number of Instances
All instances
1901
Difficulty
Easy
560
Medium
642
Hard
699
Puzzle category
Appendix
Table 7: Number of instances in the Enigmata test set, grouped by difficulty, puzzle category, and puzzle name.
Software Environment
Python
3.12.13
CUDA Toolkit
12.9
PyTorch
2.11.0
verl
0.8.0
vLLM
0.19.1
transformers
5.5.4
Appendix
Table 8: Training configuration.
Figure 5: SAT-RL training trajectories on SAT-Bench for Qwen3.5-4B and Qwen3.5-9B. Curves show means over three runs; shading shows population standard deviation.