SAT-RL：借助符号求解器训练语言模型进行逻辑推理

# SAT-RL: Training Language Models for Logical Reasoning with Symbolic Solvers
Source: [https://arxiv.org/html/2610.14402](https://arxiv.org/html/2610.14402)
###### Abstract

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[GitHub](https://github.com/sunjia72/SAT-RL)\.

## 1Introduction

Large language models \(LLMs\) have demonstrated strong capabilities on mathematical and logical reasoning tasks, including the Law School Admission Test \(LSAT\), the International Mathematical Olympiad \(IMO\), and broad AGI datasets such as AGI\-Eval\([Zhong et al\., 2021](https://arxiv.org/html/2610.14402#bib.bib50);[Ren et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib52);[Zhong et al\., 2024](https://arxiv.org/html/2610.14402#bib.bib51)\)\. In particular, reinforcement learning \(RL\) has played a central role in these advances by enabling long\-horizon reasoning, self\-verification, and agentic tool calling\([Schulman et al\., 2017](https://arxiv.org/html/2610.14402#bib.bib39);[Guo et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib12);[Shao et al\., 2024](https://arxiv.org/html/2610.14402#bib.bib41);[Yu et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib43)\)\. Despite this progress, recent work on logical reasoning benchmarks\([Lin et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib10);[Wei et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib2);[Chen et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib38)\)shows that LLMs suffer from a curse of complexity, in which accuracy drops significantly as the number of constraints and the size of the search space increase\. Incorporating symbolic checking further reveals that this accuracy degradation is related to systematic constraint violations and a persistent gap between reasoning rationales and verifiable correctness\([Qi et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib49)\)\.

On the other hand, symbolic solvers such as Boolean satisfiability \(SAT\) solvers, satisfiability modulo theories \(SMT\) solvers, and first\-order theorem provers \(TPs\) can scale to large combinatorial spaces and produce reliable logical deductions by finding satisfying assignments or proofs of unsatisfiability under well\-defined theories\. Commonly used solvers include CaDiCaL\([Ignatiev et al\., 2018](https://arxiv.org/html/2610.14402#bib.bib48)\), Z3\([de Moura and Bjørner, 2008](https://arxiv.org/html/2610.14402#bib.bib19)\), cvc5\([Barbosa et al\., 2022](https://arxiv.org/html/2610.14402#bib.bib20)\), and Vampire\([Riazanov and Voronkov, 2001](https://arxiv.org/html/2610.14402#bib.bib21)\), most of which have Python interfaces available through PyPI packages\. Inspired by this reliability, a line of research has combined LLMs with symbolic solvers\. For example, SAT\-LM\([Ye et al\., 2023](https://arxiv.org/html/2610.14402#bib.bib5)\)and Logic\-LM\([Pan et al\., 2023](https://arxiv.org/html/2610.14402#bib.bib1)\)encode natural\-language logic tasks into formal constraints and invoke Z3 in a one\-shot declarative query, while other systems such as SymPro\-LM\([Mittal et al\., 2024](https://arxiv.org/html/2610.14402#bib.bib24)\)and MCP\-Solver\([Szeider, 2024](https://arxiv.org/html/2610.14402#bib.bib25)\)support agentic multi\-turn interactions with solver feedback and self\-correction\. However, these methods operate only at inference time and rely on solver\-specific knowledge implicitly learned during pretraining, making them vulnerable to program errors\. Moreover, they offer limited means of aligning solver encodings with the constraints in the original problem statements\.

Rather than treating symbolic solvers as fixed inference\-time heuristics, a promising research direction is to integrate LLMs with symbolic solvers through training that ensures the reliability of reasoning traces and optimizes interactions between LLMs and symbolic solvers\. To close this gap, we introduce SAT\-RL, a framework that enables LLMs to plan and iteratively refine symbolic solver calls using reinforcement learning\. The framework consists of two major components: \(i\) a stage for generating synthetic logic data with ground\-truth solvers and verifiers to support supervised fine\-tuning \(SFT\) warm\-up, and \(ii\) an RL stage with verifiable rewards and instance\-conditioned solver\-tool sampling to guide exploration\. Overall, SAT\-RL aims to produce hybrid reasoning systems that retain natural\-language accessibility while achieving scalable, faithful, and verifiable logical reasoning across diverse problem domains\.

## 2Related Work

### 2\.1Benchmarks for Logical Reasoning

Benchmarks for logical reasoning span natural\-language comprehension, formal validity, and verifiable constraint puzzles\. Reading\-comprehension datasets such as LogiQA\([Liu et al\., 2020](https://arxiv.org/html/2610.14402#bib.bib28);[Liu et al\., 2023](https://arxiv.org/html/2610.14402#bib.bib29)\)and ReClor\([Yu et al\., 2020](https://arxiv.org/html/2610.14402#bib.bib30)\)test multiple\-choice logical inference over passages, while CLUTRR\([Sinha et al\., 2019](https://arxiv.org/html/2610.14402#bib.bib31)\)targets relational induction over narratives\. Formal corpora such as FOLIO and P\-FOLIO\([Han et al\., 2024a](https://arxiv.org/html/2610.14402#bib.bib6);[Han et al\., 2024b](https://arxiv.org/html/2610.14402#bib.bib7)\), RuleTaker\([Clark et al\., 2020](https://arxiv.org/html/2610.14402#bib.bib8)\), and LogicNLI\([Tian et al\., 2021](https://arxiv.org/html/2610.14402#bib.bib9)\)emphasize first\-order validity or entailment with more explicit logical structure and, in the case of P\-FOLIO, proof\-chain annotations\. A complementary line of work uses programmatically generated puzzles with exact solution checking: SAT\-Bench\([Wei et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib2)\)randomly samples SAT formulas and creates instances with LLM annotations, ZebraLogic and BoardgameQA\([Lin et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib10);[Kazemi et al\., 2023](https://arxiv.org/html/2610.14402#bib.bib11)\)provide scalable generators with difficulty control, and Enigmata\([Chen et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib38)\)broadens coverage across 36 puzzle families\. Recent work emphasizes robustness to memorization through automatic generation in AutoLogi\([Zhu et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib37)\)and periodic refreshes in NPHardEval\([Fan et al\., 2024](https://arxiv.org/html/2610.14402#bib.bib34)\), and broadens puzzle coverage with long\-tail game settings in HardcoreLogic\([Liang et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib32)\)\. Complementary evaluation efforts such as LogicBench and Multi\-LogiEval\([Parmar et al\., 2024](https://arxiv.org/html/2610.14402#bib.bib36);[Patel et al\., 2024](https://arxiv.org/html/2610.14402#bib.bib35)\)assemble multi\-step logical test suites, while CFBench\([Zhang et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib33)\)evaluates whether models can satisfy explicit constraints in generated outputs\.

### 2\.2Logical Reasoning with LLMs

Prompting techniques, such as chain\-of\-thought \(CoT\), tree\-of\-thought \(ToT\), and self\-consistency sampling, improve decomposition and search over candidate responses\([Wei et al\., 2022](https://arxiv.org/html/2610.14402#bib.bib17);[Yao et al\., 2023](https://arxiv.org/html/2610.14402#bib.bib4);[Wang et al\., 2022](https://arxiv.org/html/2610.14402#bib.bib18)\)\. Several studies focus on coupling LLMs with external symbolic solvers to enable verifiable reasoning steps: SAT\-LM\([Ye et al\., 2023](https://arxiv.org/html/2610.14402#bib.bib5)\)issues a one\-shot declarative query to Z3\([de Moura and Bjørner, 2008](https://arxiv.org/html/2610.14402#bib.bib19)\), while MCP\-Solver\([Szeider, 2024](https://arxiv.org/html/2610.14402#bib.bib25)\)supports iterative constraint\-model construction and validation through a structured interface for Z3, PySAT\([Ignatiev et al\., 2018](https://arxiv.org/html/2610.14402#bib.bib48)\), and MiniZinc\([Nethercote et al\., 2007](https://arxiv.org/html/2610.14402#bib.bib47)\)\. FCoReBench\([Mittal et al\., 2024](https://arxiv.org/html/2610.14402#bib.bib24)\)targets first\-order combinatorial reasoning with scalable instances\.

RL can improve reasoning by directly optimizing model behavior under preference signals or reward functions\. Proximal Policy Optimization \(PPO\) remains a common RLHF backbone due to its stable on\-policy updates in large action spaces\([Schulman et al\., 2017](https://arxiv.org/html/2610.14402#bib.bib39)\)\. Direct Preference Optimization \(DPO\) avoids an explicit reward model by optimizing a closed\-form objective over pairwise preferences\([Rafailov et al\., 2023](https://arxiv.org/html/2610.14402#bib.bib40)\)\. Group Relative Policy Optimization \(GRPO\) estimates advantages from within\-group comparisons over multiple sampled responses, reducing reliance on value\-function learning\([Shao et al\., 2024](https://arxiv.org/html/2610.14402#bib.bib41)\)\. Recent variants refine policy\-gradient baselines or update rules for long\-horizon reasoning, including REINFORCE\+\+\([Hu, 2025](https://arxiv.org/html/2610.14402#bib.bib42)\)and OPO\([Hao et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib46)\)\. Self\-play\-based methods, such as SPIN and SPPO\([Chen et al\., 2024](https://arxiv.org/html/2610.14402#bib.bib45);[Wu et al\., 2024](https://arxiv.org/html/2610.14402#bib.bib44)\), generate preference data from model–model interactions to iteratively strengthen policies\. DAPO emphasizes stabilizing long\-horizon training through improved optimization and regularization\([Yu et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib43)\)\.

## 3Methods

![Refer to caption](https://arxiv.org/html/2610.14402v1/workflow.png)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\.Overall, we integrate long\-horizon reinforcement learning with multi\-turn tool calls to symbolic solvers\. The SAT\-RL pipeline comprises three stages: \(i\) a data generation and preprocessing stage for supervised fine\-tuning; \(ii\) an SFT stage that warms up the base policy model; and \(iii\) an RL stage that fine\-tunes the model using DAPO\([Yu et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib43)\), a variant of GRPO\([Shao et al\., 2024](https://arxiv.org/html/2610.14402#bib.bib41)\), while interleaving code execution via Sandbox Fusion\([Bytedance\-Seed\-Foundation\-Code\-Team et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib22)\)as the MCP backend\. We first introduce the notation and problem formulation and then describe the proposed methods in detail\.

### 3\.1Preliminaries

#### Notation\.

We denote the trainable policy model byπθ\\pi\_\{\\theta\}, whereθ\\thetadenotes the model parameters\. The conditional distribution over outputs is given by

πθ​\(y∣x\)=∏t=1TP⁡\(yt∣y<t,x,θ\)\\pi\_\{\\theta\}\(y\\mid x\)=\\prod\_\{t=1\}^\{T\}P\(y\_\{t\}\\mid y\_\{<t\},x,\\theta\)wherexxis the input query andy=\(y1,…,yT\)y=\(y\_\{1\},\\ldots,y\_\{T\}\)is the output token sequence\.

Throughout the paper, we use the term symbolic solvers to collectively refer to the following PyPI distributions:z3\-solver,pysmt,python\-sat,ortools, andsympy\. In particular, Z3\([de Moura and Bjørner, 2008](https://arxiv.org/html/2610.14402#bib.bib19)\)and PySMT are SMT interfaces supporting theories such as first\-order arithmetic over integers, reals, and bit\-vectors; PySAT \(python\-sat\) provides Python bindings to state\-of\-the\-art SAT and MaxSAT solvers; OR\-Tools is an optimization library for combinatorial and linear programming; and SymPy is a computer algebra system for symbolic mathematics with limited logical reasoning support\. A tool call refers to an executable program generated by the model and executed in a sandboxed environment during rollout\.

#### Problem Formulation\.

We study natural\-language \(NL\) logical reasoning tasks that admit a reduction to a satisfiability problem modulo a background theory\. Following prior work on solver\-grounded reasoning\([Ye et al\., 2023](https://arxiv.org/html/2610.14402#bib.bib5);[Qi et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib49)\), we formalize each problem instancePPas a 4\-tupleP=\(𝒯,V,Φ,q\)P=\(\\mathcal\{T\},V,\\Phi,q\), where𝒯\\mathcal\{T\}is a first\-order background theory,V=\{v1,…,vn\}V=\\\{v\_\{1\},\\dots,v\_\{n\}\\\}is a finite set of free variables,Φ\\Phiis a first\-order formula over the signature of𝒯\\mathcal\{T\}whose free variables are contained inVV, andqqis a query whose free variables are also contained inVV\. The theory𝒯\\mathcal\{T\}determines the semantics of the symbols and predicates appearing inΦ\\Phiandqq, including propositional logic, linear integer arithmetic, and linear real arithmetic\.

Letℳ𝒯​\(Φ,V\)\\mathcal\{M\}\_\{\\mathcal\{T\}\}\(\\Phi,V\)denote the set of𝒯\\mathcal\{T\}\-models that satisfyΦ\\Phiand interpret exactly the variables inVV:ℳ𝒯\(Φ,V\)=\{M∣M⊧𝒯Φanddom\(M\)=V\},\\mathcal\{M\}\_\{\\mathcal\{T\}\}\(\\Phi,V\)=\\\{\\,M\\mid M\\models\_\{\\mathcal\{T\}\}\\Phi\\;\\text\{and\}\\;\\mathrm\{dom\}\(M\)=V\\,\\\},where each modelMMassigns values to the variables inVVthat satisfyΦ\\Phi\. We consider the following query types:

- •Decision\.The decision taskDecide​\(P\)\\text\{Decide\}\(P\)asks whetherℳ𝒯​\(Φ,V\)\\mathcal\{M\}\_\{\\mathcal\{T\}\}\(\\Phi,V\)is non\-empty\. The output isTrueif and only if at least one model exists\.
- •Solving\.Given an optional optimization objective𝒪\\mathcal\{O\}, the solving taskSolve​\(P,𝒪\)\\text\{Solve\}\(P,\\mathcal\{O\}\)asks for a modelM∈argmaxM′∈ℳ𝒯​\(Φ,V\)​𝒪​\(M′\)M\\in\\underset\{M^\{\\prime\}\\in\\mathcal\{M\}\_\{\\mathcal\{T\}\}\(\\Phi,V\)\}\{\\operatorname\{argmax\}\}\\mathcal\{O\}\(M^\{\\prime\}\), or any modelM∈ℳ𝒯​\(Φ,V\)M\\in\\mathcal\{M\}\_\{\\mathcal\{T\}\}\(\\Phi,V\)if no objective is given\. Note that whenΦ\\Phiis a Boolean formula in conjunctive normal form \(CNF\), a typical MaxSAT problem sets𝒪\\mathcal\{O\}to be the number of satisfied clauses, whereas a SAT problem does not specify an objective\.
- •Counting\.The counting taskCount​\(P\)\\text\{Count\}\(P\)asks for the number of satisfying assignments, which equals the size of the model set\|ℳ𝒯​\(Φ,V\)\|\\bigl\|\\mathcal\{M\}\_\{\\mathcal\{T\}\}\(\\Phi,V\)\\bigr\|\.

#### Example\.

Consider the question: In how many distinct ways can a factory package exactly5050widgets using only 4\-widget and 6\-widget boxes? To model this instance using the 4\-tupleP=\(𝒯,V,Φ,q\)P=\(\\mathcal\{T\},V,\\Phi,q\)defined above, let𝒯\\mathcal\{T\}be linear integer arithmetic andV=\{x,y\}V=\\\{x,y\\\}, wherexxandyyrepresent the numbers of 4\-widget and 6\-widget boxes, respectively\. DefineΦ\\Phias\(4​x\+6​y=50\)∧\(x≥0\)∧\(y≥0\)\(4x\+6y=50\)\\wedge\(x\\geq 0\)\\wedge\(y\\geq 0\)\. The corresponding counting query asks forCount​\(P\)\\text\{Count\}\(P\)\. Since the satisfying models are\{\(2,7\),\(5,5\),\(8,3\),\(11,1\)\}\\\{\(2,7\),\(5,5\),\(8,3\),\(11,1\)\\\}, the answer is44\. A concrete OR\-Tools implementation is provided in Appendix[D](https://arxiv.org/html/2610.14402#A4)\.

### 3\.2Data Generation and Processing

Table 1:Comparison of logical reasoning benchmarks across different features\.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\.In this section, we describe the data processing procedures for SFT and RL training\. Our synthetic dataset, Synthetic\-Logic, is used to warm up the policy model during the SFT phase\. We leverage SAT\-Bench\([Wei et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib2)\)for RL training and Enigmata\([Chen et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib38)\)for evaluation\.

#### Synthetic Data Generation for SFT\.

We construct the Synthetic\-Logic dataset for SFT warm\-up by systematically selecting task families and generating verifiable puzzle instances under controlled difficulty\. Our dataset covers 16 logical reasoning tasks, including 9 drawn from Karp’s list of NP\-complete problems\([Karp, 2009](https://arxiv.org/html/2610.14402#bib.bib27)\), such as Subset Sum and the Traveling Salesman Problem \(TSP\)\. In addition, we include 7 further NP\-hard tasks, such as binarized neural network \(BNN\) verification and N\-Queens puzzles, with full task descriptions provided in Appendix[B\.1](https://arxiv.org/html/2610.14402#A2.SS1)\. Each task is instantiated for each of the three query types—decision, solving, and counting—as formalized in Section[3\.1](https://arxiv.org/html/2610.14402#S3.SS1.SSS0.Px2)\. Table[2](https://arxiv.org/html/2610.14402#S3.T2)summarizes the coverage of task categories\.

For each combination of task type, query type, and symbolic solver, we predefine a structured template consisting of a natural\-language problem description and a ground\-truth solver program implementing the formal constraint encoding\. Ground\-truth answers for decision and counting queries are obtained by executing the corresponding solver program, whereas responses to solving queries are validated using task\-specific verifiers that check the correctness of candidate witnesses produced by the model\. This design ensures that every instance is paired with an executable and verifiable reference trace grounded in the intended solver semantics\.

We randomly sample 10 instances for each fixed combination of task, query type, and solver across different difficulty parameter settings\. For decision problems, we target a balanced 50%/50% SAT/UNSAT split and discard instances that fail due to solver timeouts during ground\-truth execution\. This procedure yields 1,399 synthetic SFT𝒟SFT\\mathcal\{D\}\_\{\\text\{SFT\}\}instances after removing timeout instances, and they are split into 1,260 training and 139 test instances that are fully verifiable with ground\-truth responses and verifiers\.

#### Data Preprocessing for RL\.

We focus on logical reasoning datasets whose difficulty and size can be controlled\. For RL training, we use SAT\-Bench\([Wei et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib2)\), which consists of logic puzzles automatically generated from CNF formulas\. An LLM verbalizes each clause as a natural\-language constraint, and each problem poses a yes\-or\-no decision question asking whether the constraints are satisfiable\. Difficulty is controlled at generation time by the number of clauses and variables, with more clauses yielding harder puzzles\. SAT\-Bench includes a built\-in mapping between each sampled formula variable and the corresponding natural\-language entity, enabling SAT\-RL to compute the logic\-equivalence reward during training\.

#### Data Preprocessing for Evaluation\.

For out\-of\-distribution evaluation, we test the trained models on Enigmata\([Chen et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib38)\), a large collection of synthetic and verifiable logical and constraint\-based puzzles, such as Tic\-Tac\-Toe and the 24 Game\. Each instance requires the explicit construction of a satisfying assignment and includes a built\-in correctness verifier\. The final dataset sizes are reported in Table[3](https://arxiv.org/html/2610.14402#S3.T3)\.

Table 3:Sizes of the training and test splits for each dataset\.

### 3\.3Supervised Fine\-tuning

We initialize the trainable policy modelπθ\\pi\_\{\\theta\}by supervised fine\-tuning on the solver\-augmented dataset𝒟SFT\\mathcal\{D\}\_\{\\text\{SFT\}\}constructed in Section[3\.2](https://arxiv.org/html/2610.14402#S3.SS2)\. Each example\(x,y\)∈𝒟SFT\(x,y\)\\in\\mathcal\{D\}\_\{\\text\{SFT\}\}pairs an input promptxxwith a target responseyythat includes a valid solver program embedded within<tool\_call\>\.\.\.</tool\_call\>\. We train the policy model using the objective:

𝒥SFT​\(θ\)=𝔼\(x,y\)∼𝒟SFT​\[∑t=1\|y\|log⁡πθ​\(yt∣x,y<t\)\]\\mathcal\{J\}\_\{\\text\{SFT\}\}\(\\theta\)\\;=\\;\\mathbb\{E\}\_\{\(x,y\)\\sim\\mathcal\{D\}\_\{\\text\{SFT\}\}\}\\Biggl\[\\sum\_\{t=1\}^\{\|y\|\}\\log\\pi\_\{\\theta\}\\\!\\bigl\(y\_\{t\}\\mid x,y\_\{<t\}\\bigr\)\\Biggr\]
This warm start teachesπθ\\pi\_\{\\theta\}basic solver\-tool API usage, planning, and coding, and stabilizes subsequent RL by reducing early\-stage invalid tool executions\.

### 3\.4Reinforcement Learning

We fine\-tune the SFT\-initialized policy model with DAPO\([Yu et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib43)\)using multi\-turn tool execution\.

#### Tool Call Interface\.

We follow the ReTool paradigm\([Feng et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib26)\)to interleave natural\-language reasoning with executable solver calls\. The LLM emits reasoning tokensrir\_\{i\}within<think\>\.\.\.</think\>blocks and executable code or CLI commandscic\_\{i\}within<tool\_call\>\.\.\.</tool\_call\>blocks\. A sandbox compiles and executescic\_\{i\}and returns the resulting stdout and stderr as feedbackfif\_\{i\}within a<tool\_response\>\.\.\.</tool\_response\>block, which immediately follows the corresponding<tool\_call\>block\. The rollout thus interleaves reasoning, tool calls, and tool responses as

\[r1,c1,f1,…,rn,cn,fn,a\]\[r\_\{1\},\\,c\_\{1\},\\,f\_\{1\},\\,\\dots,\\,r\_\{n\},\\,c\_\{n\},\\,f\_\{n\},\\,a\]whereaais the final answer\.

We implement training using the verl\([Sheng et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib3)\)pipeline with agentic mode enabled\. For multi\-turn tool execution, we deploy an asynchronous code server via Sandbox Fusion to support parallel, high\-throughput solver execution\. We use the prompt in Appendix[C](https://arxiv.org/html/2610.14402#A3)to incentivize the policy model to use symbolic solvers and align variables with the problem context through the built\-in variable mapping in SAT\-Bench\([Wei et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib2)\)\.

#### Reward Design\.

Overall, we aim to incentivize the policy model to solve diverse logical reasoning problems by learning to query various symbolic solvers using faithful formula encodings\. The reward should focus not only on the correctness of the final answer but also on the quality of the encoded formula\. Thus, we define the total rewardrras the sum of four verifiable components: formatrformatr\_\{\\text\{format\}\}, correctnessrcorrectr\_\{\\text\{correct\}\}, compilabilityrtoolr\_\{\\text\{tool\}\}, and qualityrequivr\_\{\\text\{equiv\}\}\. All components are initialized to 0\.

For each instance, we uniformly sample one of the five solvers \(Z3, PySMT, PySAT, OR\-Tools, and SymPy\) as the required solver, thereby familiarizing the model with diverse solvers and avoiding collapse to a single solver backend during training\([Li et al\., 2026](https://arxiv.org/html/2610.14402#bib.bib23)\)\. To enable final\-answer parsing, we require the final answeraain the response to be enclosed in triple backticks using the`\`\`\`answer\`\`\``format and assign a format rewardrformat=0\.1r\_\{\\text\{format\}\}=0\.1when parsing succeeds\. For final\-answer evaluation, we reward correct answers, encourage an honestI don’t knowresponse under uncertainty, and penalize incorrect answers to discourage random guessing\. We allow an explicit abstention token \(rendered as`\`\`\`idk\`\`\``\) and define the adjusted correctness reward as follows:

rcorrect​\(a\)=\{1ifais correct0ifaisidk−1−εifais incorrectr\_\{\\text\{correct\}\}\(a\)=\\begin\{cases\}1&\\text\{if $a$ is correct\}\\\\ 0&\\text\{if $a$ is \{idk\}\}\\\\ \-1\-\\varepsilon&\\text\{if $a$ is incorrect\}\\end\{cases\}\(1\)Because the SAT\-Bench training set has only two possible final answers \(yes/no\), this design makes uniform random guessing strictly suboptimal in expectation\. The penalty for an incorrectaanaturally generalizes to−1n−1−ε\\frac\{\-1\}\{n\-1\}\-\\varepsilonfor multiple\-choice problems withnnchoices\.

We assign a tool\-syntax rewardrtool=0\.1r\_\{\\text\{tool\}\}=0\.1if the final tool call executes without compilation errors and uses the sampled solver\. Beyond compilability, we also judge the quality of the solver call based on the logical similarity between the ground\-truth formula and the proposed formula extracted from the last tool call\. This approach is inspired by a body of work on autoformalization\([Murphy et al\., 2024](https://arxiv.org/html/2610.14402#bib.bib54);[Liu et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib53)\)\. Suppose the ground\-truth and proposed CNF formulas have aligned variables and are represented by

Ftruth=C1∧⋯∧Cn\\displaystyle F\_\{\\text\{truth\}\}=C\_\{1\}\\wedge\\cdots\\wedge C\_\{n\}Fpred=D1∧⋯∧Dm\\displaystyle F\_\{\\text\{pred\}\}=D\_\{1\}\\wedge\\cdots\\wedge D\_\{m\}We verify the equivalenceFtruth↔FpredF\_\{\\text\{truth\}\}\\leftrightarrow F\_\{\\text\{pred\}\}using Z3 to check whether

\(Fpred∧¬Ftruth\)∨\(¬Fpred∧Ftruth\)\(F\_\{\\text\{pred\}\}\\wedge\\neg F\_\{\\text\{truth\}\}\)\\vee\(\\neg F\_\{\\text\{pred\}\}\\wedge F\_\{\\text\{truth\}\}\)is unsatisfiable\. We further assignrequiv=1r\_\{\\text\{equiv\}\}=1if the formulas are equivalent\. The overall reward score is therefore

r=rformat\+rcorrect\+rtool\+requivr=r\_\{\\text\{format\}\}\+r\_\{\\text\{correct\}\}\+r\_\{\\text\{tool\}\}\+r\_\{\\text\{equiv\}\}

#### Training Objective\.

We leverage Decoupled Clip and Dynamic Sampling Policy Optimization \(DAPO\)\([Yu et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib43)\), a variant of Group Relative Policy Optimization \(GRPO\)\([Shao et al\., 2024](https://arxiv.org/html/2610.14402#bib.bib41)\), as our RL training algorithm\. Given an input promptxx, DAPO samples a group ofGGcompletions\{oi\}i=1G\\\{o\_\{i\}\\\}\_\{i=1\}^\{G\}from the old policyπθold\\pi\_\{\\theta\_\{\\text\{old\}\}\}, computes the rewardRiR\_\{i\}for each completion, and estimates the corresponding advantages:

A^i,t=Ri−mean​\(\{Rj\}j=1G\)std​\(\{Rj\}j=1G\)\\hat\{A\}\_\{i,t\}=\\frac\{R\_\{i\}\-\\text\{mean\}\(\\\{R\_\{j\}\\\}\_\{j=1\}^\{G\}\)\}\{\\text\{std\}\(\\\{R\_\{j\}\\\}\_\{j=1\}^\{G\}\)\}It then optimizesθ\\thetawith the following training objective:

𝒥DAPO\(θ\)=𝔼\[1G∑i=1G1\|oi\|∑t=1\|oi\|\(min\(ri,t\(θ\)A^i,t,\\displaystyle\\mathcal\{J\}\_\{\\text\{DAPO\}\}\(\\theta\)=\{\}\\mathbb\{E\}\\Biggl\[\\frac\{1\}\{G\}\\sum\_\{i=1\}^\{G\}\\frac\{1\}\{\\lvert o\_\{i\}\\rvert\}\{\}\\sum\_\{t=1\}^\{\\lvert o\_\{i\}\\rvert\}\\Bigl\(\\min\\Bigl\(r\_\{i,t\}\(\\theta\)\\,\\hat\{A\}\_\{i,t\},clip\(ri,t\(θ\),1−ϵlow,1\+ϵhigh\)A^i,t\)\)\]\\displaystyle\\text\{clip\}\\bigl\(r\_\{i,t\}\(\\theta\),\\,1\-\\epsilon\_\{\\text\{low\}\},1\+\\epsilon\_\{\\text\{high\}\}\\bigr\)\\,\\hat\{A\}\_\{i,t\}\\Bigr\)\\Bigr\)\\Biggr\]where the expectation is taken overx∼𝒟x\\sim\\mathcal\{D\}and\{oi\}i=1G∼πθold\(⋅∣x\)\\\{o\_\{i\}\\\}\_\{i=1\}^\{G\}\\sim\\pi\_\{\\theta\_\{\\text\{old\}\}\}\(\\cdot\\mid x\)\. Here,\|oi\|\|o\_\{i\}\|denotes the number of tokens inoio\_\{i\},ϵlow\\epsilon\_\{\\text\{low\}\}andϵhigh\\epsilon\_\{\\text\{high\}\}denote the lower and upper clipping thresholds, respectively, and the importance ratiori,tr\_\{i,t\}is defined as

ri,t=πθ​\(oi,t\|x,oi,<t\)πθold​\(oi,t\|x,oi,<t\)r\_\{i,t\}=\\frac\{\\pi\_\{\\theta\}\(o\_\{i,t\}\|x,o\_\{i,<t\}\)\}\{\\pi\_\{\\theta\_\{\\text\{old\}\}\}\(o\_\{i,t\}\|x,o\_\{i,<t\}\)\}Complete rollout examples with reward computation can be found in Appendices[E\.1](https://arxiv.org/html/2610.14402#A5.SS1)and[E\.2](https://arxiv.org/html/2610.14402#A5.SS2)\.

## 4Evaluation

In this section, we evaluate SAT\-RL across multiple models and datasets to examine its in\-domain performance and out\-of\-domain generalization\. In particular, we design our empirical evaluation to answer the following research questions:

![Refer to caption](https://arxiv.org/html/2610.14402v1/images/correctness_satrl_vs_baseline.png)

![Refer to caption](https://arxiv.org/html/2610.14402v1/images/entropy_satrl_vs_baseline.png)

Figure 2:Training trajectories on SAT\-Bench for ReTool and SAT\-RL \(mean±\\pmpopulation standard deviation across three runs\)\.Left: validation correctness\.Right: policy entropy\.1. RQ1\.In\-Domain Improvements\.Does SAT\-RL improve accuracy on in\-domain logical reasoning benchmarks?
2. RQ2\.Out\-of\-Domain Generalization\.Does training with SAT\-RL on logic puzzles generalize to out\-of\-domain logical or mathematical tasks?
3. RQ3\.Ablation Studies\.How do key components of SAT\-RL, including SFT with synthetic data, tool sampling, and logic\-equivalence checking, affect test accuracy and training behavior?

#### Hyperparameter Settings\.

We use verl v0\.8\.0 as our SFT and RL training framework\([Sheng et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib3)\)\. We use DAPO\([Yu et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib43)\)with a rollout group size ofG=8G=8as the RL training objective\. During training, the maximum input and output token limits are set to 4096 and 8192, respectively\. The detailed setup is provided in Appendix[B](https://arxiv.org/html/2610.14402#A2)\.

#### Model Setup\.

We evaluate cutting\-edge proprietary models, including OpenAI GPT\-5\.6 Luna\([Singh et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib14)\), Claude Sonnet 5, and Claude Haiku 4\.5\([Anthropic, 2026](https://arxiv.org/html/2610.14402#bib.bib15);[Anthropic, 2025](https://arxiv.org/html/2610.14402#bib.bib16)\), with the reasoning\-effort parameter set to “high\.” We train 4B\- and 9B\-parameter variants of the Qwen3\.5\([Team, 2026](https://arxiv.org/html/2610.14402#bib.bib13)\)model family\. We compare the SAT\-RL regime with the ReTool\([Feng et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib26)\)baseline regime, in which the model can interact with tools without being incentivized to use symbolic solvers, and the reward includes only format, correctness, and successful compilation of tools\. We train each model under each regime on the SAT\-Bench training split\([Wei et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib2)\)and evaluate in\-domain performance on its test split\. We use Enigmata\([Chen et al\., 2025](https://arxiv.org/html/2610.14402#bib.bib38)\)and AIME 2025 to evaluate out\-of\-domain generalization in logic and mathematics\. For each setup, we conduct three training runs\(N=3\)\(N=3\)in parallel with different random seeds to assess training stability\. We report test accuracy, with a correct response scoring 1\.0 and an incorrect response scoring 0\.0\.

### 4\.1RQ 1: In\-Domain Performance

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±\\pmstandard deviation\.We evaluate in\-domain test accuracy on SAT\-Bench and observe that SAT\-RL enables the Qwen3\.5\-9B model to outperform cutting\-edge proprietary models, as detailed in Table[4](https://arxiv.org/html/2610.14402#S4.T4)and Figure[2](https://arxiv.org/html/2610.14402#S4.F2)\. The base Qwen3\.5\-9B model performs poorly on the SAT\-Bench dataset and has difficulty following the`\`\`\`answer\`\`\``format, with fewer than 20% of its responses yielding parseable answers\. Its test accuracy reaches 70\.0% after SFT and 97\.2% after RL, surpassing Claude Sonnet 5 \(93\.0%\) and the ReTool\-trained Qwen3\.5\-9B model \(83\.5%\)\. A similar pattern appears for Qwen3\.5\-4B: SAT\-RL improves its accuracy from 19\.8% to 85\.4%, outperforming the larger ReTool\-trained Qwen3\.5\-9B model\. Overall, SAT\-RL yields consistent in\-domain accuracy improvements across model sizes\.

### 4\.2RQ 2: Out\-of\-Domain Generalization

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](https://arxiv.org/html/2610.14402#A1)\.We evaluate Qwen3\.5\-9B on the Enigmata benchmark across difficulty and category partitions after training on SAT\-Bench under ReTool and SAT\-RL\. For each regime, we select the final checkpoint with the highest SAT\-Bench accuracy across three runs \(Table[5](https://arxiv.org/html/2610.14402#S4.T5)\)\. SAT\-RL raises overall accuracy from 33\.9% to 59\.9%, outperforming Claude Haiku 4\.5 and the strongest flagship models in categories such as Crypto\. Across the easy, medium, and hard subsets, the gains are 19\.6%, 31\.6%, and 25\.9%, respectively\. SAT\-RL improves all seven categories, with the largest gains on Crypto and Logic, where accuracy reaches 100\.0% and 82\.8%, respectively\. These results demonstrate substantial transfer to tasks that emphasize constraint satisfaction and multi\-step deductive reasoning\.

On AIME 2025 \(30 problems\), SAT\-RL modestly improves Avg@8 test accuracy from 86\.7% \(208/240\) to 88\.3% \(212/240\); both the base and SAT\-RL\-trained Qwen3\.5\-9B models solve 28/30 problems\. Overall, under this configuration, SAT\-RL generalizes to out\-of\-domain logic tasks and provides limited but non\-negative gains in mathematical reasoning\.

### 4\.3RQ 3: Ablation Studies

We perform ablation studies to quantify the impact of \(i\) SFT, \(ii\) the logic\-equivalence rewardrequivr\_\{\\text\{equiv\}\}, and \(iii\) tool sampling, as shown in Table[6](https://arxiv.org/html/2610.14402#S4.T6)\. \(i\) Removing the SFT stage causes the largest degradation in SAT\-Bench accuracy, from 97\.2% to 54\.9%; the latter is comparable to random guessing when responses follow the required parseable answer format\. \(ii\) After removingrequivr\_\{\\text\{equiv\}\}from training, inspection of generated rollouts reveals reward\-hacking behavior, including degenerate tool calls such as “from z3 import \*\\nprint\('z3 imported '\)”, which superficially obtain thertoolr\_\{\\text\{tool\}\}reward\. This reduces the in\-domain accuracy to 91\.2%, with only 80\.6% of solver calls having formula encodings equivalent to the ground\-truth formulas\. \(iii\) Ablating tool sampling incurs a slight accuracy drop and causes a severe collapse in solver diversity: over 99% of tool calls are routed toz3, as illustrated in Figure[4](https://arxiv.org/html/2610.14402#S4.F4)\. It also reduces Enigmata accuracy to 52\.7%\. In contrast, enabling tool sampling yields a substantially more balanced distribution across symbolic solvers\. Together, these ablations demonstrate that logic\-equivalence checking, SFT, and tool sampling are all necessary for robust end\-to\-end performance in SAT\-RL\. Figure[3](https://arxiv.org/html/2610.14402#S4.F3)summarizes the corresponding logic\-equivalence trajectories\.

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\.![Refer to caption](https://arxiv.org/html/2610.14402v1/images/logic_equivalence_ablation.png)Figure 3:Logic\-equivalence trajectories on SAT\-Bench\. In the “w/o Logic Equivalence” ablation,requivr\_\{\\text\{equiv\}\}is computed but excluded from the training reward\.![Refer to caption](https://arxiv.org/html/2610.14402v1/images/solver_query_distribution.png)

![Refer to caption](https://arxiv.org/html/2610.14402v1/images/z3_vs_others_distribution.png)

Figure 4:Distribution of symbolic solver usage with tool sampling enabled \(left\) and disabled \(right\)\.

## 5Conclusion

We present SAT\-RL, an RL framework that integrates synthetic data and symbolic solver interaction into LLM training, enabling accurate logical reasoning and faithful solver use\. Experiments show that SAT\-RL improves in\-domain logical reasoning and generalizes to unseen out\-of\-domain benchmarks, outperforming base LLMs and ReTool baselines\.

## Limitations

Our current study focuses on logical reasoning and a fixed set of widely used symbolic solvers, which limits the scope of this work\. Broader program synthesis and open\-ended natural\-language reasoning remain to be explored\. Future work will extend the framework to richer tool\-using agent systems and more general coding and mathematical reasoning domains\.

## References

- Anthropic \(2025\)AnthropicClaude Haiku 4\.5 System Card\.System CardAnthropic\.External Links:[Link](https://www-cdn.anthropic.com/7aad69bf12627d42234e01ee7c36305dc2f6a970.pdf)Cited by:[§4](https://arxiv.org/html/2610.14402#S4.SS0.SSS0.Px2.p1.1)\.
- Anthropic \(2026\)AnthropicClaude Sonnet 5 System Card\.System CardAnthropic\.Note:Published June 30, 2026External Links:[Link](https://www.anthropic.com/claude-sonnet-5-system-card)Cited by:[§4](https://arxiv.org/html/2610.14402#S4.SS0.SSS0.Px2.p1.1)\.
- Barbosaet al\.\(2022\)H\. Barbosa, C\. Barrett, M\. Brain, G\. Kremer, H\. Lachnitt, M\. Mann, A\. Mohamed, M\. Mohamed, A\. Niemetz, A\. Nötzli,et al\.Cvc5: a versatile and industrial\-strength smt solver\.InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems,pp\. 415–442\.Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p2.1)\.
- Bytedance\-Seed\-Foundation\-Code\-Teamet al\.\(2025\)Bytedance\-Seed\-Foundation\-Code\-Team, :, Y\. Cheng, J\. Chen, J\. Chen, L\. Chen, L\. Chen, W\. Chen, Z\. Chen, S\. Geng, A\. Li, B\. Li, B\. Li, L\. Li, B\. Liu, J\. Liu, K\. Liu, Q\. Liu, S\. Liu, S\. Liu, T\. Liu, T\. Liu, Y\. Liu, R\. Long, J\. Mai, G\. Ning, Z\. Y\. Peng, K\. Shen, J\. Su, J\. Su, T\. Sun, Y\. Sun, Y\. Tao, G\. Wang, S\. Wang, X\. Wang, Y\. Wang, Z\. Wang, J\. Xia, L\. Xiang, X\. Xiao, Y\. Xiao, C\. Xi, S\. Xin, J\. Xu, S\. Xu, H\. Yang, J\. Yang, Y\. Yang, J\. Yuan, J\. Zhang, Y\. Zhang, Y\. Zhang, S\. Zheng, H\. Zhu, and M\. ZhuFullStack bench: evaluating llms as full stack coders\.External Links:2412\.00535,[Link](https://arxiv.org/abs/2412.00535)Cited by:[§3](https://arxiv.org/html/2610.14402#S3.p1.1)\.
- Chenet al\.\(2025\)J\. Chen, Q\. He, S\. Yuan, A\. Chen, Z\. Cai, W\. Dai, H\. Yu, J\. Chen, X\. Li, Q\. Yu,et al\.Enigmata: scaling logical reasoning in large language models with synthetic verifiable puzzles\.InThe Thirty\-ninth Annual Conference on Neural Information Processing Systems,Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p1.1),[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1),[§3\.2](https://arxiv.org/html/2610.14402#S3.SS2.SSS0.Px3.p1.1),[§3\.2](https://arxiv.org/html/2610.14402#S3.SS2.p1.1),[Table 1](https://arxiv.org/html/2610.14402#S3.T1.2.1.5.1),[§4](https://arxiv.org/html/2610.14402#S4.SS0.SSS0.Px2.p1.1)\.
- Chenet al\.\(2024\)Z\. Chen, Y\. Deng, H\. Yuan, K\. Ji, and Q\. GuSelf\-play fine\-tuning converts weak language models to strong language models\.arXiv preprint arXiv:2401\.01335\.Cited by:[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p2.1)\.
- Clarket al\.\(2020\)P\. Clark, O\. Tafjord, and K\. RichardsonTransformers as soft reasoners over language\.InProceedings of the Twenty\-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020,C\. Bessiere \(Ed\.\),pp\. 3882–3890\.External Links:[Link](https://doi.org/10.24963/ijcai.2020/537),[Document](https://dx.doi.org/10.24963/IJCAI.2020/537)Cited by:[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1)\.
- de Moura and Bjørner \(2008\)L\. de Moura and N\. BjørnerZ3: an efficient smt solver\.InTACAS,Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p2.1),[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p1.1),[§3\.1](https://arxiv.org/html/2610.14402#S3.SS1.SSS0.Px1.p2.1)\.
- Fanet al\.\(2024\)L\. Fan, W\. Hua, L\. Li, H\. Ling, and Y\. ZhangNPHardEval: dynamic benchmark on reasoning ability of large language models via complexity classes\.InProceedings of the 62nd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),L\. Ku, A\. Martins, and V\. Srikumar \(Eds\.\),Bangkok, Thailand,pp\. 4092–4114\.External Links:[Link](https://aclanthology.org/2024.acl-long.225/),[Document](https://dx.doi.org/10.18653/v1/2024.acl-long.225)Cited by:[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1)\.
- Fenget al\.\(2025\)J\. Feng, S\. Huang, X\. Qu, G\. Zhang, Y\. Qin, B\. Zhong, C\. Jiang, J\. Chi, and W\. ZhongRetool: reinforcement learning for strategic tool use in llms\.arXiv preprint arXiv:2504\.11536\.Cited by:[§3\.4](https://arxiv.org/html/2610.14402#S3.SS4.SSS0.Px1.p1.1),[§4](https://arxiv.org/html/2610.14402#S4.SS0.SSS0.Px2.p1.1)\.
- Guoet al\.\(2025\)D\. Guo, D\. Yang, H\. Zhang, J\. Song, R\. Zhang, R\. Xu, Q\. Zhu, S\. Ma, P\. Wang, X\. Bi,et al\.Deepseek\-r1: incentivizing reasoning capability in llms via reinforcement learning\.arXiv preprint arXiv:2501\.12948\.Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p1.1)\.
- Hanet al\.\(2024a\)S\. Han, H\. Schoelkopf, Y\. Zhao, Z\. Qi, M\. Riddell, W\. Zhou, J\. Coady, D\. Peng, Y\. Qiao, L\. Benson, L\. Sun, A\. Wardle\-Solano, H\. Szabó, E\. Zubova, M\. Burtell, J\. Fan, Y\. Liu, B\. Wong, M\. Sailor, A\. Ni, L\. Nan, J\. Kasai, T\. Yu, R\. Zhang, A\. R\. Fabbri, W\. Kryscinski, S\. Yavuz, Y\. Liu, X\. V\. Lin, S\. Joty, Y\. Zhou, C\. Xiong, R\. Ying, A\. Cohan, and D\. RadevFOLIO: natural language reasoning with first\-order logic\.InProceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, EMNLP 2024, Miami, FL, USA, November 12\-16, 2024,Y\. Al\-Onaizan, M\. Bansal, and Y\. Chen \(Eds\.\),pp\. 22017–22031\.External Links:[Link](https://aclanthology.org/2024.emnlp-main.1229)Cited by:[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1)\.
- Hanet al\.\(2024b\)S\. Han, A\. Yu, R\. Shen, Z\. Qi, M\. Riddell, W\. Zhou, Y\. Qiao, Y\. Zhao, S\. Yavuz, Y\. Liu, S\. Joty, Y\. Zhou, C\. Xiong, D\. Radev, R\. Ying, and A\. CohanP\-FOLIO: evaluating and improving logical reasoning with abundant human\-written reasoning chains\.InFindings of the Association for Computational Linguistics: EMNLP 2024, Miami, Florida, USA, November 12\-16, 2024,Y\. Al\-Onaizan, M\. Bansal, and Y\. Chen \(Eds\.\),pp\. 16553–16565\.External Links:[Link](https://aclanthology.org/2024.findings-emnlp.966)Cited by:[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1)\.
- Haoet al\.\(2025\)Y\. Hao, L\. Dong, X\. Wu, S\. Huang, Z\. Chi, and F\. WeiOn\-policy rl with optimal reward baseline\.arXiv preprint arXiv:2505\.23585\.Cited by:[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p2.1)\.
- Hu \(2025\)J\. HuReinforce\+\+: a simple and efficient approach for aligning large language models\.arXiv preprint arXiv:2501\.03262\.Cited by:[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p2.1)\.
- Ignatievet al\.\(2018\)A\. Ignatiev, A\. Morgado, and J\. Marques\-SilvaPySAT: a python toolkit for prototyping with sat oracles\.InInternational Conference on Theory and Applications of Satisfiability Testing,pp\. 428–437\.Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p2.1),[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p1.1)\.
- Karp \(2009\)R\. M\. KarpReducibility among combinatorial problems\.In50 Years of Integer Programming 1958\-2008: from the Early Years to the State\-of\-the\-Art,pp\. 219–241\.Cited by:[§3\.2](https://arxiv.org/html/2610.14402#S3.SS2.SSS0.Px1.p1.1)\.
- Kazemiet al\.\(2023\)M\. Kazemi, Q\. Yuan, D\. Bhatia, N\. Kim, X\. Xu, V\. Imbrasaite, and D\. RamachandranBoardgameQA: A dataset for natural language reasoning with contradictory information\.InAdvances in Neural Information Processing Systems 36: Annual Conference on Neural Information Processing Systems 2023, NeurIPS 2023, New Orleans, LA, USA, December 10 \- 16, 2023,A\. Oh, T\. Naumann, A\. Globerson, K\. Saenko, M\. Hardt, and S\. Levine \(Eds\.\),External Links:[Link](http://papers.nips.cc/paper/_files/paper/2023/hash/7adce80e86aa841490e6307109094de5-Abstract-Datasets/_and/_Benchmarks.html)Cited by:[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1)\.
- Liet al\.\(2026\)L\. Li, Z\. Zhou, J\. HAO, J\. K\. Liu, Y\. Miao, W\. Pang, X\. Tan, W\. Chu, Z\. Wang, S\. Pan, C\. Qu, and Y\. QiThe choice of divergence: a neglected key to mitigating diversity collapse in reinforcement learning with verifiable reward\.InThe Fourteenth International Conference on Learning Representations,External Links:[Link](https://openreview.net/forum?id=xPEsxcO7F7)Cited by:[§3\.4](https://arxiv.org/html/2610.14402#S3.SS4.SSS0.Px2.p2.1)\.
- Lianget al\.\(2025\)J\. Liang, S\. Wan, X\. Wu, Y\. Li, Q\. Chen, D\. Tang, S\. Wang, and Z\. WeiHardcoreLogic: challenging large reasoning models with long\-tail logic puzzle games\.arXiv preprint arXiv:2510\.12563\.Cited by:[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1)\.
- Linet al\.\(2025\)B\. Y\. Lin, R\. Le Bras, K\. Richardson, A\. Sabharwal, R\. Poovendran, P\. Clark, and Y\. ChoiZebraLogic: on the scaling limits of llms for logical reasoning\.InInternational Conference on Machine Learning,pp\. 37889–37905\.Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p1.1),[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1),[Table 1](https://arxiv.org/html/2610.14402#S3.T1.2.1.3.1)\.
- Liuet al\.\(2023\)H\. Liu, J\. Liu, L\. Cui, Z\. Teng, N\. Duan, M\. Zhou, and Y\. ZhangLogiQA 2\.0 \- an improved dataset for logical reasoning in natural language understanding\.IEEE ACM Trans\. Audio Speech Lang\. Process\.31,pp\. 2947–2962\.External Links:[Link](https://doi.org/10.1109/TASLP.2023.3293046),[Document](https://dx.doi.org/10.1109/TASLP.2023.3293046)Cited by:[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1)\.
- Liuet al\.\(2020\)J\. Liu, L\. Cui, H\. Liu, D\. Huang, Y\. Wang, and Y\. ZhangLogiQA: A challenge dataset for machine reading comprehension with logical reasoning\.InProceedings of the Twenty\-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020,C\. Bessiere \(Ed\.\),pp\. 3622–3628\.External Links:[Link](https://doi.org/10.24963/ijcai.2020/501),[Document](https://dx.doi.org/10.24963/IJCAI.2020/501)Cited by:[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1)\.
- Liuet al\.\(2025\)Q\. Liu, X\. Zheng, X\. Lu, Q\. Cao, and J\. YanRethinking and improving autoformalization: towards a faithful metric and a dependency retrieval\-based approach\.InThe Thirteenth International Conference on Learning Representations,Cited by:[§3\.4](https://arxiv.org/html/2610.14402#S3.SS4.SSS0.Px2.p3.1)\.
- Mittalet al\.\(2024\)C\. Mittal, K\. Kartik, P\. Singla,et al\.FCoReBench: can large language models solve challenging first\-order combinatorial reasoning problems?\.arXiv preprint arXiv:2402\.02611\.Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p2.1),[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p1.1),[Table 1](https://arxiv.org/html/2610.14402#S3.T1.2.1.4.1)\.
- Murphyet al\.\(2024\)L\. Murphy, K\. Yang, J\. Sun, Z\. Li, A\. Anandkumar, and X\. SiAutoformalizing Euclidean Geometry\.InProceedings of the International Conference on Machine Learning,Cited by:[§3\.4](https://arxiv.org/html/2610.14402#S3.SS4.SSS0.Px2.p3.1)\.
- Nethercoteet al\.\(2007\)N\. Nethercote, P\. J\. Stuckey, R\. Becket, S\. Brand, G\. J\. Duck, and G\. TackMiniZinc: towards a standard cp modelling language\.InInternational conference on principles and practice of constraint programming,pp\. 529–543\.Cited by:[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p1.1)\.
- Panet al\.\(2023\)L\. Pan, A\. Albalak, X\. Wang, and W\. Y\. WangLogic\-lm: empowering large language models with symbolic solvers for faithful logical reasoning\.External Links:2305\.12295,[Link](https://arxiv.org/abs/2305.12295)Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p2.1)\.
- Parmaret al\.\(2024\)M\. Parmar, N\. Patel, N\. Varshney, M\. Nakamura, M\. Luo, S\. Mashetty, A\. Mitra, and C\. BaralLogicBench: towards systematic evaluation of logical reasoning ability of large language models\.arXiv\.org\.External Links:[Link](https://arxiv.org/abs/2404.15522)Cited by:[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1)\.
- Patelet al\.\(2024\)N\. Patel, M\. Kulkarni, M\. Parmar, A\. Budhiraja, M\. Nakamura, N\. Varshney, and C\. BaralMulti\-logieval: towards evaluating multi\-step logical reasoning ability of large language models\.arXiv\.org\.External Links:[Link](https://arxiv.org/abs/2406.17169)Cited by:[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1)\.
- Qiet al\.\(2025\)C\. Qi, R\. Ma, B\. Li, H\. Du, B\. Hui, J\. Wu, Y\. Laili, and C\. HeLarge language models meet symbolic provers for logical reasoning evaluation\.arXiv preprint arXiv:2502\.06563\.Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p1.1),[§3\.1](https://arxiv.org/html/2610.14402#S3.SS1.SSS0.Px2.p1.1)\.
- Rafailovet al\.\(2023\)R\. Rafailov, A\. Sharma, E\. Mitchell, C\. D\. Manning, S\. Ermon, and C\. FinnDirect preference optimization: your language model is secretly a reward model\.Advances in Neural Information Processing Systems36,pp\. 53728–53741\.Cited by:[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p2.1)\.
- Renet al\.\(2025\)Z\. Ren, Z\. Shao, J\. Song, H\. Xin, H\. Wang, W\. Zhao, L\. Zhang, Z\. Fu, Q\. Zhu, D\. Yang,et al\.Deepseek\-prover\-v2: advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition\.arXiv preprint arXiv:2504\.21801\.Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p1.1)\.
- Riazanov and Voronkov \(2001\)A\. Riazanov and A\. VoronkovVampire 1\.1\.InInternational Joint Conference on Automated Reasoning,pp\. 376–380\.Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p2.1)\.
- Schulmanet al\.\(2017\)J\. Schulman, F\. Wolski, P\. Dhariwal, A\. Radford, and O\. KlimovProximal policy optimization algorithms\.External Links:1707\.06347,[Link](https://arxiv.org/abs/1707.06347)Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p1.1),[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p2.1)\.
- Shaoet al\.\(2024\)Z\. Shao, P\. Wang, Q\. Zhu, R\. Xu, J\. Song, X\. Bi, H\. Zhang, M\. Zhang, Y\. Li, Y\. Wu,et al\.Deepseekmath: pushing the limits of mathematical reasoning in open language models\.arXiv preprint arXiv:2402\.03300\.Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p1.1),[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p2.1),[§3\.4](https://arxiv.org/html/2610.14402#S3.SS4.SSS0.Px3.p1.1),[§3](https://arxiv.org/html/2610.14402#S3.p1.1)\.
- Shenget al\.\(2025\)G\. Sheng, C\. Zhang, Z\. Ye, X\. Wu, W\. Zhang, R\. Zhang, Y\. Peng, H\. Lin, and C\. WuHybridFlow: a flexible and efficient rlhf framework\.InProceedings of the Twentieth European Conference on Computer Systems,EuroSys ’25,pp\. 1279–1297\.External Links:[Link](http://dx.doi.org/10.1145/3689031.3696075),[Document](https://dx.doi.org/10.1145/3689031.3696075)Cited by:[§3\.4](https://arxiv.org/html/2610.14402#S3.SS4.SSS0.Px1.p2.1),[§4](https://arxiv.org/html/2610.14402#S4.SS0.SSS0.Px1.p1.1)\.
- Singhet al\.\(2025\)A\. Singh, A\. Fry, A\. Perelman, A\. Tart, A\. Ganesh, A\. El\-Kishky, A\. McLaughlin, A\. Low, A\. Ostrow, A\. Ananthram,et al\.Openai gpt\-5 system card\.arXiv preprint arXiv:2601\.03267\.Cited by:[§4](https://arxiv.org/html/2610.14402#S4.SS0.SSS0.Px2.p1.1)\.
- Sinhaet al\.\(2019\)K\. Sinha, S\. Sodhani, J\. Dong, J\. Pineau, and W\. L\. HamiltonCLUTRR: a diagnostic benchmark for inductive reasoning from text\.InProceedings of the 2019 Conference on Empirical Methods in Natural Language Processing and the 9th International Joint Conference on Natural Language Processing \(EMNLP\-IJCNLP\),K\. Inui, J\. Jiang, V\. Ng, and X\. Wan \(Eds\.\),Hong Kong, China,pp\. 4506–4515\.External Links:[Link](https://aclanthology.org/D19-1458/),[Document](https://dx.doi.org/10.18653/v1/D19-1458)Cited by:[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1)\.
- Szeider \(2024\)S\. SzeiderMCP\-solver: integrating language models with constraint programming systems\.arXiv preprint arXiv:2501\.00539\.Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p2.1),[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p1.1)\.
- Team \(2026\)Q\. TeamQwen3\. 5\-omni technical report\.arXiv preprint arXiv:2604\.15804\.Cited by:[§4](https://arxiv.org/html/2610.14402#S4.SS0.SSS0.Px2.p1.1)\.
- Tianet al\.\(2021\)J\. Tian, Y\. Li, W\. Chen, L\. Xiao, H\. He, and Y\. JinDiagnosing the first\-order logical reasoning ability through logicnli\.InProceedings of the 2021 Conference on Empirical Methods in Natural Language Processing, EMNLP 2021, Virtual Event / Punta Cana, Dominican Republic, 7\-11 November, 2021,M\. Moens, X\. Huang, L\. Specia, and S\. W\. Yih \(Eds\.\),pp\. 3738–3747\.External Links:[Link](https://doi.org/10.18653/v1/2021.emnlp-main.303),[Document](https://dx.doi.org/10.18653/V1/2021.EMNLP-MAIN.303)Cited by:[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1)\.
- Wanget al\.\(2022\)X\. Wang, J\. Wei, D\. Schuurmans, Q\. Le, E\. Chi, S\. Narang, A\. Chowdhery, and D\. ZhouSelf\-consistency improves chain of thought reasoning in language models\.arXiv preprint arXiv:2203\.11171\.Cited by:[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p1.1)\.
- Weiet al\.\(2025\)A\. Wei, Y\. Wu, Y\. Wan, T\. Suresh, H\. Tan, Z\. Zhou, S\. Koyejo, K\. Wang, and A\. AikenSatbench: benchmarking llms’ logical reasoning via automated puzzle generation from sat formulas\.InProceedings of the 2025 Conference on Empirical Methods in Natural Language Processing,pp\. 33820–33837\.Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p1.1),[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1),[§3\.2](https://arxiv.org/html/2610.14402#S3.SS2.SSS0.Px2.p1.1),[§3\.2](https://arxiv.org/html/2610.14402#S3.SS2.p1.1),[§3\.4](https://arxiv.org/html/2610.14402#S3.SS4.SSS0.Px1.p2.1),[Table 1](https://arxiv.org/html/2610.14402#S3.T1.2.1.2.1),[§4](https://arxiv.org/html/2610.14402#S4.SS0.SSS0.Px2.p1.1)\.
- Weiet al\.\(2022\)J\. Wei, X\. Wang, D\. Schuurmans, M\. Bosma, F\. Xia, E\. Chi, Q\. V\. Le, D\. Zhou,et al\.Chain\-of\-thought prompting elicits reasoning in large language models\.Advances in neural information processing systems35,pp\. 24824–24837\.Cited by:[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p1.1)\.
- Wuet al\.\(2024\)Y\. Wu, Z\. Sun, H\. Yuan, K\. Ji, Y\. Yang, and Q\. GuSelf\-play preference optimization for language model alignment\.arXiv preprint arXiv:2405\.00675\.Cited by:[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p2.1)\.
- Yaoet al\.\(2023\)S\. Yao, D\. Yu, J\. Zhao, I\. Shafran, T\. Griffiths, Y\. Cao, and K\. NarasimhanTree of thoughts: deliberate problem solving with large language models\.Advances in neural information processing systems36,pp\. 11809–11822\.Cited by:[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p1.1)\.
- Yeet al\.\(2023\)X\. Ye, Q\. Chen, I\. Dillig, and G\. DurrettSatlm: satisfiability\-aided language models using declarative prompting\.Advances in Neural Information Processing Systems36,pp\. 45548–45580\.Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p2.1),[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p1.1),[§3\.1](https://arxiv.org/html/2610.14402#S3.SS1.SSS0.Px2.p1.1)\.
- Yuet al\.\(2025\)Q\. Yu, Z\. Zhang, R\. Zhu, Y\. Yuan, X\. Zuo, Y\. Yue, W\. Dai, T\. Fan, G\. Liu, L\. Liu,et al\.Dapo: an open\-source llm reinforcement learning system at scale\.arXiv preprint arXiv:2503\.14476\.Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p1.1),[§2\.2](https://arxiv.org/html/2610.14402#S2.SS2.p2.1),[§3\.4](https://arxiv.org/html/2610.14402#S3.SS4.SSS0.Px3.p1.1),[§3\.4](https://arxiv.org/html/2610.14402#S3.SS4.p1.1),[§3](https://arxiv.org/html/2610.14402#S3.p1.1),[§4](https://arxiv.org/html/2610.14402#S4.SS0.SSS0.Px1.p1.1)\.
- Yuet al\.\(2020\)W\. Yu, Z\. Jiang, Y\. Dong, and J\. FengReClor: A reading comprehension dataset requiring logical reasoning\.In8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, April 26\-30, 2020,External Links:[Link](https://openreview.net/forum?id=HJgJtT4tvB)Cited by:[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1)\.
- Zhanget al\.\(2025\)T\. Zhang, C\. Zhu, Y\. Shen, W\. Luo, Y\. Zhang, H\. Liang, F\. Yang, M\. Lin, Y\. Qiao, W\. Chen,et al\.CFBench: a comprehensive constraints\-following benchmark for LLMs\.InProceedings of the 63rd Annual Meeting of the Association for Computational Linguistics \(Volume 1: Long Papers\),pp\. 32926–32944\.Cited by:[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1)\.
- Zhonget al\.\(2024\)W\. Zhong, R\. Cui, Y\. Guo, Y\. Liang, S\. Lu, Y\. Wang, A\. Saied, W\. Chen, and N\. DuanAgieval: a human\-centric benchmark for evaluating foundation models\.InFindings of the Association for Computational Linguistics: NAACL 2024,pp\. 2299–2314\.Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p1.1)\.
- Zhonget al\.\(2021\)W\. Zhong, S\. Wang, D\. Tang, Z\. Xu, D\. Guo, J\. Wang, J\. Yin, M\. Zhou, and N\. DuanAr\-lsat: investigating analytical reasoning of text\.arXiv preprint arXiv:2104\.06598\.Cited by:[§1](https://arxiv.org/html/2610.14402#S1.p1.1)\.
- Zhuet al\.\(2025\)Q\. Zhu, F\. Huang, R\. Peng, K\. Lu, B\. Yu, Q\. Cheng, X\. Qiu, X\. Huang, and J\. LinAutoLogi: automated generation of logic puzzles for evaluating reasoning abilities of large language models\.CoRRabs/2502\.16906\.External Links:[Link](https://doi.org/10.48550/arXiv.2502.16906),[Document](https://dx.doi.org/10.48550/ARXIV.2502.16906),2502\.16906Cited by:[§2\.1](https://arxiv.org/html/2610.14402#S2.SS1.p1.1)\.

## Appendix AComponents of the Enigmata Test Set

We report statistics for the Enigmata test set \(Section[4\.2](https://arxiv.org/html/2610.14402#S4.SS2)\), grouped by difficulty, puzzle category, and task, in Table[7](https://arxiv.org/html/2610.14402#A1.T7)\.

Data TypeNumber of InstancesAll instances1901DifficultyEasy560Medium642Hard699Puzzle categoryArithmetic120countdown60game2460Crypto120crypto\_KKA60crypto\_KPA60Graph220hamiltonian\_cycle60hamiltonian\_path60maze60natural\_language\_navigation40Grid539binario60campsite60magic\_square60skyscraper60star\_battle60sudoku60sudoku260sum\_skyscraper60full\_crosswords40symbolic\_hard19Logic180FOLIO60knights\_and\_knaves60zebra\_logic60Search320kakurasu60minesweeper60slant60hitori40light\_up40tic\_tac\_toe40checkmate\_in\_one20Sequential402car\_painting60eight\_puzzle60fifteen\_puzzle60nine\_puzzle60sixteen\_puzzle60stack\_permutation60twiddle22big\_bench\_symbolic20Table 7:Number of instances in the Enigmata test set, grouped by difficulty, puzzle category, and puzzle name\.
## Appendix BHyperparameter Settings

The SFT and RL training configurations are shown in Table[8](https://arxiv.org/html/2610.14402#A2.T8)\. Training Qwen3\.5\-9B on SAT\-Bench require around 24 hours\.

Table 8:Training configuration\.### B\.1Description of Synthetic Puzzles

#### Clique \(K\-Clique\)\.

Given an undirected graph, the task is to select a set of vertices that forms a clique of a target size\. Hyperparameters: number of verticesNN, clique sizeKK, and edge listedges⊆\{\(u,v\):0≤u<v<N\}\\texttt\{edges\}\\subseteq\\\{\(u,v\):0\\leq u<v<N\\\}\.

#### Feedback Node Set \(Directed Feedback Vertex Set\)\.

Given a directed graph, the task is to remove a small set of vertices so that the remaining graph becomes acyclic\. Hyperparameters: number of verticesNN, removal budgetKK, and directed edge listedges⊆V×V\\texttt\{edges\}\\subseteq V\\times V\.

#### GraphKK\-Coloring\.

Given an undirected graph, the task is to assign one ofKKcolors to each vertex such that adjacent vertices have different colors\. Hyperparameters: number of verticesNN, number of colorsKK, and edge listedges\.

#### Max Cut \(Threshold Formulation\)\.

Given an undirected graph, the task is to find a binary partition of vertices whose cut size meets a target threshold\. Hyperparameters: number of verticesNN, thresholdTT\(required number of crossing edges\), and edge listedges\.

#### Partition\.

Given positive integers, the task is to split them into two groups with equal sums \(equivalently, find a subset summing to half the total\)\. Hyperparameters: number of itemsNNand the integer arrayarr\(with total sum determining the implied target\)\.

#### Subset Sum\.

Given positive integers and a target, the task is to choose a subset whose sum equals the target exactly\. Hyperparameters: number of itemsNN, target sumTT, and integer arrayarr\.

#### Traveling Salesman Problem \(Threshold Variant\)\.

Given a complete weighted graph, the task is to find a Hamiltonian tour whose total cost satisfies a threshold constraint\. Hyperparameters: number of nodesNN, tour\-cost thresholdTT, and weight matrixW∈ℤN×N\\texttt\{W\}\\in\\mathbb\{Z\}^\{N\\times N\}\.

#### Set Covering\.

Given a universe and a family of subsets, the task is to select a small number of sets whose union covers the entire universe\. Hyperparameters: universe sizeUU, number of setsMM, budget parameterKK, and set familysets=\[S0,…,SM−1\]\\texttt\{sets\}=\[S\_\{0\},\\dots,S\_\{M\-1\}\]withSi⊆\{0,…,U−1\}S\_\{i\}\\subseteq\\\{0,\\dots,U\-1\\\}\.

#### Set Packing\.

Given a universe and a family of subsets, the task is to select a prescribed number of pairwise disjoint sets\. Hyperparameters: universe sizeUU, number of setsMM, packing sizeKK, and set familysets=\[S0,…,SM−1\]\\texttt\{sets\}=\[S\_\{0\},\\dots,S\_\{M\-1\}\]\.

#### NFA Path Problems\.

Given an NFA \(as an explicit transition relation\), the task is to find an accepted path of a fixed length from a start state to an accepting state\. Hyperparameters: number of statesSS, alphabet sizeAA, path lengthLL, start statestart, accepting setaccepts, and transition listtransitions=\[\(s,a,t\)\]\\texttt\{transitions\}=\[\(s,a,t\)\]\.

#### Binary Neural Network \(BNN\) Robustness\.

Given a threshold\-gate BNN and a seed input, the task is to find an input within a Hamming ball that flips the network output\. Hyperparameters: input dimensionn\_in, network structurelayers\(neurons with thresholdkkand signed literals\), and property dictpropcontainingseed, radiusε=eps\\varepsilon=\\texttt\{eps\}, andy\_seed\.

#### Partial N\-Queens\.

Given a partially filledN×NN\\times Nchessboard, the task is to place one queen in each row while respecting the pre\-placed queens and nonattacking constraints\. Hyperparameters: board sizeNNand fixed queen positionspre=\[\(r​o​w,c​o​l\)\]\\texttt\{pre\}=\[\(row,col\)\]\.

#### Generalized Sudoku\.

Given anN×NN\\times NSudoku grid \(withN=n2N=n^\{2\}\), the task is to fill in the blanks while satisfying row, column, and sub\-block uniqueness constraints\. Hyperparameters: grid sizeNNand the partially filled gridgiven\_grid\(where00or\.denotes a blank\)\.

#### Magic Square\.

Given anN×NN\\times Ngrid, the task is to assign integers so that every row, every column, and both main diagonals sum to the same magic constant\. Hyperparameters: orderNN, value domain \(typically\{1,…,N2\}\\\{1,\\dots,N^\{2\}\\\}with an all\-different constraint\), and an optional set of pre\-filled cellsgivens=\[\(r,c,v\)\]\\texttt\{givens\}=\[\(r,c,v\)\]\.

#### Latin Square\.

Given anN×NN\\times Ngrid over symbols\{1,…,N\}\\\{1,\\dots,N\\\}, the task is to fill the grid so that each symbol appears exactly once in every row and every column\. Hyperparameters: orderNNand an optional partially filled gridgiven\_grid∈\(\{0,1,…,N\}\)N×N\\texttt\{given\\\_grid\}\\in\(\\\{0,1,\\dots,N\\\}\)^\{N\\times N\}, where00denotes blanks\.

#### Futoshiki\.

Given anN×NN\\times NLatin\-square\-style grid together with inequality clues between neighboring cells, the task is to fill the grid with symbols\{1,…,N\}\\\{1,\\dots,N\\\}satisfying both row/column uniqueness and all inequality constraints\. Hyperparameters: orderNN, an optional partially filled gridgiven\_grid, and a set of directed inequality edges between adjacent cellsineq=\[\(\(r1,c1\),\(r2,c2\)\)\]\\texttt\{ineq\}=\[\(\(r\_\{1\},c\_\{1\}\),\(r\_\{2\},c\_\{2\}\)\)\], where each edge denotes\(r1,c1\)<\(r2,c2\)\(r\_\{1\},c\_\{1\}\)<\(r\_\{2\},c\_\{2\}\)\.

## Appendix CPrompt Templates

Below, we present the LLM template used for SAT\-RL training on SAT\-Bench\.

Input[⬇](data:text/plain;base64,U29sdmUgdGhlIHByb2JsZW0gc3RlcCBieSBzdGVwIGFuZCBwdXQgeW91ciBmaW5hbCBhbnN3ZXIgaW4gdGhlIGZvcm1hdCBgYGA8YW5zd2VyPmBgYC4KCklmIHRoZSBldmlkZW5jZSBpcyBnZW51aW5lbHkgaW5zdWZmaWNpZW50IGFmdGVyIHVzaW5nIHRoZSB0b29sLCB5b3UgbWF5IG91dHB1dCBgYGBpZGtgYGAuCgpGb3IgdGhpcyBpbnN0YW5jZSwgeW91IG11c3QgaW1wb3J0IGFuZCB1c2UgdGhlIGB7e3NhbXBsZWRfdG9vbH19YCBhcyB0aGUgc29sdmVyL3Rvb2wgY2FsbC4KClZhcmlhYmxlIE1hcHBpbmc6Cnt7dmFyaWFibGVfbWFwcGluZ319CgpQcm9ibGVtIFN0YXRlbWVudDoKe3twcm9ibGVtfX0K)Solvetheproblemstepbystepandputyourfinalanswerintheformat‘‘‘<answer\>‘‘‘\.Iftheevidenceisgenuinelyinsufficientafterusingthetool,youmayoutput‘‘‘idk‘‘‘\.Forthisinstance,youmustimportandusethe‘\{\{sampled\_tool\}\}‘asthesolver/toolcall\.VariableMapping:\{\{variable\_mapping\}\}ProblemStatement:\{\{problem\}\}

Below, we present the LLM template used for training in the other settings\. This template is also used for all evaluations\.

Input[⬇](data:text/plain;base64,U29sdmUgdGhlIHByb2JsZW0gc3RlcCBieSBzdGVwIGFuZCBwdXQgeW91ciBmaW5hbCBhbnN3ZXIgaW4gdGhlIGZvcm1hdCBgYGA8YW5zd2VyPmBgYC4KClByb2JsZW0gU3RhdGVtZW50Ogp7e3Byb2JsZW19fQo=)Solvetheproblemstepbystepandputyourfinalanswerintheformat‘‘‘<answer\>‘‘‘\.ProblemStatement:\{\{problem\}\}

## Appendix DOR\-Tools Example

Below is an example OR\-Tools program\.

fromortools\.sat\.pythonimportcp\_model

classCounter\(cp\_model\.CpSolverSolutionCallback\):

def\_\_init\_\_\(self,x,y,want\_print=True\):

super\(\)\.\_\_init\_\_\(\)

self\.\_x,self\.\_y=x,y

self\.count=0

self\.want\_print=want\_print

defon\_solution\_callback\(self\):

self\.count\+=1

ifself\.want\_print:

print\(f"Solution\{self\.count\}:x=\{self\.Value\(self\.\_x\)\},y=\{self\.Value\(self\.\_y\)\}"\)

model=cp\_model\.CpModel\(\)

\#Variables\(nonnegativeintegers\)

x=model\.NewIntVar\(0,50,"x"\)\#upperboundscanbeloose

y=model\.NewIntVar\(0,50,"y"\)

\#Constraint:4x\+6y=50

model\.Add\(4\*x\+6\*y==50\)

solver=cp\_model\.CpSolver\(\)

cb=Counter\(x,y,want\_print=True\)

solver\.SearchForAllSolutions\(model,cb\)

print\("Numberofsolutions:",cb\.count\)

## Appendix ESolved Examples

Below, we show examples solved during training and evaluation\.

### E\.1Solved SAT\-Bench Example

Below, we show an example SAT\-Bench instance successfully solved by Qwen3\.5\-9B during SAT\-RL training\. This instance requires the use of the Z3 solver\. We omit the repeated system prompt template and directly show the instance below\.

Input\.The input instance is as follows:

Scenario:

Ateamofthreescientists\-\-\-Anna,Ben,andClara\-\-\-areconductingresearchontwophenomena\(0=gravitationalwaves,1=darkmatter\)\.Theyconducteachexperimentintwodifferentenvironments\(0=laboratory,1=field\)\.Foreachscientist,phenomenon,andenvironment,wedecidewhethertheexperimentwassuccessfullyconducted\.Eachdecisionisindependent\.

Conditions:

1\.EitherClarasuccessfullyconductsanexperimentondarkmatterinthefield,orAnnadoesnotsuccessfullyconductanexperimentondarkmatterinthelaboratory\.

2\.EitherClarasuccessfullyconductsanexperimentondarkmatterinthefield,orBendoesnotsuccessfullyconductanexperimentongravitationalwavesinthelaboratory\.

3\.EitherClaradoesnotsuccessfullyconductanexperimentondarkmatterinthefield,orBendoesnotsuccessfullyconductanexperimentongravitationalwavesinthelaboratory\.

4\.EitherClarasuccessfullyconductsanexperimentondarkmatterinthefield,orBensuccessfullyconductsanexperimentongravitationalwavesinthelaboratory\.

Question:

Canalltheseexperimentalconditionsbesimultaneouslysatisfied?

Output\.The model’s output is as follows:

<think\>

Letmeanalyzethisproblemstepbystep\.

First,Ineedtounderstandthevariables:

\-x\(i,j,k\)meansscientistisuccessfullyconductsanexperimentonphenomenonjinenvironmentk

\-iin\{0,1,2\}\(Anna,Ben,Clara\)

\-jin\{0,1\}\(gravitationalwaves,darkmatter\)

\-kin\{0,1\}\(laboratory,field\)

Nowletmetranslatetheconditions:

Condition1:EitherClarasuccessfullyconductsanexperimentondarkmatterinthefield,orAnnadoesnotsuccessfullyconductanexperimentondarkmatterinthelaboratory\.

\-Clara=i=2,darkmatter=j=1,field=k=1:x\(2,1,1\)

\-Anna=i=0,darkmatter=j=1,laboratory=k=0:x\(0,1,0\)

\-Condition1:x\(2,1,1\)∨\\lor¬\\lnotx\(0,1,0\)

Condition2:EitherClarasuccessfullyconductsanexperimentondarkmatterinthefield,orBendoesnotsuccessfullyconductanexperimentongravitationalwavesinthelaboratory\.

\-Clara=i=2,darkmatter=j=1,field=k=1:x\(2,1,1\)

\-Ben=i=1,gravitationalwaves=j=0,laboratory=k=0:x\(1,0,0\)

\-Condition2:x\(2,1,1\)∨\\lor¬\\lnotx\(1,0,0\)

Condition3:EitherClaradoesnotsuccessfullyconductanexperimentondarkmatterinthefield,orBendoesnotsuccessfullyconductanexperimentongravitationalwavesinthelaboratory\.

\-Clara=i=2,darkmatter=j=1,field=k=1:x\(2,1,1\)

\-Ben=i=1,gravitationalwaves=j=0,laboratory=k=0:x\(1,0,0\)

\-Condition3:¬\\lnotx\(2,1,1\)∨\\lor¬\\lnotx\(1,0,0\)

Condition4:EitherClarasuccessfullyconductsanexperimentondarkmatterinthefield,orBensuccessfullyconductsanexperimentongravitationalwavesinthelaboratory\.

\-Clara=i=2,darkmatter=j=1,field=k=1:x\(2,1,1\)

\-Ben=i=1,gravitationalwaves=j=0,laboratory=k=0:x\(1,0,0\)

\-Condition4:x\(2,1,1\)∨\\lorx\(1,0,0\)

LetmeuseZ3tocheckiftheseconditionscanbesimultaneouslysatisfied\.

ForZ3,I’llusex\_2\_1\_1forx\(2,1,1\)andx\_1\_0\_0forx\(1,0,0\)\.

</think\>

<tool\_call\>

fromz3importBool,Or,Not,And,Solver,sat,unsat

\#Definethevariables

x\_2\_1\_1=Bool\("x\_2\_1\_1"\)\#Clara,darkmatter,field

x\_1\_0\_0=Bool\("x\_1\_0\_0"\)\#Ben,gravitationalwaves,laboratory

\#Createtheconditions

condition1=Or\(x\_2\_1\_1,Not\(x\_0\_1\_0\)\)ifFalseelseOr\(x\_2\_1\_1,Not\(Bool\("x\_0\_1\_0"\)\)\)

condition2=Or\(x\_2\_1\_1,Not\(x\_1\_0\_0\)\)

condition3=Or\(Not\(x\_2\_1\_1\),Not\(x\_1\_0\_0\)\)

condition4=Or\(x\_2\_1\_1,x\_1\_0\_0\)

\#Createsolverandaddconstraints

solver=Solver\(\)

solver\.add\(And\(condition2,condition3,condition4\)\)

\#Checksatisfiability

result=solver\.check\(\)

print\(result\)

</tool\_call\>

<tool\_response\>

stdout:sat

</tool\_response\>

<think\>

Thesolverreturned"sat"whichmeanstheconditionsaresatisfiable\.Thismeansallconditionscanbesimultaneouslysatisfied\.

Therefore,theanswerisyes\.

</think\>

‘‘‘yes‘‘‘

Reward\.The reward score is as follows:

\{"format":0\.1,"correctness":1\.0,"tool\_success":0\.1,"equivalence":1\.0\}

Justification\.The model’s response contains a correctly parsed answer and a compilable Z3 tool call\. The variable mapping is as follows:x2,1,1x\_\{2,1,1\}is mapped to “Clara conducts the dark\-matter experiment in the field”,x1,0,0x\_\{1,0,0\}is mapped to “Ben conducts the gravitational\-wave experiment in the laboratory”, andx0,1,0x\_\{0,1,0\}is mapped to “Anna conducts the dark\-matter experiment in the laboratory”\.

The ground\-truth formula isFtruth=\(x2,1,1∨¬x0,1,0\)∧\(x2,1,1∨¬x1,0,0\)∧\(¬x2,1,1∨¬x1,0,0\)∧\(x2,1,1∨x1,0,0\)F\_\{\\text\{truth\}\}=\\left\(x\_\{2,1,1\}\\lor\\neg x\_\{0,1,0\}\\right\)\\land\\left\(x\_\{2,1,1\}\\lor\\neg x\_\{1,0,0\}\\right\)\\land\\left\(\\neg x\_\{2,1,1\}\\lor\\neg x\_\{1,0,0\}\\right\)\\land\\left\(x\_\{2,1,1\}\\lor x\_\{1,0,0\}\\right\)\.

The extracted formula isFpred=\(x2,1,1∨¬x1,0,0\)∧\(¬x2,1,1∨¬x1,0,0\)∧\(x2,1,1∨x1,0,0\)F\_\{\\text\{pred\}\}=\\left\(x\_\{2,1,1\}\\lor\\neg x\_\{1,0,0\}\\right\)\\land\\left\(\\neg x\_\{2,1,1\}\\lor\\neg x\_\{1,0,0\}\\right\)\\land\\left\(x\_\{2,1,1\}\\lor x\_\{1,0,0\}\\right\)\. AlthoughFpredF\_\{\\text\{pred\}\}does not include the clause\(x2,1,1∨¬x0,1,0\)\\left\(x\_\{2,1,1\}\\lor\\neg x\_\{0,1,0\}\\right\), it is still logically equivalent toFtruthF\_\{\\text\{truth\}\}\(that is,Ftruth↔FpredF\_\{\\text\{truth\}\}\\leftrightarrow F\_\{\\text\{pred\}\}\)\. In fact, the truth table is

x2,1,1x1,0,0x0,1,0F1F20000000100010000110010011101111100011100\\begin\{array\}\[\]\{c c c\|c c\}x\_\{2,1,1\}&x\_\{1,0,0\}&x\_\{0,1,0\}&F\_\{1\}&F\_\{2\}\\\\ \\hline\\cr 0&0&0&0&0\\\\ 0&0&1&0&0\\\\ 0&1&0&0&0\\\\ 0&1&1&0&0\\\\ 1&0&0&1&1\\\\ 1&0&1&1&1\\\\ 1&1&0&0&0\\\\ 1&1&1&0&0\\end\{array\}

### E\.2Solved Enigmata Example

Input\.The input instance is as follows:

1\.\*\*NOTATIONS:\*\*

Theinitialboardconsistsofemptycellsandblockedcells\.

Emptycellsaredenotedby’\.’,blockedcellsaredenotedby’X’,andstarsaredenotedby’\*’\.

2\.\*\*STARMUSTBEPLACEDINEMPTYCELL:\*\*

EachstarmustbeplacedinanEMPTYcell\.

Blockedcellscannotcontainstars\.

Youcanonlychangecellsdenotedby’\.’,andmustnotchangecellsdenotedby’X’\.

3\.\*\*EXACTLY1STARINEACHROWANDCOLUMN:\*\*

EachrowandcolumnmustcontainEXACTLYonestar\.

Notwostarscanbeinthesameroworcolumn\.

Thereshouldn’tberowsorcolumnswithoutstars\.

4\.\*\*NOADJACENTSTARSROW\-WISE,COLUMN\-WISE,ORDIAGONALLY:\*\*

Notwostarscanbeadjacenttoeachother,evendiagonally\.

\-Row\-wiseadjacency:twostarsareinthesamerow,andthereisnoemptycellbetweenthem\.

\-Column\-wiseadjacency:twostarsareinthesamecolumn,andthereisnoemptycellbetweenthem\.

\-Diagonaladjacency:twostarsareinthesamediagonal,andthereisnoemptycellbetweenthem\.

Notethatyouarepronetomakemistakesindiagonaladjacency,sobeextracareful\.Hereare2examplesofdiagonaladjacencyinapartialgrid:

‘‘‘

\.\*\.\.

\.\.\*\.

‘‘‘

‘‘‘

\.\.\*\.

\.\*\.\.

‘‘‘

Inbothcases,thetwostarsarediagonallyadjacent\.Youshouldavoidthissituation\.

5\.\*\*CHECKFORCONSTRAINTSANDBACKTRACK:\*\*

Ineachstep,youshouldcheckifitviolatestheconstraintsin2\.,3\.,and4\.

Ifyoufindinconsistencies,youshouldbacktrackandtryadifferentplacement\.

Ifyoufindthatyoucan’tplaceastaranywherewithoutviolatingtheconstraints,youshouldbacktrackandtryadifferentplacement\.

Sincethereisonlyonesolution,thereisgreatchanceyourfirstplacementisincorrect,whichmeansyoumightneedtostartover\.

6\.\*\*RESPONSEFORMAT:\*\*

Yourresponseshouldincludethefinalboard\.

Thefinalboardisarevisedversionoftheinitialboardinawaythatifyouneedtoplaceastarinanemptycell,replacethe’\.’witha’\*’\.

Don’tchangetheblockedcellsdenotedby’X’\.

Yourfinalboardshouldbewrappedbetween<begin\_board\>and<end\_board\>tags\.

Usethefollowingstructure:

FinalBoard:

‘‘‘

<begin\_board\>

\[FinalBoard\]

<end\_board\>

‘‘‘

Hereisthepuzzle:

\.XX\.X\.\.

\.XX\.\.X\.

\.XX\.XXX

\.\.\.\.\.\.\.

\.\.\.\.XX\.

\.\.X\.XXX

\.\.\.\.\.\.\.

Output\.The model’s output is as follows:

<think\>

Theuserwantsmetosolveastar\-battlepuzzle\.

Let’sstartbysettingupthemodelwithpysat,thensolve,thenprinttheresult:

Step1:Importpysatanddefinebinaryvariables‘star\[r\]\[c\]‘\.

Step2:Addconstraintsforeachrow/coltohaveexactlyonestar\(clauseslike‘sum\(star\[r\]\[c\]forallc\)==1‘\)\.

Step3:Addconstraintstopreventadjacent/diagonalstars\(novariableequalsanyneighborinthe3x3area\)\.

Step4:Addconstraintsonblockedcells\(eachstarvariableforablockedcellmustbefalse\)\.

Step5:Solvetheinstance\.

Step6:Extractthepositionswhere‘star\[r\]\[c\]‘istrueandconstructthefinalboard\.

</think\>

<tool\_call\>

frompysat\.formulaimportCNF,IDPool

frompysat\.solversimportGlucose3

defsolve\(\):

puzzle=\[

\["\.","X","X","\.","X","\.","\."\],

\["\.","X","X","\.","\.","X","\."\],

\["\.","X","X","\.","X","X","X"\],

\["\.","\.","\.","\.","\.","\.","\."\],

\["\.","\.","\.","\.","X","X","\."\],

\["\.","\.","X","\.","X","X","X"\],

\["\.","\.","\.","\.","\.","\.","\."\],

\]

rows=len\(puzzle\)

cols=len\(puzzle\[0\]\)

vpool=IDPool\(\)

stars=\[\[vpool\.id\(f"star\_\{r\}\_\{c\}"\)forcinrange\(cols\)\]forrinrange\(rows\)\]

cnf=CNF\(\)

forrinrange\(rows\):

cnf\.append\(list\(stars\[r\]\)\)

forcinrange\(cols\):

cnf\.append\(\[\-stars\[r\]\[c\]\]\)

forcinrange\(cols\):

cnf\.append\(list\(stars\[r\]\[c\]forrinrange\(rows\)\)\)

forrinrange\(rows\):

forcinrange\(cols\):

fordrin\(\-1,0,1\):

fordcin\(\-1,0,1\):

ifdr==0anddc==0:

continue

nr,nc=r\+dr,c\+dc

if0<=nr<rowsand0<=nc<cols:

cnf\.append\(\[\-stars\[r\]\[c\],\-stars\[nr\]\[nc\]\]\)

forrinrange\(rows\):

forcinrange\(cols\):

ifpuzzle\[r\]\[c\]=="X":

cnf\.append\(\[\-stars\[r\]\[c\]\]\)

withGlucose3\(bootstrap\_with=cnf\.clauses\)assolver:

ifnotsolver\.solve\(\):

return"Unsolvable"

model=set\(solver\.get\_model\(\)\)

planted=\[\]

forrinrange\(rows\):

forcinrange\(cols\):

ifstars\[r\]\[c\]inmodel:

planted\.append\(\(r,c\)\)

final\_board=\[\]

forrinrange\(rows\):

row\_chars=\[\]

forcinrange\(cols\):

ifpuzzle\[r\]\[c\]=="X":

row\_chars\.append\("X"\)

elif\(r,c\)inplanted:

row\_chars\.append\("\*"\)

else:

row\_chars\.append\("\."\)

final\_board\.append\(""\.join\(row\_chars\)\)

return"\\n"\.join\(final\_board\)

print\(solve\(\)\)

</tool\_call\>

<tool\_response\>

stdout:Unsolvable

</tool\_response\>

<think\>

Theprevioussolverreturned"Unsolvable",whichshouldnotbepossibleforawell\-formedpuzzlewithauniquesolution\.Imusthavemadeanerrorinhowtheconstraintsweremodeled\-\-\-specificallytheadjacencyconstraintmaybetoorestrictiveorincorrectlyimplemented\.Letmecarefullyreconsiderthediagonaladjacencymodelandsimplifytheexact\-1constraintsusinglinearexpressions,thenretrythesolvercall\.

</think\>

<tool\_call\>

frompysat\.formulaimportCNF,IDPool

frompysat\.solversimportGlucose3

frompysat\.cardimportCardEnc,EncType

defsolve\(\):

puzzle=\[

\["\.","X","X","\.","X","\.","\."\],

\["\.","X","X","\.","\.","X","\."\],

\["\.","X","X","\.","X","X","X"\],

\["\.","\.","\.","\.","\.","\.","\."\],

\["\.","\.","\.","\.","X","X","\."\],

\["\.","\.","X","\.","X","X","X"\],

\["\.","\.","\.","\.","\.","\.","\."\],

\]

rows=len\(puzzle\)

cols=len\(puzzle\[0\]\)

vpool=IDPool\(\)

stars=\[\[vpool\.id\(f"star\_\{r\}\_\{c\}"\)forcinrange\(cols\)\]forrinrange\(rows\)\]

cnf=CNF\(\)

forrinrange\(rows\):

cnf\.extend\(CardEnc\.equals\(lits=stars\[r\],bound=1,vpool=vpool,encoding=EncType\.seqcounter\)\.clauses\)

forcinrange\(cols\):

cnf\.extend\(CardEnc\.equals\(lits=\[stars\[r\]\[c\]forrinrange\(rows\)\],bound=1,vpool=vpool,encoding=EncType\.seqcounter\)\.clauses\)

forrinrange\(rows\):

forcinrange\(cols\):

fordrin\(\-1,0,1\):

fordcin\(\-1,0,1\):

ifdr==0anddc==0:

continue

nr,nc=r\+dr,c\+dc

if0<=nr<rowsand0<=nc<cols:

cnf\.append\(\[\-stars\[r\]\[c\],\-stars\[nr\]\[nc\]\]\)

forrinrange\(rows\):

forcinrange\(cols\):

ifpuzzle\[r\]\[c\]=="X":

cnf\.append\(\[\-stars\[r\]\[c\]\]\)

withGlucose3\(bootstrap\_with=cnf\.clauses\)assolver:

ifnotsolver\.solve\(\):

return"Unsolvable"

model=set\(solver\.get\_model\(\)\)

planted=\[\]

forrinrange\(rows\):

forcinrange\(cols\):

ifstars\[r\]\[c\]inmodel:

planted\.append\(\(r,c\)\)

final\_board=\[\]

forrinrange\(rows\):

row\_chars=\[\]

forcinrange\(cols\):

ifpuzzle\[r\]\[c\]=="X":

row\_chars\.append\("X"\)

elif\(r,c\)inplanted:

row\_chars\.append\("\*"\)

else:

row\_chars\.append\("\."\)

final\_board\.append\(""\.join\(row\_chars\)\)

return"\\n"\.join\(final\_board\)

print\(solve\(\)\)

</tool\_call\>

<tool\_response\>

stdout:\.XX\.X\*\.

\.XX\*\.X\.

\*XX\.XXX

\.\.\*\.\.\.\.

\.\.\.\.XX\*

\.\*X\.XXX

\.\.\.\.\*\.\.

</tool\_response\>

<think\>

Thesolverreturnedavalidsolution:

‘‘‘

\.XX\.X\*\.

\.XX\*\.X\.

\*XX\.XXX

\.\.\*\.\.\.\.

\.\.\.\.XX\*

\.\*X\.XXX

\.\.\.\.\*\.\.

‘‘‘

Thisshouldbeformattedaccordingtotherequiredoutputstructurewiththe<begin\_board\>and<end\_board\>tags\.Letmeverifythissolutioniscorrect:

\-Row0:staratcolumn5

\-Row1:staratcolumn3

\-Row2:staratcolumn0

\-Row3:staratcolumn2

\-Row4:staratcolumn6

\-Row5:staratcolumn1

\-Row6:staratcolumn4

Thisgivesallcolumns\[5,3,0,2,6,1,4\],whicharealldistinct\(0\-6exactlyonce\)\.Noroworcolumnhasmorethanonestar\.Checkingdiagonallyadjacentstars:

\-Row0col5andRow1col3:notadjacent

\-Row1col3andRow2col0:notadjacent

\-Row2col0andRow3col2:notadjacent

\-Row3col2andRow4col6:notadjacent

\-Row4col6andRow5col1:notadjacent

\-Row5col1andRow6col4:notadjacent

Noneareadjacenthorizontally,vertically,ordiagonally\.Theplacementalsorespectstheblockedcells\(’X’\)\.Thisisthecorrectanduniquesolution\.

</think\>

FinalBoard:

‘‘‘

<begin\_board\>

\.XX\.X\*\.

\.XX\*\.X\.

\*XX\.XXX

\.\.\*\.\.\.\.

\.\.\.\.XX\*

\.\*X\.XXX

\.\.\.\.\*\.\.

<end\_board\>

‘‘‘

Justification:The first PySAT call creates variables for all 49 cells and adds an at\-least\-one clause for each row, but this formulation produces an UNSAT result that contradicts the task’s stated unique\-solution premise\. The model then corrects the formula and obtains a satisfying solution\. The star columns by row are\(5,3,0,2,6,1,4\)\(5,3,0,2,6,1,4\)\. These placements ensure that every row and column has exactly one star, that each star replaces an empty cell, and that the star columns in adjacent rows differ by more than one\. Therefore, the solution is correct, as confirmed by the verifier\.

## Appendix FAdditional Training Trajectories

Additional training trajectories of detailed reward component, the test correctness and entropy is shown to Figure[5](https://arxiv.org/html/2610.14402#A6.F5)\.

![Refer to caption](https://arxiv.org/html/2610.14402v1/appendix_image/total_reward.png)\(a\)Total rewardrr\.
![Refer to caption](https://arxiv.org/html/2610.14402v1/appendix_image/correctness.png)\(b\)Validation correctness\.
![Refer to caption](https://arxiv.org/html/2610.14402v1/appendix_image/policy_entropy.png)\(c\)Policy entropy\.
![Refer to caption](https://arxiv.org/html/2610.14402v1/appendix_image/adjusted_correctness_reward.png)\(d\)Adjusted correctness rewardrcorrectr\_\{\\text\{correct\}\}\.
![Refer to caption](https://arxiv.org/html/2610.14402v1/appendix_image/format_reward.png)\(e\)Format rewardrformatr\_\{\\text\{format\}\}\.
![Refer to caption](https://arxiv.org/html/2610.14402v1/appendix_image/solver_usage_divide_by_two.png)\(f\)Tool rewardrtoolr\_\{\\text\{tool\}\}\.
![Refer to caption](https://arxiv.org/html/2610.14402v1/appendix_image/logic_equivalence_reward.png)\(g\)Logic\-equivalence rewardrequivr\_\{\\text\{equiv\}\}\.

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\.