Have Large Language Models Learned to Reason? A Characterization via 3-SAT
Authors: RISHI HAZRA
Gabriele Venturato
Pedro Zuidberg Dos Martires
Luc De Raedt
Venue: COLM 2025 (2025)
Keywords: Large Language Models
Reasoning
Computational Complexity
Logic
Satisfiability
Phase Transitions
TL;DR: We use phase transitions in random 3-SAT to characterize reasoning abilities of LLMs.

Abstract: Large Language Models (LLMs) have been touted as AI models possessing advanced reasoning abilities. In theory, autoregressive LLMs with Chain-of-Thought (CoT) can perform more serial computations to solve complex reasoning tasks. However, recent studies suggest that, despite this capacity, LLMs do not truly learn to reason but instead fit on statistical features. To study the reasoning capabilities in a principled fashion, we adopt a computational theory perspective and propose an experimental protocol centered on 3-SAT -- the prototypical NP-complete problem lying at the core of logical reasoning and constraint satisfaction tasks. Specifically, we examine the phase transitions in random 3-SAT and characterize the reasoning abilities of state-of-the-art LLMs by varying the inherent hardness of the problem instances. By comparing DeepSeek R1 with other LLMs, our findings reveal two key insights (1) LLM accuracy drops significantly on harder instances, suggesting all current models struggle when statistical shortcuts are unavailable (2) Unlike other LLMs, R1 shows signs of having learned the underlying reasoning. Following a principled experimental protocol, our study moves beyond the benchmark-driven evidence often found in LLM reasoning research. Our findings highlight important gaps and suggest clear directions for future research. Link to our code.

Published as a conference paper at COLM 2025
Have Large Language Models Learned to Reason? A Characterization via 3-SAT
Rishi Hazra', Gabriele Venturato", Pedro Zuidberg Dos Martires' Luc De Raedt
CCentre for Applied Autonomous Sensor Systems (AASS),
Örebro University, 70182, Sweden
"Department of Computer Science, KU Leuven, 3001, Belgium (rishi.hazra, pedro. zuidbergi mostmartires @o (gabriele, venturato, luc. d
Abstract
Large Language Models (LLMs) have been touted as AI models possessing advanced reasoning abilities. In theory, autoregressive LLMs with Chain- of-Thought (CoT) can perform more serial computations to solve complex reasoning tasks. However, recent studies suggest that, despite this capacity, LLMs do not truly learn to reason but instead fit on statistical features. To study the reasoning capabilities in principled fashion, we adopt a computational theory perspective and propose an experimental protocol centered on 3-SAT the prototypical NP-complete problem lying at the core of logical reasoning and constraint satisfaction tasks. Specifically, we examine the phase transitions in random 3-SAT and characterize the reasoning abilities of state-of-the-an LLMs by varying the inherent hardness of the problem instances. By comparing DeepSeek Ri with other LLMss, our findings reveal two key insights (1) LLM accuracy drops significantly on harder instances, suggesting all current models struggle when statistical shortcuts are unavailable (2) Unlike other LLMs, R1 shows signs of having learned the underlying reasoning. Following a principled experimental protocol, our study moves beyond the benchmark-driven evidence often found in LLM reasoning research. Our findings highlight important gaps and suggest clear directions for future research. Link to our code.
Introduction
The success and versatility of Large Language Models (LLMs) have sparked widespread interest and debate on whether LLMs are capable of reasoning. Recent studies suggest that LLMs are inherently capable of zero-shot reasoning (Kojima et al., 2022). This ability has been shown emerge and improve with scale (Wei et al., 2022a; Srivastava et al., 2023), and can be further enhanced through prompting techniques that encourage LLMs to think step-by- step (Wei al., 2022b; Yao et al., 2023b). Demonstrations include, inter alia, planning (Huang et al., 2022; Hazra et al., 2024b), theorem proving (Jiang et al., 2023; Welleck et al., 2022), search and optimization Ciomera-Paredess
al., 2024; Hazra al., 2024a), self-reflection (Yao et al., 2023a; Madaan et al., 2023), and tool usage (Schick et al., 2023).
Conversely, a growing body of research presents a more critical view of these reasoning abilities. For instance, LLMs may exhibit limitations in consistent logical reasoning (Ark- oudas, 2023; Saparov & He, 2023), effective planning (Valmeekam al., 2022), and accurate self-evaluation of their outputs (Stechly et al., 2023). So, to what extent can LLMs reason?
Recent works address this question by characterizing LLMs' theoretical capabilities and limitations using worst-case complexity analysis. Peng et al. (2024) demonstrated that multi-layer transformers cannot solve problems such as Derivability, 2-SAT, and Horn SAT. However, with T-chain of thought (CoT) steps, transformers' abilities can be extended up to those solvable by Boolean circuits size T (Li et al., 2024). Moreover, with polynomially many correct intermediate CoT steps, an LLM can compute all circuits in polynomial size,

---

Published as a conference paper at COLM 2025
P/poly, superclass of P. Therefore, LLMs should able to solve reasoning problems falling into these complexity classes, like 2-SAT and Homn-SAT. It is also expected to solve some but not all - 3-SAT instances since certain problems may require circuit complexities that exceed polynomial bounds. Empirically, this aligns with test-time compute scaling studies that show improved reasoning performance with increased computational resources (Light- man et al., 2024; Snell et al., 2025). Thus, from theoretical standpoint, LLMs equipped with CoT possess the capacity to solve reasoning problems falling in P P/Poly.
However, despite this, recent works have shown that LLMs are not learning to reason, by fitting on statistical features and not internalizing the logic (i.e. learning to reproduce the style and not logic) (Zhang et al., 2023) much like the Clever Hans Cheat (Bachmann Nagarajan, 2024). With the advent of Large Reasoning Models (LRMs) like DeepSeek R1 (DeepSeek-Al) 2025a) which leverage more test-time compute, there is renewed optimism about enhancing reasoning capabilities. However, is unclear if this marks a real step change, due to limitations in current reasoning benchmarks like (1) growing concerns about dataset contamination' (Zhang et al., 2024) that can inflate the reasoning performance; (2) conflation of commonsense reasoning rooted in relrieving world knowledge, and logical or deductive reasoning requiring algebraic manipulation of knowledge (Genesereth & Nilsson, 1987) - making it challenging to decouple the two.
To move beyond these limitations, more principled approach to evaluating reasoning is needed. We adopt Leon Bottou's definition, which defines reasoning as " "algebraically manipulating previously acquired knowledge to answer new question" (Bottou, 2014). This closely aligns with Russell and Norvig's description of Al as rational thinking (Russell & Norvig, 2010). Building on this, we ask: Have LLMs learned to reason, and if so, to what extent? We answer through the following contributions:
(1) Characterizing LLM-reasoning from a computational theory perspective. Adhering to Leon Bottou's s definition, we propose an experimental framework centered on 3-SAT, to eval- uate reasoning. Introduced in Figure 1, 3-SAT a foundational problem in computational complexity, and many problems in Al such as (propositional fragments of) logical reasoning, planning, and constraint satisfaction can be reduced to 3-SAT. We also extend our analysis to tractable fragments like 2-SAT (NL-Complete) (Bollobás et al., 2001) and 1-3 Horn-SAT (P- (P-Complete) (Demopoulos & Vardi, 2006) which also exhibit phase transitions, revealing interesting observations across complexity classes. Our approach provides formal and robust evaluation of reasoning abilities and bridges computational theory with modern AI.
(2) Studying Phase Transition Characteristics of LLMs. We investigate the phase transition characteristics of LLMs (Cheeseman et al., 1991), i.e., how LLMs' performance varies in the easy and hard regions of the problem space, unlike standard reasoning benchmarks that overlook variations due to inherent hardness of problems. We observe that LLM performance declines in the hard region where statistical features are largely absent.
(3) Comprehensive evaluation of state-of-the-an LLMs. We conducted extensive exper- iments across state-of-the-art open-source and proprietary LLMs. We find a significant gap between the performances of DeepSeek R1 (DeepSeek-AL 2025a) to other LLMs like GPT-40 AO,enAI, 2024), Claude 3.7 Sonnet (Anthropic, 2025), Gemini 2.0 Flash (Google, 2024), and DeepSeek V3 (DeepSeek-Al) 2025b). Interestingly, the CoT traces produced by DeepSeek R1 reveal patterns suggestive of an in-context tree search with backtracking, which may account for its superior performance. In contrast, the other models consistently fail to demonstrate comparable reasoning capabilities. This leads us to believe that LRMs like R1 could be step-change in reasoning abilities.
2 Preliminaries
2.1 Phase Transitions in Random 3-SAT
We study the reasoning capabilities of LLMs on random 3-SAT problems. 3-SAT consti- tutes one of the most fundamental problems in computer science as it is the prototypical
Data closely resembling the benchmark leaks into the training data.
2

---

Published as a conference paper at COLM 2025
X;
Coejunctive Normal Form (CNF)
The SAT Problem
X1
X
Solver Make at leaer one call green every ron, OR, no solution exitts, NO
X
[X]] V X
V
A
X
Congratu you won
( V X1
y K
Ittrral all idertiial Iterats green and all negative Iterals red.
X
[-X y Xg V A
[-]] 7-X V X
X V- V A
Xd)
Figure The 3-SAT problem, visualized using a variant of the SAT game (Roussel). In SAT, the goal is to return truth assignment to Boolean variables that satisfies Boolean formula in conjunctive normal form (CNF), or return unSAT if none exists. In the visualization, each row represents a clause-a disjunction (logical OR, V) of literals, where each literal is either positive (X1) or negative (-X1). clause satisfied if at least one of its literals is assigned true. Clauses are joined by logical AND (A), so all must be satisfied for the formula to hold. no such assignment exists, the formula unsatisfiable
NP-complete problem, lying at the foundation of computational complexity theory. More- over, various prevalent reasoning problems in artificial intelligence, such as planning and constraint satisfaction, can be reduced to solving 3-SAT problems (Garey & Johnson, 1990).
By randomly sampling 3-SAT formulas?, we avoid domain-specific biases, and it lets us control the complexity of the generated formulas. In fact, an interesting empirical observation is the presence of phase transition in random 3-SAT problems (Cheeseman et al., 1991). When randomly sampling 3-SAT formulas, one can observe a sharp change in the probability
3-SAT formula being satisfiable when plotted against is the number of clauses and и is the number of variables. For random 3-SAT, this phase transition occurs at de R 4.267 (Mertens et al., 2006; Ding et al., 2015), i.e. the point at which randomly sampled 3-SAT formula has equal probability to be satisfiable or unsatisfiable. This naturally divides 3-SAT problems into three regions: the under-constrained region below the threshold (Easy), the constrained region in the neighborhood of the threshold (Hard), and the over-constrained region above the threshold (Easy), cf. Figure 2.
m/nu, where m
2.2
SAT Solvers
SAT solvers are tools to automatically verify the satisfiability of propositional logic formulas. (DPLL) algorithm (Davis et al., 1962) is key component of modern SAT solvers. It consists of a backtracking- based algorithm, equipped heuristts,, efficiently explore the search space and determine if formula is satisfiable (Figure 2). The algorithm selects literal and assigns truth value to it. This is applied recursively until all clauses are satisfied, meaning that the original formula satisfiable. Modern SÄT solvers are based on Conflict-Driven Clause Learning (CDCL) (Silva & Sakallah, 1996) which enhances DPLL with conflict analysis and clause learning. In Figure 2, we show how the time to determine the satisfiability of random 3-SAT formula varies in function of a. Most prominently, we see a pronounced peak in runtime around the &c.
The Danii-Putaan-Loggmm---oooo
Analogously to characterizing SAT solvers by their behavior with varying a, we study the reasoning capabilities of LLMs with respect the phase transition in random 3-SAT.
3 Related Work
Merrill & Sabharwal (2023) established that multi-layer transformers belong to the complex- ity class log-uniform TC Subsequently, Peng et al. (2024) demonstrated that multi-layer transformers cannot solve problems such as Derivability, 2-SAT, Horn SAT, and Circuit
We Selman al. (1996) random model, where clauses are sampled with replacement.
3

---

Published as a conference paper at COLM 2025
Phase Transitions
(X6 X XI
Xo V X G
1.0
Salver narninng time
Probisakiffabiiy)
0,025
-2JA
X
X3)
0.020
DACOmO22
X6
0.6
0.015
0.5
X1
X:
0.4
0.3
0.2
0.005
Easy Hard
Figure 2: [Left]: Random 3-SAT Phase Transitions (Cheeseman et al., 1991). Plotted in red the probability of a randomly sampled 3-SAT formula being satisfied against the hardness a of the formula. We can observe clear phase transition occurring at A, R 4.267 (marked by a green We identify two Easy regions, one on either side of a, The gray area in the middle denotes the Hard region. The boundaries of the hard region are defined where the probability of the formula being satisfied ceases to be deterministically 1 (left) or (right). The solid blue line shows the mean time taken by the MiniSAT solver to solve 3-SAT instances. Notably, there is a spike in the solver's 's runtime near &.- This is due to the absence of useful heuristics in this region, forcing the solver to resort to exhaustive searches. [Right]: DPLL Search Trace from SAT Solver for the given formula. Red boxes denote unsatisfiable assignments; the green box highlights satisfying one. 0, 1 are truth assignments.
Evaluation unless L=NL. While these results provide worst-case performance bounds for transformer architectures, their relevance to average-case complexity is limited (Coarfa et al., 2000), therefore, offering only partial insights into the practical reasoning capabilities of LLMs. Notably, recent works have shown that 7 chain of thought (CoT) steps can extend transformers' abilities beyond TC², up to those solvable by Boolean circuits of size T (Li et al., 2024). With T being polynomial in the input size, LLMs can in theory solve problems in P class like 2-SAT and Horn SAT. Our SAT experiments support this, showing improved reasoning with extended CoT steps. Yet, a central question remains: can LLMs learn to reason effectively, given that they are theoretically capable?
To this end, Dziri et al. (2023) investigate the performance of LLMs on compositional tasks with varying levels of complexity. Their experiments reveal significant performance decline as task complexity increases, measured by problem size and reasoning depth. The findings indicate that while models can memorize single-step operations from training, they fail to compose these steps into correct reasoning paths. Similarly, Zhang et al. (2023) found that BERT-based models fail to generalize (i.e., not NP-complete) problem class, overfitting to statistical features during training. Our results extend these findings by showing that performance declines are better explained by inherent problem hardness as captured by phase transitions - rather than size or depth alone.
autoof-distributin data even within a tractable
Closest to our work is the NVHardEval (Fan et al., 2024), which examines reasoning across various computational complexity classes. We extend this by analyzing phase transition characteristics and how performance varies with inherent problem hardness. Our evaluation focuses on classes with known phase transitions (Schaefer, 1978), including 2-SAT (NL- Complete), 1-3 Horn-SAT (P-Complete), and 3-SAT (NP-Complete). By comparing LRMs with LLMs, gain deeper insights into the impact of longer reasoning traces, performance across easy and hard regions, and variation with model count (i.e., number of solutions).
Our findings also align with Xiang et al. (2025), who claim that classical CoT training data fails to capture the non-linear and iterative nature of complex reasoning. They propose Meta-CoT, which explicitly models this "thinking" process. We observe that DeepSeek R1
4

---

Published as a conference paper at COLM 2025
exhibits Meta-CoT-like behavior, autoregressively generating search trees that reflect latent reasoning steps - suggesting that the model has, to some extent, learned to reason.
Methodology
4.1
Using LLMs as 3-SAT Solvers
To use LLMs as 3-SAT solvers, we reframe the 3-SAT problem as a natural language menu- selection problem, termed SAT-Menu. As shown in Box 1, the prompt input to the LLM consists of task outline, along with specific scenario detailing the dietary preferences of set of people. The LLM's objective is to identify combination of orderable (akin to positive literals) and non-orderable (akin to negative literals) food items that meet these preferences; or declare the situation unsatisfiable (unSAT) if no valid combination exists. Note, that the prompt example in Box 1 constitutes a minimal example stripped of all details. The complete system prompt incorporates techniques known to enhance the apparent reasoning capabilities of LLMs, such as chain-of-thought (Co'T) (Wei et al., 2022b) and in-context learning (Brown et al., 2020) (see Box Appendix for the full prompt).
Additionally, we introduce a second problem formulation where the LLM is directly given the underlying 3-SAT formula Conjunctive Normal Form (CNF). We refer to this scenario as SAT-CNF. Specifically, in this setting, the problem is presented as a list of integers to the LLM, similar to the approach outlined in SAT Game (Figure 1). For more details about the prompt, we refer the reader to Box 3 in the Appendix.
Box 1: SAT-Menu Prompt
# System Message
Your task is to output two distinct lists of food items, one denoting what be ordered ('orderable') and the other what cannot mrdderrrer,,le", of individuals. Each person must find the selection satisfactory based on their likes dislikes. The satisfaction criteria are: 1. A person is satisfied if at least one liked item is in 'orderable' list or one disliked item is in 'not.orderable' list. 2. No item can appear on both lists. 3. All participants must be satisfied by the combination of the two lists. 4. Importantly, no such combination exists that satisfies all, output empty lists for both. Check carefully before finalizing. You always think step-by-step and show all your work in the explanation. Output your final solution comma-separated list of strings in Python code (orderable [...], _ofderraaeellee = [..]]}
meet the preferences a group
Input for new problem
Preferences: Jay: Likes nachos, ratatouille. Dislikes pie. Ada: Likes pie. Dislikes burger, ravioli. Zoe: Likes ravioli. Dislikes pie, burger. Arun: Likes ratatouille. Dislikes pie, nachos. Ula: Likes ratatouille. Dislikes ravioli, nachos. Ying: Likes nachos, ratatouille. Disfikes burger.
We consider two 3-SAT variants to evaluate reasoning Decision problem (NP-complete) where the model determines satisfiability, answering "yes" or "no"; and the Search problem (NP-hard), where it should return a satisfying assignment if it exists, else return "no".
Since we have theoretical bounds that apply specifically to autoregressive LLMs, we restrict our evaluation to state-of-the-art models that follow this paradigm namely, GPT-4o (Ope- nAI, 2024), Gemini 2.0 Flash (Google, 2024), Claude 3.7 Sonnet (Anthropic, 2025), and DeepSeek V3 (DeepSeek-AI, 2025b). Additionally, 2025a) in our analysis, as (1) we have access to its tf (CoT) "thinking" tokens, which we can confirm are generated autoregressively); (2) it is one of the top m The generation configurations are listed in Appendix Table 2. To verify the LLM-generated solutions, we employed MiniSAT v2.2 (Eén & Sörensson, 2003) solver.
include DeepSeek R1 (DeepSeek-AI,
Althhough other thinking models exist, they either do not expose their thinking tokens only provide them through their respective user interface. As such, we cannot verify whether their reasoning is produced autoregressively or through search-based methods at test time. hhtts://hhuggingface.oo hhaaemmaa//haboo--eeeeeeeeeeerr
5

---

Published as a conference paper at COLM 2025
3-SAT (SAT-Menu)
02
Claude 3.7 Sonnet
EBT:4n
DeepSeek Vi-wayy
Gentni 2.0 Flash
DeepSeck V3 hard
Decpbtcc
Decptock Ki-atoy
Despptesk
Deeptwokk Hi-haad
catisfaciitt ratto
Figure 3: [Left] 3-SAT performance comparison for the search version of SAT-Menu. [Right] Accuracy vs. satisfiability ratio on the search version of SAT-Menu. We only include satisfiable instances and analyze hard (solid line) and easy regions (dashed line) separately. We use 90% confidence intervals quantify uncertainty around the estimated accuracy. In the plots, these intervals help assess the reliability of accuracy estimates narrow bands indicate high certainty, while wider bands suggest greater variability.
Notably, techniques such Tree-of-Thoughts (Yao et al., 2023a), Best-of-N (Wang al., 2023) sampling, or other tree-based search frameworks effectively wrap LLMs in an external symbolic search and are beyond the scope of our analysis. These methods use the LLM to generate ideas (nodes of the tree) while orchestrating search or backtracking over a tree data structure. Crucially, the graph algorithm (e.g,, tree traversal, backtracking) is not internally generated or maintained by the LLM. Instead, it is externally imposed. Our goal assess whether LLMs can natively reason for example, whether they can generate multiple candidate solutions, maintain them in memory, reason over them, and converge to a consistent answer entirely in context.
4.2 Dataset Generation
To generate 3-SAT data, we varied a = m/n as a parameter to guide the generation process.
For each E [1, the Appendix provides the full range of values. MiniSAT v2.2 (Eén & Sörensson, 2003) labels each instance satisfiable unsatisfiable. Additionally, each instance is annotated with model count (i.e. number of feasible solutions for formula) using the D4 model counter (Lagniez Marquis, 2017).
selected
[1, [1] based feasible values of m. Table in
For SAT-Menu setup, we map each instance (i.e. CNF formula) to a menu selection puzzle. The goal is to select combination of orderable and non-orderable food items way that satisfies everyone's preferences. To this end, food item is sampled without replacement corresponding to the list of variables in the formula. Then, every clause in the formula is treated as the preferences for an individual, leading to the creation of two distinct lists for each person: "Likes," " for food items linked to positive literals, and "Dislikes," for those associated with negated literals, cf. Box 2.
Detailed statistics and data generation processes for 2-SAT and Horn-SAT are provided in Appendix A. All our experiments use pool of randomly sampled z 5000 formulas which include satisfiable and unsatisfiable instances.
5
Results
5.1
Do LLMs Reason?
We evaluate the performance LLMs by measuring their accuracy in solving SAT Search across formulas with varying As shown in Figure 3 [Left], we find that all LLMss exhibit

---

Published as a conference paper at COLM 2025
2:6 (ATCCM))
1-5 Hom-557 (56TCM)
2:5AT (SA7-rerrl
Same:
Claake Stowet
Figure 4: Performance across all complexity classes for the search problem. R1 outperforms all LLMs across all complexity classes. From left to right, 3-SAT (SAT-CNF), 1-3 Horn SAT (SAT-CNF), and 2-SAT (SAT-Menu). It can be observed that LLM performances are affected around the critical points for 3-SAT (a, 4.267) and 2-SAT (n, 1.0). We use 90% confidence intervals to quantify uncertainty around the estimated accuracy narrow bands indicate high certainty.
inverted phase transitions (Lasy-Hard-Easy pattern) in the SAT Search problem. Their performance is high in the easy regions, while it significantly drops to 10% in the hard region. The hard region performance remains unaffected by in-context learning (Appendix Figure 10). We also observe that R1 significantly outperforms other LLMs where R1's accuracy in the hard region surpasses even the easy-region performance of LLMs.
similar performance trend is observed for SAT-Decision (Appendix Figure 10). From the confusion matrix (Appendix Figure 12), we observe that R1 accurately detects satisfiable formulas, demonstrating a higher degree of soundness in its reasoning. However, it often fails to find the satisfying assignment itself, indicating limited completeness in the hard region. Other LLMs, by contrast, exhibit lower levels of both soundness and completeness.
In Figure 3 [Right], plot the performance of LLMs against the satisfiability ratio, defined as model count where the model count the number of satisfying assignments and ı is 2" the number of variables. This denotes the probability that a randomly selected variable assignment satisfies the given 3-SAT theory We can observe a clear dependence between the accuracy and satisfiability ratio: formulas with more satisfying assignments tend to be easier for LLMs. This holds across both easy and hard regions. R1, however, maintains consistent accuracy regardless of satisfiability ratio, much like a classical SAT solver. Similar plots comparing other LLMs are shown in Appendix Figure 11.
We also test 2-SAT (Figure 4), where we observe a distinct dip in LLM performance around the known phase transition at a, (Bollobás et al., 2001), indicating sensitivity to structural hardness even in problems within NL class. However, LLMSs show no clear patterns on 1-3 Horn-SAT. In contrast, R1 achieves near-perfect accuracy both 2-SAT and Horn-SAT, showing no degradation near the phase transition. This suggests that R1 handles problems in the lower complexity classes with ease.
5.2 Has R1 internalized search?
We qualitatively analyzed the search traces generated by R1 and other LLMs on SAT-CNF (Figure 5) and ŠAT-Menu tasks (Figure 8). Specifically, we annotated the "thinking" traces and attempted to map them to known symbolic search algorithms better understand the type and depth of search strategies employed, particularly by R1.
In Figure 5, we highlight failure case where both R1 and GPT-4o incorrectly conclude that satisfiable formula is unsatisfiable. Despite such failures, our analysis reveals that R1 consistently exhibits surprisingly coherent and interpretable search behaviors, including:
Note, this is different from the probability that at least one satisfying assignment exists. Two formulas can both be satisfiable but have different model counts, hence different satisfiability ratios.
7

---

Published as a conference paper at COLM 2025
21, [-6. 4. 10]
(1,,,,,,1,,-,,, 17,
31
61
8, 5.
[7.6 91. [-6, 1,66,4400 8, [-6, 1.
17,2,6), 14, 9, (7, 10),
16,
5,
41,
[2,
-7, 16
1, 4, (-0, 9,1..,11
X10
X 10
20
X1
X1
21
X7
X4
?
X3
X5
X5
X
23
X6
?
XA
Xs
XA
?
24
X9
X
X8
X
3
3
X5
26
18
X2
X2
X5
8
X
Let start by chacking unit classes, but wall, al ciussos here are disjunctions three So, there ar no unit dauses. (Heurtetic Usage: Unit Clauses) Another approach look for pure lttrrls. pure Iaraa appears only positive only negative form throughout all disuses (Heurtstic Usage: Purn (embs)
approach: look variables appeor frequently, Let's occurrecces of each variable
(ignoring sign). (Heuriate Usagu: Maximum Goourencas iinum clausss)
Well make guassee when necessary. backtrack centrod
New, check
(Fatee). -8.8)
imsolinng
We can gready approach oach assign
requir moppcttooly (Heuristic Usaga:
()
vartable make the
not
yul assigned If aleead assignad, check
Walt, dause 6: (46 -.3] Sinre is Trun, -5 Falen -9 is True (since tmi aton) So clause 8 requuees 3 be
susifiis the dause.
"Tue. So 3 must be True. /Mistake: Clause 6 arradd satisfied in stop 7, nowaver it's not wrong to ser X,
ceee -1 ces cenanee sen cee cesanee Clause (Falee) (Fatoe)
but
Cause Assign: True
Cause Assign:: True
Tiuu.. So we have conflict must be both True and Falso. This moans oument assigrments monts lead contteciction We
Cluss Assign: trum
backtrack. (Backtracking: Step 9)
On Assign Falise
Causes 5,8.7.3
Where did -Traa,, but clause 10 requring 1-Fabe Lit's backraack where we aut E-ru.e Maybe instead of setting ge BeTrue, we should sut BsFabe and see what happens. Walt but when we sot 4-urue dause 4 [-4, 6] is Far need ol
wrong? Lat's see. The conflitt arises from setting B-Tra which leads dluss 22 requring
Caause 12. Assign False
Gause 14: Ass oooign F:Fals
Gause 14 is sattched
deeia then reed E-False. Lat's backtrack where we set True and B=True, but then Instead of setting G-True, set GeFaise. (Self Reffection slop decddnn what node backtrack 1o)
True deFision So let's setting
Cra 15 Assi gn Faaee
Crn see 18.17 am saladied
Cluss 18 not salisted
Tris mearo our current exsignment is
Glause (52 (Hatee) (laton)) need
(Mistake:
baderracing)
motld. To sanety dause 18, at loast one
of
aare, T-uuue SnFaate Fa True True a-ie B-Faice, 2nialle. But 1 must be both True and Falze So this
path is Hmmm Let's backtrack further Maybe setting S-True was wrtnngg cholos, by setting
x10 Faise contrad cartior
True contredict
beliaten reteed Lat's backtrack where we net 10=Patee TwTrue BwFaten (Blasktrackingg Step
ad True contradicts.
no way to satisty siause 18 without
catisfed Cause by (Mistake: Unit propagation mastake
So setting anialte leads several
4mialee need Cause 18 salisted Xlrtlalls)
violating provious assignments.
Nltenatively maybe the formula is unsatistable. But need to check thoroughly. Let me check another path. Suppose instead of seating Falle what if set T0-True? (Baif Correction: Stop 20)
conflicting variables
already fized, satisfying assignment possible.
seems that every path try leads contradiction. Therefore original formula may be unsatisflable.
Figure Failure Cases: SAT-CNF traces for DeepSeek-R1 and GPT-4o. Although the input formula is satisfiable, both models incorrectly predict it as unsat. Colored boxes indicate model behaviors: cyan for heuristic variable selection, orange -- for mistakes, green... ... for backtracking, yellow for self-reflection, and violet for self-correction. Left branch always represents a True assignment. 1 marks unsatisfiability, and ? indicates an unexplored subtree. Integers are denoted variables (10 - X10) Numbers show the order of steps. The input formula is in CNF, where each list of integers represents a clause (e-g., [-9, 10, -7] + (-X9 V X10 V -X7)), and the full formula is a conjunction (A) of these clauses.
Tree search: R1 constructs and logically navigates a search tree. It maintains an awareness of its current position in the search space and builds upon previous decisions. Heuristic usage: R1 actively applies classical SAT-solving heuristics, including: (1) Unit Clause Elimination: Identifies and assigns values to literals that appear alone in clause
8

---

Published as a conference paper at COLM 2025
(2) Pure Literal Elimination: Searches for literals that appear with only one polarity across all clauses and assigns them accordingly. (3) MOMS (Maximum Occurrences in Minimum Size clauses) (Crawford & Auton, 1996; Hooker & Vinay, 1995): Prioritizes variables that occur most frequently in the smallest clauses. (4) Lookahead (Heule et al., 2012; Heule & Kullmann, 2017): Anticipates the downstream consequences of assignments before committing. (5) Unit Propagation: Deduces necessary assignments implied by current decisions and propagates them through the formula.
Backtracking: Upon encountering conflicts, R1 identifies the source of the inconsistency and backtracks. In many cases, it performs backjumping (i.e., jumping the most recent conflicting node) to return to the most recent cause of failure (Steps 9, 13).
Self-reflection: When conflicts arise, R1 engages in reasoning about why the contradiction occurred, revisits earlier decisions, and identifies the specific variable assignments that led to inconsistency.
Self-correction: R1 demonstrates the ability to recognize flawed strategies inconsistent outcomes, revise previous decisions, and explore alternative branches in the search space.
Overall, R1 seems to have learned the underlying logic of search and not just the style- unlike, GPT-4o which performs a greedy search without backtracking. We examined why R1 occasionally fails despite structured behavior, identifying key failure modes:
Incomplete. Despite initiating a structured search process, R1 often terminates prema- turely without fully exploring the search tree. Consequently, it fails to guarantee finding satisfying assignment even if one exists. This is depicted by in Figure 5.
Limited soundness. R1 sometimes generates logically inconsistent intermediate states by overlooking clauses (e.g., considering only 47 out of 48 clauses) or incorrectly handling variable assignments after backtracking (e.g., treating a previously unset variable as assigned in Step 11). This results in invalid reasoning states (Steps 3, 14 in Figure 5).
R1 uses human-like narration in its reasoning trace expressing internal dialogue, or narrative-style thinking. While this makes the trace more interpretable for humans, it introduces redundant and verbose explanations that do not advance the logical search.
We also analyze SAT-Menu traces in Figure 8 (Appendix) and observe that the search process is noticeably more unstructured compared to SAT-CNF. While R1 still displays many abovementioned behaviors such as tree search, heuristic application, backtracking, self-correction, and reflection, it struggles to map SAT-Menu inputs into structured CNF- like representations, which it could potentially handle more effectively. This limitation suggests that R1's reasoning ability is still closely tied to familiar input formats, and its generalization to more natural or abstract representations remains a challenge.
We find that R1's output tokens grow polynomially with input tokens (Figure 13, Appendix), unlike other LLMs whose outputs remain largely constant. This suggests that R1 adapts its reasoning depth based on input size aligning with theoretical work showing that polynomially many CoT steps can boost LLMs' reasoning power (Li et al., 2024). We hypothesize that merely training LLMs to produce longer CoT traces via next-token pre- diction may still encourage statistical patterns in learning rather than true reasoning as highlighted in Bachmann & Nagarajan (2024). In contrast, R1's improved performance may stem from reinforcement learning, which can guide models to develop coherent and goal-directed thought processes, rather than just mimicking token sequences (as evidenced by the performance difference between DeepSeek R1 and its base model V3, cf. Figure 3)
Discussion
In this section, we analyze the LLM performance by drawing analogies with SAT solvers and discuss the implications for the reasoning capabilities of LLMs.
Why are Easy regions easy? The reason why MiniSAT is capable of solving problems in the easy regions faster than problems around a, is due to the heuristics built into the solver that guide the search for satisfying solutions (e.g. unit propagation, MOMS). That is, heuristics work well when they can exploit statistical features in the problem instance to be solved.

---

Published as a conference paper at COLM 2025
LLMs, too, appear to perform well in these easy regions. However, this performance can be reinterpreted as statistical pattern matching rather than genuine reasoning. For example, LLMs may associate high number of input tokens with unsatisfiability an assumption that often holds for overconstrained formulas (see Appendix B). In such cases, the model is not solving the problem logically but reacting to superficial cues in the input.
a o
Why is the Hard region hard? Around the critical phase transition threshold (a,), known heuristics fail due to the complexity and combinatorial explosion of possible assignments inherent to NP-hard problems such as 3-SAT. As a result, solvers resort to exhaustive or extended search procedures. In this hard region, statistical patterns are weak or nonexistent, making heuristic guidance less effective.
Without statistical patterns, LLMs must rely on multi-step reasoning typically struggle. This aligns with Bottou's 's definition of reasoning. Specifically, these models struggle to compose known functions (such as variable selection, assignment, backtracking) into longer, novel reasoning chains that generalize beyond their training distribution. Similar observations have been made by Dziri et al. (2023) for function composition and by Zhang et al. (2023) for logical reasoning using BERT (Devlin et al., 2019).
- a task at which they
In contrast, R1 shows signs of having learned the underlying reasoning. Its ability to generalize to longer harder reasoning problems potentially outside its training distri- bution suggests a shift from pattern matching to structured search. While its reasoning process remains incomplete, this progress marks step-change in LLM reasoning abilities something that is not immediately apparent in standard reasoning benchmarks, which are increasingly saturated (cf., Figure 7 in Appendix). It opens up promising path, encouraging the community to build on its training recipe.
What if the tested models were trained on SAT data? We suspect that all models have likely encountered SAT data during pretraining. This is evidenced by their immediate use of terminology and strategies (e.g., DPLL, tree search, backtracking) when presented with SAT instances in CNF form. However, the core concern is not whether SAT-related content exists in the training data (which it likely does), but whether our specific evaluation is compromised by data leakage. We address this by considering two scenarios:
Exact data overlap. The strongest form of data leakage occurs when the evaluation set contains identical instances present in the model's training data. This scenario is highly unlikely in our case. We use a custom SAT data generator, and neither the data nor the generator was open-sourced before publication. This rules out direct memorization. In-distribution, but non-identical data. The most plausible scenario is that the evaluation data shares a distributional similarity with pretraining data. Even in this case, our evaluation results on the Hard region minimize reliance on shallow statistical patterns.
A third possibility is aut-of-distribution generalization, where models must rely on reason- ing rather than statistical shortcuts. This is consistent with prior work (Zhang et al., 2024; Dziri et al., 2023), which demonstrates that LLMs trained on reasoning tasks suffer sharp performance degradation under even modest distribution shifts when fitting on statistical patterns. We also highlight our SAT-Menu setup, where the problem is reframed as menu-based preference selection task. extremely unlikely that such a format appears in pretraining data, yet we still observe a clear performance gap between R1 and other models.
7 Conclusion
While R1 shows promising results in reasoning, it should be noted that our experiments were conducted on bounded 3-SAT problems with maximum of 10 variables and 110 clauses. In contrast, classical solvers can solve problems with thousands of variables with perfect accuracy. Moreover, RI still struggles in the hard region and its reasoning is neither perfectly sound (i.e. produces incorrect conclusions), nor complete (i.e. it cannot guarantee finding a solution). For better reliability and accuracy, it is advisable to use search scaffolds with LLMs, aligned with neurosymbolic techniques (De Raedt et al., 2020) recognizing the ability of LLMs as approximate idea adea-generators for problems as against directly solving them (Kambhampati et al., 2024) while invoking solvers for completeness (cf. Appendix C).
10

---

Published as a conference paper at COLM 2025
Acknowledgments
This work was supported by the Wallenberg Al Autonomous Systems and Software Pro- gram (WASP) funded by the Knut and Alice Wallenberg Foundation, by the EU H2020 ICT48 project "TAILOR" under contract #952215, and the KU Leuven Research Fund (C14/18/06) This research received funding from the Flemish Government (AI Research Program) and Flanders Research Foundation (G097720N). The resources and services used in this work were provided by the VSC (Flemish Supercomputer Center), funded by the Research Foun- dation Flanders (FWO) and the Flemish Government. We also thank Deepak Nathani, Holger Hoos, Heikki Mannila, Paolo Frasconi, Pascal Van Hentenryck, Ross King, Giuseppe Marra, Pieter Delobelle, Hendrik Blockeel, and Raffaele Marino for their valuable feedback.
References
Anthropic. Claude 3.7 sonnet and claude code. 2025. URL https://ww.anthropiccccc news/claude-33 3-a-udee-----nnet
Konstantine Arkoudas. Gpt-4 can't reason. arXiv, 2308.03762, 2023, URL https://api. smmarttiscch...rr...r///ooooooos wttg/CorppuID:26000111
semanticscholarr.
Gregor Bachmann and Vaishnavh V The pitfalls of next-token prediction. arxiv, 2403.06963, 2024. URL hts.ttttss//ppp...nnaiiccccchoor (raalarrorrr/rrpuuSS1/2222311111 http::/:........ttt....ooorrrooo
Béla Bollobás, Christian Jennifer T Chayes, Jeong Han Kim, and David B Wilson. The scaling window of the 2-sat transition. Random Structures Algorithmss 18(3):201-256, 2001.
Léon Bottou. From machine learning to machine reasoning: An essay. Machine learning, 94: 133-149, 2014.
Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared D Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel Ziegler, Jeffrey Wu, Clemens Winter, Chris Hesse, Mark Chen, Eric Sigler, Mateusz Litwin, Scott Gray, Benjamin Chess, Jack Clark, Christopher Berner, Sam McCandlish, Alec Radford, Ilya Sutskever, and Dario Amodei. Language models are few-shot learners. In Advances in Neural Information Processing Systems, volume 33, pp. 1877-190,, 2020. URL httpttss/////cceeeiie www.ddininnnnnnnnnneeeeeeeeee neurips. cccrips.cc/pppprr http:c/peeee.lles/pappppppeepp wwt.eessppppee//////// 1457c0d6bfcb49674
pdf..
Peter Cheeseman, Bob Kanefsky, and William M. Taylor. Where the really hard problems are. In Proceedings of the 12th International Joint Conference on Artificial Infelligence Volume 1, 1JCAI'91, pp. 331-337. Morgan Kaufmann Publishers Inc., 1991.
Cristian Coarfa, Demetrios D Demopoulos, Alfonso San Miguel Aguirre, Devika Subrama- nian, and Moshe Y Vardi. Random 3-sat: The plot thickens. In International Conference on Principles and Practice of Constraint Programminng, pp. 143-159. Springer, 2000.
James M Crawford and Larry D Auton. Experimental results on the crossover point in random 3-sat. Artificial intelligence, 81(1-2):31-57, 1996.
Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem- proving. Communications of the ACM, 5(7):394-3977 1962.
Luc De Raedt, Sebastijan Dumančić, Robin Manhaeve, and Giuseppe Marra. From statistical relational to neuro-symbolic artificial intelligence. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI-20, pp. 4943-4950, International Joint Conferences on Artificial Intelligence Organization, 7 2020. doi: 10.24963 ///3///iccii22000 24963/ijcai. 688. URL httt::://doi.rrg/// httt:s///ooooogg/...22666//iiii 1tt.6///.ca...22//6.... 2020/688. Survey track.
DeepSeek-AN Deepseek-rl: Incentivizing reasooiiiiiinnngnnnnnnnnnnn capability in llms via reinforcement 12948.
learning, 2025a. URL
11

---

Published as a conference paper at COLM 2025
DeepSeek-AL. Deepseek-v3 technical report, 2025b. URL /tt/tssss//aarivoogr///////11/1 19437.
Demetrios D Demopoulos and Moshe Y Vardi. The phase transition in the random hornsat problem. In Computational Complexity and Statistical Physics. Oxford University Press, 2006.
Jacob Devlin, Ming-Wei Wei Chang, Kenton Lee, and Kristina Toutanova. BERT:
Pre-training of deep bidirectional transformers for language understanding. In Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, Volume (Long and Short Papers), pp. 4171-4186. Association for Computational Linguistics, June 2019. doi: //aclan loy org/N19- E0//N19-144 1423.
URL https:
Jian Ding, Allan Sly, and Nike Sun. Proof of the satisfiability conjecture for large k. In Proceedings of the forty-seventh annual ACM symposium on Theory of computing, pp. 59-68, 2015.
Nouha Dziri, Ximing Lu, Melanie Sclar, Xiang (Lorraine) Li, Liwei Jiang, Bill Yuchen Lin, Sean Welleck, Peter West, Chandra Bhagavatula, Ronan Le Bras, Jena Hwang, Soumya Sanyal, Xiang Ren, Allyson Ettinger, Zaid Harchaoui, and Yejin Choi. Faith and fate: Lim- its of transformers on compasitionality. In Advances in Neural Information Processing Sys- tems, volume 36, pp. 70293-70332, 2023. URL /tll://ppprr/233/fff/////2222222
neurips cc/paper Cope .dff.
Niklas Eén and Niklas Sörensson. An extensible sat-solver. In International conference on theory and applications of satisfiability testing, pp. 502-518. Springer, 2003.
Lizhou Fan, Wenyue Hua, Lingyao Li, Haoyang Ling, and Yongfeng Zhang. Nphardeval:
Dynamic benchmark on reasoning ability of large language models via complexity classes, 2024. URL https: //tppis////xxx.oo// wwtp://wwww.w..//////bb1 14890.
Michael R. Garey and David S. Johnson. Computers and Intractability; A Guide to the Theory of NP-Complelenees. W. H. Freeman & Co., USA, 1990. ISBN 0716710455.
Michael R. Genesereth and Nils J. Nilsson. Logical foundations of artificial intelligence. Morgan Kaufmann Publishers Inc., 1987.
Google. Introducing gemini 2.0: Our new ai model for the agentic 2024.
era.
URL https://blog google-gemini-- apdatee-du-e-aeee decabterreecembe--222224
Rishi Hazra, Alkis Sygkounas, Andreas Persson, Amy Loutfi, and Pedro Zuidberg Dos Martires. REvolve: Reward Evolution with Large Language Models for Autonomous Driving, 2024a. URL htttp:://aati:i wwwpiiivvogg//bbe/s/eee barrg/bbs/2480 01309.
https///axxi..or///as//////////
Rishi Hazra, Pedro Zuidberg Dos Martires, and Luc De Raedt. SayCanPay: Heuristic Plan- ning with Large Language Models using Learnable Domain Knowledge. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 38, pp. 20123,20133, 2024b.
Marijn J. H. Heule and Oliver Kullmann. The science of brute force. Commun. ACM, 60(8): 70-79, July 2017. ISSN 0001-0782, doi: 10.1145/3107239, URL /ttps://doi..rrg/ 1145/ 3107239.
Marijn J. H. Heule, Oliver Kullmann, Siert Wieringa, and Armin Biere. Cube and conquer: Guiding edcl sat solvers by lookaheads. In Kerstin Eder, João Lourenço, and Onn Shehory (eds.), Hardware and Software: Verification and Testing, pp. 50-65. Springer Berlin Heidelberg, 2012.
John N Hooker and V Vinay. Branching rules for satisfiability, Journal of Automated Reasoning, 15(3):359-38) 1995.
Wenlong Huang, Pieter Abbeel, Deepak Pathak, and Igor Mordatch. Language models as zero-shot planners: Extracting actionable knowledge for embodied agents. In Proceedings of the 39th International Conference on Machine Learning, volume 162, pp. 9118-9147, 2022.
12

---

Published as a conference paper at COLM 2025
Albert Qiaochu Jiang, Sean Welleck, Jin Peng Zhou, Timothee Lacroix, Jiacheng Liu, Wenda Li, Mateja Jamnik, Guillaume Lample, and Yuhuai Wu. Draft, sketch, and prove: Guiding formal theorem provers with informal proofs. In The Eleventh International Conference Learning Represenlations, 2023. URL https: http///pppeeviieeeee
Subbarao Kambhampati, Karthik Valmeekam, L. Guan, Kaya Stechly, Mudit Verma, Sid- dhant Bhambri, Lucas Saldyt, and Anil Murthy. Llms can't plan, but can help planning in llm-modulo frameworks. arXiv, 2402.01817, 2024. URL https: / //api. semanticscholar,
org/CorpusID: ///CorpusSD::274131777 26741377.
Takeshi Kojima, Shixiang (Shane) Gu, Machel Reid, Yutaka Matsuo, and Yusuke Iwasawa. Large language models are zero-shot reasoners. In Ad- vances in Neural Information Processing Systems, volume 35, pp. 22199-22213, 2022. URL 8bb0d29
http://nnnn.rrriss..papppeerllra pdf.
Jean-Marie Lagniez and Pierre Marquis. An improved decision-dnnt compiler. In Proceedings of the Twentt-SSixth International Joint Conference Artificial Intelligence, IJCA1-17, pp. 667- 673, 2017. doi: 10.24963 /tt//////ccii1/1////// /93. URL https: /doi. org/10.
Zhiyuan Li, Hong Liu, Denny Zhou, and Tengyu Ma. Chain of thought empowers trans- formers solve inherently serial problems. In The Twelfih International Conference Learning Representations, 2024. URL https: httpr//wwww//ooomm/////////////
Hunter Lightman, Vineet Kosaraju, Yuri Burda, Harrison Edwards, Bowen Baker, Teddy Lee, Jan Leike, John Schulman, Ilya Sutskever, and Karl Cobbe. Let's verify step by step. In The Twoefft International Conference on Learning Representations, 2024. URL https: //openreview.o wtwp://wweettoornonii....... @pNGE0i.
B. Liu, Yuqian Jiang, Xiaohan Zhang, Qian Liu, Shiqi Zhang, Joydeep Biswas, and Peter Stone. Llm+p: Empowering large language models with optimal planning proficiency. arxiv, 2304.11477, 2023. URL https: http:/ppp...mmmnncccchhhlllll
Aman Madaan, Niket Tandon, Prakhar Gupta, Skyler Hallinan, Luyu Gao, Sarah Wiegreffe, Uri Alon, Nouha Dziri, Shrimai Prabhumoye, Yiming Yang, Shashank Gupta, Bodhisattwa Prasad Majumder, Katherine Hermann, Sean Welleck, Amir Yazdanbakhsh, and Peter Clark. Self-refine: Iterative refinement with self- feedback. In Advances in Neural Information Processing Systems, volume 36, pp. 46534- 46594, 2023. URL https: https://proceeddings wewrriiiiiinnnnnnisseeeeeeeeieee neurips. cc/paper Filles/paper22023/LIL. pdf.
William Merrill and Ashish Sabharwal. The parallelism tradeoff: Limitations of log-precision transformers. Transactions of the Association for Computational Linguistics, 11:531-545, 2023.
doi: 10.1162/tacl...005555 URL https:// https://aclaantholog hwwplloggyorggg2221 wwg./02g. tacl-1.31.
Stephan Mertens, Marc Mézard, and Riccardo Zecchina. Threshold values of random k-sat from the cavity method. Random Structures Algorithms, 28(3):340-373 2006.
Cristopher Moore, Gabriel Istrate, Demetrios Demopoulos, and Moshe Y Vardi. A continuous-disconimnouus second-order transition in the satisfiability of random horn-sat formulas. Random Structures & Algorithms, 31(2):173-185, 2007.
OpenAl. Gpt-4o system card. 2024. URL htttps://cdl stttp:://cdn.openai.. www/gottto--sssteeeeeeeeeo----ee pdf.
Binghui Peng, Srini Narayanan, and Christos Papadimitriou. On limitations of the trans- former architecture. arXiv, 2402.08164, 2024. URL https://api. wew.iisssmatticoooo.... org/ CorpusID:267636544.
Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi. Mathemati- cal discoveries from program search with large language models. Nature, 625(7995):
13

---

Published as a conference paper at COLM 2025
468-475 Jan 2024. ISSN 1476-4687. doi: 10.008//41155-00--099224 URL https:
//doi.org/11
Olivier Roussel. satgame/.
The SAT Game.
Stuart Russell and Peter Norvig. Artificial Intelligence: A Modern Approach. Prentice Hall, 3 edition, 2010.
Abulhair Saparov and He He. Language models are greedy reasoners: systematic formal analysis of thain-of-thought. In The Eleventh International Conference on Learning Representations, 2023. URL
Thomas J. Schaefer. The complexity of satisfiability problems. Proceedings of the Tenth Annual ACM Symposium on Theory of Computing, STOC '78, pp. 216-226, New York, NY, USA, 1978. Association for Computing Machinery. doi: 0111445/8001338044333 URL http://ooooorg/////////oo /145/800 33.354300.
Timo Schick, Jane Dwivedi-Yoe Roberto Dessi, Roberta Raileanu, Maria Lomeli, Eric Hambro, Luke Zettlemoyer, Nicola Cancedda, and Thomas Scialom. Toolformer: Language models can teach themselves to tools. In Advances in Neural Information Processing Systems, volume 36, pp. 68539-68551, 68551, 2023. URL http./tss/pprooeeenissseeeue/ neurips. cc/ secppppp.... files/ .df.
Bart Selman, David G Mitchell, and Hector J Levesque. Generating hard satisfiability problems. Artificial intelligence, (1(1-2):17-29 1996.
JP Marques Silva and Karem A Sakallah. Grasp-a new search algorithm for satisfiability. In Proceedings of International Conference on Computer Aided Design, pp. 200-2200222222 227.227.2 IEEE, 1996.
Charlie Victor Snell, Jaehoon Lee, Kelvin Xu, and Aviral Kumar. Scaling LLM test-time compute optimally can be more effective than scaling parameters for reasoning. In The Thirteenth International Conference on Learning Representations, 2025. URL https:// openreview.o new.e/ww.eeeeeeeeeeeeeeeeee pppereeieww.eetffouunnd------ /
Aarohi Srivastava, Abhinay Rastogi, Abhishek Rao, Abu Awal Md Shoeb, Abubakar Abid, Adam Fisch, Adam R. Brown, Adam Santoro, Aditya Gupta, Adrià Garriga-Alonso, Agnieszka Kluska, Aitor Lewkowycz, Akshat Agarwal, Alethea Power, Alex Ray, Alex Warstadt, Alexander W. Kocurek, Ali Safaya, Ali Tazarv, Alice Xiang, Alicia Parrish, Allen Nie, Aman Hussain, Amanda Askell, Amanda Dsouza, Ambrose Slone, Ameet Rahane, Anantharaman S. Iyer, Anders Johan Andreassen, Andrea Madotto, Andrea Santilli, An- dreas Stuhlmüller, Andrew M. Dai, Andrew La, Andrew Lampinen, Andy Zou, Angela Jiang, Angelica Chen, Anh Vuong, Animesh Gupta, Anna Gottardi, Antonio Norelli, Anu Venkatesh, Arash Gholamidavoodi, Arfa Tabassum, Arul Menezes, Arun Kirubarajan, Asher Mullokandov, Ashish Sabharwal, Austin Herrick, Avia Efrat, Aykut Erdem, Ayla Karakaş, B. Ryan Roberts, Bao Sheng Loe, Barret Zoph, Barttomiej Bojanowski, Batuhan Özyurt, Behnam Hedayatnia, Behnam Neyshabur, Benjamin Inden, Benno Stein, Berk Ekmekci, Bill Yuchen Lin, Blake Howald, Bryan Orinion, Cameron Diao, Cameron Dour, Catherine Stinson, Cedrick Argueta, Cesar Ferri, Chandan Singh, Charles Rathkopf, Chenlin Meng, Chitta Baral, Chiyu Wu, Chris Callison-Burch Christopher Waites, Chris- tian Voigt, Christopher D Manning, Christopher Potts, Cindy Ramirez, Clara E. Rivera, Clemencia Siro, Colin Raffel, Courtney Ashcraft, Cristina Garbacea, Damien Sileo, Dan Garrette, Dan Hendrycks, Dan Kilman, Dan Roth, C. Daniel Freeman, Daniel Khashabi, Daniel Levy, Daniel Mosegui González, Danielle Perszyk, Danny Hernandez, Danqi Chen, Daphne Ippolito, Dar Gilboa, David Dohan, David Drakard, David Jurgens, Debajyoti Datta, Deep Ganguli, Denis Emelin, Denis Kleyko, Deniz Yuret, Derek Chen, Derek Tam, Dieuwke Hupkes, Diganta Misra, Dilyar Buzan, Dimitri Coelho Mollo, Diyi Yang, Dong- Ho Lee, Dylan Schrader, Ekaterina Shutova, Ekin Dogus Cubuk, Elad Segal, Eleanor Hagerman, Elizabeth Barnes, Elizabeth Donoway, Ellie Pavlick, Emanuele Rodolà, Emma Lam, Eric Chu, Eric Tang, Erkut Erdem, Ernie Chang, Ethan A Chi, Ethan Dyer, Ethan Jerzak, Ethan Kim, Eunice Engefu Manyasi, Evgenii Zheltonozhski,, Fanyue Xia, Fate- meh Siar, Fernando Martinez-Plumed, Francesca Happé, Francois Chollet, Frieda Rong,
14

---

Published as a conference paper at COLM 2025
Gaurav Mishra, Genta Indra Winata, Gerard de Melo, Germán Kruszewski, Giambattista Parascandolo, Giorgio Mariani, Gloria Xinyue Wang, Gonzalo Jaimovitch-Lopez, Gregor Betz, Guy Gur-Ari, Hana Galijasevic, Hannah Kim, Hannah Rashkin, Hannaneh Ha- jishirzi, Harsh Mehta, Hayden Bogar, Henry Francis Anthony Shevlin, Hinrich Schuetze, Hiromu Yakura, Hongming Zhang, Hugh Mee Wong, Ian Ng, Isaac Noble, Jaap Jumelet, Jack Geissinger, Jackson Kernion, Jacob Hilton, Jaehoon Lee, Jaime Fernández Fisac, James B Simon, James Koppel, James Zheng, James Zou, Jan Kocon, Jana Thompson, Janelle Wingfield, Jared Kaplan, Jarema Radom, Jascha Sohl-Dickstein, Jason Phang, Jason Wei, Jason Yosinski, Jekaterina Novikova, Jelle Bosscher, Jennifer Marsh, Jeremy Kim, Jeroen Taal, Jesse Jesujoba Alabi, Jiacheng Xu, Jiaming Song, Jillian Tang, Joan Waweru, John Burden, John Miller, John U. Balis, Jonathan Batchelder, Jonathan Berant, Jörg Frohberg, Jos Rozen, Jose Hernandez-Orallo, Joseph Boudeman, Joseph Guerr, Joseph Jones, Joshua B. Tenenbaum, Joshua S. Rule, Joyce Chua, Kamil Kanclerz, Karen Livescu, Karl Krauth, Karthik Gopalakrishnan, Katerina Ignatyeva, Katja Markert, Kaustubh Dhole, Kevin Cimpel, Kevin Omondi, Kory Wallace Mathewson, Kristen Chiafullo, Kse- nia Shkaruta, Kumar Shridhar, Kyle McDonell, Kyle Richardson, Laria Reynolds, Leo Gao, Li Zhang, Liam Dugan, Lianhui Qin, Lidia Contreras-Ochande Louis-Philippe Morency, Luca Moschella, Lucas Lam, Lucy Noble, Ludwig Schmidt, Luheng He, Luis Oliveros- Colón, Luke Metz, Lütfi Kerem Senel, Maarten Bosma, Maarten Sap, Maartje Ter Hoeve, Maheen Farooqi, Manaal Faruqui, Mantas Mazeika, Marco Baturan, Marco Marelli, Marco Maru, Maria Jose Ramirez-Quintana, Marie Tolkiehn, Mario Giulianelli, Martha Lewis, Martin Potthast, Matthew I. Leavitt, Matthias Hagen, Mátyás Schubert, Medina Orduna Baitemirova, Melody Arnaud, Melvin McElrath, Michael Andrew Yee, Michael Cohen, Michael Gu, Michael Ivanitskiy, Michael Starritt, Michael Strube, Michat Swkedrowski, Michele Bevilacqua, Michihiro Yasunaga, Mihir Kale, Mike Cain, Mimee Xu, Mirac Suz- gun, Mitch Walker, Mo Tiwari, Mohit Bansal, Moin Aminnaseri, Mor Geva, Mozhdeh Gheini, Mukund Varma T, Nanyun Peng, Nathan Andrew Chi, Nayeon Lee, Neta Gur-Ari Krakover, Nicholas Cameron, Nicholas Roberts, Nick Doiron, Nicole Martinez, Nikita Nangia, Niklas Deckers, Niklas Muennighoff, Nitish Shirish Keskar, Niveditha S. Iyer, Noah Constant, Noah Fiedel, Nuan Wen, Oliver Zhang, Omar Agha, Omar Elbaghdadi, Omer Levy, Owain Evans, Pablo Antonio Moreno Casares, Parth Doshi, Pascale Fung, Paul Pu Liang, Paul Vicol, Pegah Alipoormolabashi, Peiyuan Liao, Percy Liang, Peter W Chang, Peter Eckersley, Phu Mon Htut, Pinyu Hwang, Piotr Milkowski, Piyush Patil, Pouya Pezeshkpour, Priti Oli, Qiaozhu Mei, Qing Lyu, Qinlang Chen, Rabin Banjade, Rachel Etta Rudolph, Raefer Gabriel, Rahel Habacker, Ramon Risco, Raphaël Millière, Rhythm Garg, Richard Barnes, Rif A. Saurous, Riku Arakawa, Robbe Raymaekers, Robert Frank, Rohan Sikand, Roman Novak, Roman Sitelew, Ronan Le Bras, Rosanne Liu, Rowan Jacobs, Rui Zhang, Russ Salakhutdinov, Ryan Andrew Chi, Seungjae Ryan Lee, Ryan Stovall, Ryan Teehan, Rylan Yang, Sahib Singh, Saif M. Mohammad, Sajant Anand, Sam Dillavou, Sam Shleifer, Sam Wiseman, Samuel Gruetter, Samuel R. Bowman, Samuel Stern Schoenholz, Sanghyun Han, Sanjeev Kwatra, Sarah A. Rous, Sarik Ghazarian, Sayan Ghosh, Sean Casey, Sebastian Bischoff, Sebastian Gehrmann, Sebastian Schuster, Sepi- deh Sadeghi, Shadi Hamdan, Sharon Zhou, Shashank Srivastava, Sherry Shi, Shikhar Singh, Shima Asaadi, Shixiang Shane Gu, Shubh Pachchigar, Shubham Toshniwal, Shyam Upadhyay, Shyamolima Shammie Debnath, Siamak Shakeri, Simon Thormeyer, Simone Melzi, Siva Reddy, Sneha Priscilla Makini, Soo-Hwan Lee, Spencer Torene, Sriharsha Hatwar, Stanislas Dehaene, Stefan Divic, Stefano Ermon, Stella Biderman, Stephanie Lin, Stephen Prasad, Steven Piantadosi, Stuart Shieber, Summer Misherghi, Svetlana Kiritchenko, Swaroop Mishra, Tal Linzen, Tal Schuster, Tao Li, Tao Yu, Tariq Ali, Tat- sunori Hashimoto, Te-Lin Wu, Théo Desbordes, Theodore Rothschild, Thomas Phan, Tianle Wang, Tiberius Nkinyili, Timo Schick, Timofei Kornev, Titus Tunduny, Tobias Gerstenberg, Trenton Chang, Trishala Neeraj, Tushar Khot, Tyler Shultz, Uri Shaham, Vedant Misra, Vera Demberg, Victoria Nyamai, Vikas Raunak, Vinay Venkatesh Ramasesh, vinay uday prabhu, Vishakh Padmakumar, Vivek Srikumar, William Fedus, William Saun- ders, William Zhang, Wout Vossen, Xiang Ren, Xiaoyu Tong, Xinran Zhao, Xinyi Wu, Xudong Shen, Yadollah Yaghoobzadeh, Yair Lakretz, Yangqiu Song, Yasaman Bahri, Yejin Choi, Yichi Yang, Yiding Hao, Yifu Chen, Yonatan Belinkov, Yu Hou, Yufang Hou, Yuntao Bai, Zachary Seid, Zhuoye Zhao, Zijian Wang, Zijie J. Wang, Zirui Wang, and Ziyi Wu. Beyond the imitation game: Quantifying and extrapolating the capabilities of
15

---

Published as a conference paper at COLM 2025
language models. Transactions on Machine Learning Research, 2023. ISSN 2835-8856. URL https://openreview.. www.leww.eefffrrrr net/forrum)dFuyTLLBBv
Kaya Stechly, Matthew Marquez, and Subbarao Kambhampati. GPT-4 doesn't know it's wrong: An analysis of iterative prompting for reasoning problems. In NeurIPS 2023 Foundation Models for Decision Making Workshop, 2023. URL https://openreview.nrr net/
forum?2d--PM2zjDYY68
Karthik Valmeekam, Alberto Olmo, Sarath Sreedharan, and Subbarao Kambhampati. Large language models still can't plan (a benchmark for LLMs on planning and reasoning about change). In NeuriPS 2022 Foundation Models for Decision Making Workshop, 2022. URL
https://openreview wtwpeeewwwwwweefrreeeeeee net/forumidd=wUU 5XTL5X0.
Xuezhi Wang, Jason Wei, Dale Schuurmans, Quoc V Le, Ed H. Chi, Sharan Narang, Aakanksha Chowdhery, and Denny Zhou. Self-consistency improves chain of thought reasoning in language models. In The Eleventh International Conference on Learning Repre- sentations, 2023. URL https:tp/////t /ttp:////pp//eeeeeeeeee net/forum? (artoorrrmmid1PPP 1=1PLL-IMMMPM
Jason Wei, Yi Tay, Rishi Bommasani, Colin Raffel, Barret Zoph, Sebastian Borgeaud, Dani Yo- gatama, Maarten Bosma, Denny Zhou, Donald Metzler, Ed H. Chi, Tatsunori Hashimoto, Oriol Vinyals, Percy Liang, Jeff Dean, and William Fedus. Emergent abilities of large language models. Transactions Machine Learning Research, 2022a. ISSN 2835-8856. URL net www.eee..etooommnin/eee/eo hett/Forumiddeyykku5zzz
https://openreviie
Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, brian ichter, Fei Xia, Ed Chi, Quoc V Le, and Denny Zhou Chain-of-thought prompting elicits reasoning in large language models. In Advances in Neural Information Processing Systems, volume 35, pp. 24824-24837, 2022b. URL httpps: neur cctpaper_fiiiiiieecee faaaprrfiles/ppper//200 hile/9d5609613524ecc -aaee htt
pdf.
Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. Naturalprover: Grounded mathematical proof generation with language mod- els. In Advances in Neural Information Processing Systems, volume 35, pp. 4913- 4927, 2022. URL https://proceeedings meure wwt.eeipp..cpppppeerreeeeeeeeeee 1fc548a8243ad066 6ee7
pdff.
Violet Xiang, Charlie Snell, Kanishk Gandhi, Alon Albalak, Anikait Singh, Chase Blagden, Duy Phung, Rafael Rafailov, Nathan Lile, Dakota Mahan, Louis Castricato, Jan-Phillpp Franken, Nick Haber, and Chelsea Finn. Towards system 2 reasoning in Ilms: Learn- ing how to think with meta chain-of-thought, 2025. URL httpttt://aaiiv.org/abbsss// 04682.
Shunyu Yao, Dian Yu, Jeffrey Zhao, Izhak Shafran, Tom Griffiths, Yuan Cao, and Karthik Narasimhan. Tree of thoughts: Deliberate problem solving with large language models. In Advances in Neural Information Processing Systems, volume 36, pp. 11809- 11822, 2023a. URL https://pproceedngss.eerrr neurips. httppppe...lee/pprr///////////// Confeernee..efernceeeeeooo pdf.
Shunyu Yao, Jeffrey Zhao, Dian Yu, Nan Du, Izhak Shafran, Karthik R Narasimhan, and Yuan Cao. React: Synergizing reasoning and acting in language models. In The Eleventh International Conference on Learning Representations, 2023b. URL https: http::://///eeeei..eeeeee net/ Brrumiid=wEEvluYU..
Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. SATLM: Satisfiability-aided language models using declarative prompting. Advances in Neural Information Processing Systems, 36, 2024.
Honghua Zhang, Liunian Harold Li, Tao Meng, Kai-Wei Chang, and Guy Van den Broeck. On the paradox of learning to reason from data. In Proceedings of the Thirty-Second International Joint Conference on Artificial Intelligence, IJCAI-23, pp. 3365-3370 8 2023. doi: 10.249 01.22463//jjee /tt///iaaa..22//31111 URL https: //ooi. http://oooooo/../////// 24963/ijcai 2023/375.
16

---

Published as a conference paper at COLM 2025
Hugh Zhang, Jeff Da, Dean Lee, Vaughn Robinson, Catherine Wu, Will Song, Tiffany Zhao, Pranav Raja, Dylan Slack, Qin Lyu, Sean Hendryx, Russell Kaplan, Michele, Lunati, and Summer Yue. A careful examination of large language model performance on grade school arithmetic. arviv, 2405.00332, 2024.
17

---

Published as a conference paper at COLM 2025
Appendix for "Have Large Language Models Learned to Reason? A Characterization via 3-SAT"
The appendix is organized as follows. Dataset Statistics S A, Output analysis of LLMs B, LLM + Solver integration ş C, and Full Prompts $ D.
Distribution clauses
Distribution a
Satisfiability
0.25
SAT
unSAT
0.20
0.15
20
0.05
0.00
UnSAT
12
Figure 6: 3-SAT Dataset Statistics. Figures depict clauses (left) and a (right) distribution across SAT and unSAT instances, highlighting that unSAT problems typically feature more clauses and higher values.
A Dataset Statistics
A.1
3-SAT
Table lists all values of the range of a corresponding to each n. For a values within the (6, interval, incremented by 1. For the [1, interval, which contains the most "interesting problems," " we aimed for finer granularity by choosing the smallest possible increment. This increment ensures that, given the number of variables n, we obtain an integer number of clauses m. For example, with n = 3, the minimum increment is & 1, and for 4, it is aine 0.25. For each &ine we generated 300 formulas.
The distribution of formulas according to the number of variables is detailed as follows: 3,000 formulas with variables, 7,500 with variables, 9,000 with 5 variables, 4,500 with variables, 3,000 with 7 variables, 13,500 with 8 variables, 3,000 with 9 variables, and 16,500 with 10 variables.
As shown in Figure 6, the range of clauses (m) varies in [5, 90], and the alpha (a m/n) ranges in [1.1, 11.0]. For unSAT instances, the clauses range from to 110, with the alpha varying in [2.60, 11.0]. Across the entire dataset, the average number of variables (n) is 7.2, the average number clauses (m) is 33, and the mean & is 4.7. This diverse dataset provides broad spectrum for analyzing the impact of variable and clause distribution on formula satisfiability.
A.2 2-SAT
For the experiments on 2-SAT, we followed the same formula generation procedure used for 3-SAT. However, the a range earlier in 2-SAT problems. This adjustment allowed us reduce the dataset size while preserving relevant data for analysis. For each value, detailed in Table 1, we generated 100 formulas. The resulting dataset comprises a total of 29,600 formulas, of which 4,860 are satisfiable.
reduced to [0), as the unsatisfiability transition occurs
18

---

Published as a conference paper at COLM 2025
Table 1: Table shows the range of alpha value for each n (i.e. number of variables) in the
generated dataset. We generate 300 formulas per value.
Range of a
10,,20,330,400,5,,,,,,0
9.0, 10.0, 11.0
1.0, 1,5,
2.75, 3.0,
4.0, 4.25, 4.5, 4.75, 5.0,
5.25, 5,,,5,,,,,,,,,,,,,,0,,,, 9.0, 10.0, 11.0
288, 3,,,,,,,,,, 40, 4.2, 44, 4.6, 4.8,
5.8, 6,0, 7.0, 8.0, 9.0, 10.0, 11.0
1.0, 45 1.0, 3.0, 4.0, 5.0, 6,,, 1.125, 1.25, 1.375, 1,5, 1,,, 1.65, 1.75, 1.875, 2.0, 2.125, 2.25, 2.375, 2.5, 2.625, 2.75, 2.875, 3.0, 3.125, 3.25, 3.375, 3.5, 3.625, 3.75, 3.875, 4.0, 4.125, 4.25, 4.375, 4.5, 4.625, 4.75, 4.875, 5.0, 5.125, 5.25, 5.375, 5.5, 5.625, 5.75, 5.875, 6.0, 8.0, 9.0,
6.0, 7.0, 8.0, 10.0, 11.0
9.0, 10.0, 11.0
10.0, 11.0
1.0, 2,0,3.0,,4, 6.0, 8.0, 9.0, 10.0, 11.0
10
2.4, 2.5, 2.6, 2.7, 2.8, 2.9, 3,0,31,,22,333 3.4, 3.6, 3.7, 3.,, 3.9, 4.0, 4.1, 4.2, 4.3, 4.4, 4.5, 4.6, 4.7, 4.8, 4.9, 5.0, 5,3,
1.7, 1.9, 2.0, 2.1, 2.2, 2.2,
54, 5.5, 5.6, 5.7, 5.8, 59, 6.0, 8.0, 9.0, 10.0, 11.0
Table 2: Configuration Parameters for LLMs
Model
Temperature
Top_p
Max Tokens
GPT-4o
0.3
16000
Claude 3.7 Sonnet
0.3
1
8192
Gemini 2.0 Flash
0.3
8192
DeepSeek V3
0.3
1
8000
DeepSeek R1
0.3
1
8000 (up to 32,000 for CoT)
A.3 Horn-SAT
We generate formulas for random 1-3 Horn SAT, following the methodology outlined by Moore et al. (2007). Intuitively, 1-3-HornSAT formulas contain clauses with only and literals and correspond to 3-SAT in the Horn category, which are P-complete rather than NP-complete.
Specifically, we sampled formulas from H2 dd and H3 O,ds distributions, where d was fixed to 0.5 to simplify the sampling space, and d2 and d3 (referred to as a) were varied to analyze formula behavior. For consistency with 2-SAT and 3-SAT analyses, a was incremented from 0 to 12 in steps of 1, resulting formulas. Notice that for = O, the formulas still contain 0.5n + clauses due to the fixed d parameter. The choice of d1 0.5 ensures different a values and small n. Lower values produced trivially satisfiable formulas at small n, for all a values, and were therefore avoided. We empirically explored dj values starting at 0.2 in increments of 0.1 before selecting 0.5.
an + 0.5n + clauses for these Horn
observe satisfiability threshold across
We generated 300 formulas for each value and formula type, with ranging from 3 to 10. This range aligns with our other experimental settings, as opposed to the significantly larger 20, 000 used by Moore et al. (2007). Each dataset contains 31,20N formulas. Among these, 5,036 formulas are satisfiable.
B LLMs as Solvers: Output Analysis
We observed the following behaviors in the generated outputs, including chain-of- thouugh (CoT) reasoning:
19

---

Published as a conference paper at COLM 2025
Benchmarks: DeepSeek Competitors
100
DeepSeek (mathematics)
Competitor (mathematics)
DrepSeek (coding)
Competitor (coding)
Performance
Claude 3.5 Sonnet
60
Gemini Flash
Claude 3.7 Sonnet
GPT-4o
40
Claude 3.5 Sonnet
Claude 3.7 Sonnet
20
MATH-500 (Pass@1)
MATH
GSMBK
MMLU-PP Pro
SWE- SWE-bench be-cch Verified
Aider- Paler-Pofyglat (Acc.)
BigCodeBench (Hard Set Completa)
Figure 7: Performance comparison of DeepSeek R1 with the next best LLM for math and coding benchmarks. The figure shows the narrow performance margin between models suggesting that benchmarks saturated. Sources: (DeepSeek-Al, 2025a; Anthropic, 2025; Google, 2024; OpenAI, 2024; DeepSeek-Al, 2025b)
Diverse Reasoning Techniques: LLMs employ varying reasoning techniques depending the prompt type (SAT-CNF vs. SAT-Menu) and even adapt their approach across individual problems within the same prompt type.
The dominant strategy involves backtracking, as illustrated Box 5. Occasionally, LLMs employ local search, where it assigns items to "orderable" and "not-orderable" lists and iteratively modifies these based on detected conflicts (e.g,, We can create two sets for liked and disliked items and then compare them to find any conflicts. Let's begin by creating list of all the likes and dislikes to identify conflicts.).
SAT-CNF Reasoning:
The primary strategy here is trial-and-erros Occasionally, LLMs apply heuristics such as the Maximum Occurrence Minimum-sizen clauses (MOMS) heuristic to prioritize variables appearing most frequently in the smallest clauses (e.g., We start by making a tally of how many people like or dislike each foch item... If we put 'macaron' on the 'orderable' list, we will salisfy many people who like it." ").
SAT-Menu Reasoning:
"Lazy" Solutions: As noted in subsequent text, LLMs often produce "lazy" solutions in many cases, either providing an outline of how solve the problem or asking be delegated solver.
We also discuss some interesting failure the SAT-CNF context, it was observed that LLMs, often opt to pass the task to an external SAT solver rather than solving it themselves. Additionally, when attempting to find solution, these models tend to provide only conceptual outline of the solution instead of concrete answer, a tendency that becomes more pronounced with larger formulas. When prompted explicitly for solution, LLMs might simplistically conclude that the problem is unsatisfiable due to its complexity, as shown in Box 4. Although this reasoning is not entirely sound over-constrained formulas that LLMs might be leveraging this as a statistical feature.
observed during our experiments. In
still potentially be solvable appears
In contrast, R1 always attempts to solve all problems. We discuss failure case of R1 for SAT-Menu input where RI finds a satisfying assignment even though none exists. We note interesting search-based behaviors shown in Figure 8.
20

---

Published as a conference paper at COLM 2025
Tao, likes carasal, zight?), Tal 14kea parsmel custard, dialiter braad
Dislited
Ting: Loser paiacs, sear. DENGERRR CREAmAL. RAEE: DHAD,
pialiken mialikin quacinale,
wait, lotta rechack all: (Bolf-correation)
mal: Liber pial lonad, caratel. 200. Likes guscamile,
Dialshes breed, EAR: Mixlthen rest. gelete, puscorole. burpery palate. Dialshen Tea7, Teo:
by seneicering
ose be placed people...
bread,
(luuiitti Unage: Mas
ceatard, ptalites bread. Gia: Libes cacanal. Dialiios sead, costard.
likes
Gialiten boaad. Libar gelato,
Azzusa nase is in not ordecable. Then: - Sacistied people dos to
maa bf burger, mielikes
nean being not orderation Haint, Lif, chao, dia, lany Ty, Riyh, Ell, Arun, Jay, Vic. stc, Koz, the people vbs like nean rting. Sisa, Do.
lie
Liber guacemsie, Dislibes custedd,
Raol, sty, quisco.
Ving!
seat, cuzcee. Dcaisoes cacamet. Ias: 15k0s culsto. ciziiies Seead. sieaael
astiotied.
bondd baoger, Ra
Atternatively, 1f naan is in arderable, Ric is estlefted becauss he
Libes cusn. le. y uue utber people sho hav depencmncias un noun,
biallten
lokes seeed. Dialiben
Litee nass. Bialixee curtans, Surger, de if naan orderable, satinfied. Houristic Usage: sootahiant:
scojec, cacanal. ElI: 2ihes crotard. Sialises seat, carenel.
Jay. quéciaclo.
Eurqus, dacanal. Arma
btalikee custars, meg: Zark: Lites
Lise cararal. Els,, dislthes naa iass codacable) and barger Surpes
gelato. wie tholihen breats golete, pacceoll
endersble. caramal not onderable. then aia
sear, bislikes burgers guaconole Bie tiker naary carow)).
aetiifiied (Nistake:
lis sirualy veliocied since saut
Deatiees burges.
de In son crderasin)
Well tikes custard, TF oxstard to orderable iffied.
dislikes breat conn orderable in rnd cinanel torsanel arderebl by do thet
ddazn's teigl.
reeds custard in cederable. Mistata: in step C. Ne:
gelato
hy's preferences:
nea contorterabll)),
crotard
set astizziedd Thscadoce. this approach falla. 20, adding custard to oriktable caupea D. to be
cederabie, Dat b0th
torderablel
orderable,
13
buuggrr
14
ieratiefind. do w need another way to satiety Mal
(Self Detlaction: Step
right not dieliker braad and cacars), besad is coderable, thin sattsfied, don't need contand arderable, cesolves the toose with Cr., coolf-correctiot]
bread
broad
14
caromak
canamol
(gelaso, Lurger,
12
14
cuslard
cuslard
Altorratio be plan burger net raile. Satal Raazok Vor fppp in step 13 Wille poter variatie amigeeass rensin fized.)
guacamale
guacamole
This seear cover avaryona. las's chacis-chack each paraon: Zaza: mean not orderable
orderable
14
Figure 8: Failure Cases:
SAT-Menu traces for DeepSeek-R1. Although the input formula is unsatisfiable, R1 incorrectly predicts it as satisfiable. Colored boxes indicate model behaviors: cyan for heuristic variable selection, orange - for mistakes, green ... for backtracking, yellow for self-reflection, violet for self-correction, and magenta for local search. Left branch always represents an assignment to the orderable list and vice versa. 1 marks unsatisfiability. Numbers show the order of steps.
C Can an LLM + Solver boost performance?
To aid LLMs in reasoning tasks, recent studies have explored pipelined approaches using LLMs to parse inputs into solver-compliant outputs, leveraging off-the-shelf solvers to derive the final answer (Ye et al., 2024; Liu et al., 2023). This approach aligned with neurosymbolic techniques (De Raedt et al., 2020), which combine the universal function approximation capabilities of neural networks with the precision of symbolic systems.
To explore a similar setting in the context of 3-SAT, we ask whether we can augment LLMs with an external solver wherein the LLM translates (astual)-natural language into a format that symbolic SAT solver, such as MiniSAT, can process. To this end, we prompt the LLM to translate 3-SAT formulas, which we provide in the SAT-Menu input format, into solver- compliant 3-SAT formulas. We then use 3-SAT solver to solve the translated instance (see Box 5 in Appendix). We dub this approach SAT-Translate and plot GPT-4 Turbo's performance in Figure 9.
We observe that when LLMs have access to an external solver, there is a significant increase in their accuracy, reaching at best, in GPT-4's case, x 100% across the entire range of We attribute this to the relatively lower computational complexity of translating 3-SAT formulas compared to solving them (i.e. finding satisfying assignments). Interestingly, we
21

---

Published as a conference paper at COLM 2025
GPT-4
1.0
SAT-Menu
SAT-ONF
SAT-Translate
10
Figure 9: The figure compares LLM-Modulo frameworks (denoted as SAT-Translate) here, GPT-4 Turbo equipped with a solver holver-withh with standalone GPTT4 using SAT-Menu and SAT-CNF inputs. Sra-laanslate approach (in green) outperforms the rest, showing the significance of augmenting LLMs with symbolic solvers.
find that varying the input format between SAT-CNF and SAT-Menu does not significantly enhance LLMs inherent reasoning capabilities. The marked improvement in performance primarily observed when they are equipped with external solver. While ours straightforward approach, one could also explore tighter integrations as proposed in LLM- Modulo frameworks (Kambhampati verifiers (Hazra et al., 2024b), recognizing the ability of LLMs as approximate idea-generators for problems as against directly solving them.
al., 2024) which augments LLMs with critics and
It should be noted that the input to the LLM is based on fixed templates, the rules of which can be captured using regular grammar. Thus, one could write a simple parser map the menu input to CNF formula. However, mapping from ambiguous natural language to solver-compliant input may be non-trivial for the LLMs. Generally, outputs from LLMs often require additional post-processing to meet specific guidelines.
22

---

Published as a conference paper at COLM 2025
D Full Prompts
Here, we provide full prompts used in our experiments for SAT-Menu (Box 2) and SAT-CNF (Box 3).
Box 2: SAT-Menu Prompt
System Message
Your task is to output two distinct lists food items, one denoting what can ordered ('orderable') and the other what cannot ('not orderable'), to meet the preferences a group of individuals. Each person must find the selection satisfactory based their likes and dislikes. SATISFACTION CRITERIA:
A person is satisfied if at least liked item in 'orderable' list one disliked item is in oroderbleaa list. 2. No item can appear on both lists. 3. All participants must be satisfied by the combination of the two lists. Importantly, if NO such combination exists that satisfies all, output empty lists for both. Check carefully before finalizing, You always think step-by-step and show all your work in the explanation. Output your final solution comma-separated list of strings in Python code (orderable = [..]], orderable [..]]]-
# Pairs of Preferences and Solutions for in-context learning
Few-shot Examples
Input for new problem
Preferences: Jay: Likes nachos, ratatouille. Dislikes pie. Ada: Likes pie. Dislikes burger, ravioli. Zoe: Likes ravioli. Dislikes pie, burger. Arun: Likes ratatouille. Dislikes pie, nachos. Ula: Likes ratatouille. Dislikes ravioli, nachos. Ying: Likes nachos, ratatouille. Dislikes burger.
Generated Solution for the given problem
Solution: First, let's list out the likes and dislikes of each person and then categorize the food items based on their preferences.
Jay: Likes nachos, ratatouille. Dislikes pie.
Ada: Likes pie. Dislikes burger, ravioli. Zoe: Likes ravioli. Dislikes pie, burger.
Arun: Likes ratatouille. Dislikes pie, nachos.
Ula: Likes ratatouille. Dislikes ravioli, nachos.
Ying: Likes nachos, ratatouille. Dislikes burger.
Now, let's categorize the items as 'orderable' and 'not orderable' based the given preferences.
From the above preferences, we can create the following lists:
Orderable: pie, ratatouille, nachos Not orderable: burger, ravioli
Let's examine if this combination satisfies all the participants preferences.
1. Jay: Satisfied by ratatouille in orderable list.
Ada: Satisfied by pie in orderable list.
3. Zoe: Satisfied by burger in notdordeealle list.
4. Arun: Satisfied by ratatouille in orderable list.
5. Ula: Satisfied by ratatouille in orderable list.
Ying:
Satisfied by nachos orderable list.
All participants are satisfied with this combination, and no item appears in both lists. So the final lists are:
python arderable= ratatouille, nachos] not not.orderable=-burger ravioli]
23

---

Published as a conference paper at COLM 2025
Box 3: SAT-CNF Prompt
System Message Let's play the SAT (satisfiabilitt) game. The input is a list of clauses, where each clause is represented as disjunction of literals (variables or their negation connected by logical OR). Your task is to find valuation of Boolean variables such that Boolean CNF formula evaluates True. The solution should be in form of dictionary where keys are variables and values are Boolean (True or False). SATISFACTION CRITERIA: 1. At least one literal each clause should be True. 2. A variable can't be both True and False the dictionary. 3. MOST IMPORTANTLY if NO satisfying assignment exists, you MUST output EMPTY dictionary. Check carefully before finalizing. You always think step-by-step and show all your work in the explanation. Output the solution in Python code dictionary, enclosed within (output ...).
# Input For new problem Formula:
[[ 3,1, 4,1 4, 2,1]. 1, 4, 5,4,2], 4,3,1], [1,5, -, 5, [4, -, -1, 1,,,, -3]]
# Generated Solution for the given problem Solution: To find satisfying assignment for this CNF (Conjunctive Normal Form) formula, we will use a simple approach and try construct solution iteratively while checking at each step if the clauses are satisfied or not. We will go through the clauses one by one and make arbitrary decisions on the truth values of the literals. We have to ensure that no variable is assigned both True and False, and each clause must have at least one True literal.
We start with the first clause [-3, 1, -4]. Let's arbitrarily decide: 3 is False (so -3 is True),
1 is True (so we satisfy the clause [-3, 1, -4] because is True or -3 is True),
4 is True (since
haven't t made any decision on 4, we do not yet satisfy the clause with -4, but that won't tt be an immediate issue).
Our current assignments are now: 1: True, 3: False, 4: True.
Next, we consider the second clause |-4, -2, Since is True, this clause is already satisfied.
Next is [-1, -4, 5]. We need to satisfy this clause without changing the truth value of or 4, so we choose to make 5 True.
Our assignments are now: 1: True, 3: False, 4: True, True.
Next, we look at [5, 1, 2]. Since 5 True, this clause is already satisfied.
Next [-5, 4, We need to satisfy this without changing or set to True.
Our current assignments are: 1: True, 2: True, 3: False, 4: True, True.
Now the next clause is [-4,3, 1J. 4 is True, -4 is False, but is True, so the clause is satisfied.
For the clause [1, 5, -3). This clause already satisfied by being True.
For [-2, 1, This clause is also satisfied because is True.
For [1, -5.4). This again satisfied because 1 True.
Next clause is -4,-3,11]. This clause is satisfied with 4 being True.
The last clause is [-2, 5.) This is satisfied because 5 is True.
All clauses are satisfied with our current assignments, so we return:
python output: {1: True, 2: True, 3: False, True, True)
24

---

Published as a conference paper at COLM 2025
Box 4: SAT-CNF (Lazy Solution)
System Message Let's play the SAT (satisfiabilitty game. The input is a list clauses, where each clause is represented as disjunction of literals (variables or their negation connected by logical OR). Your task is to find valuation of Boolean variables such that Boolean CNF formula evaluates True. The solution should be in form dictionary where keys are variables and values are Boolean (True or False). The satisfaction criteria are: 1. At least one literal in each clause should be True. 2. A variable can't be both True and False in the dictionary. 3. If no satisfying assignment exists, you should output an empty dictionary. You always think step-by -teppp and show all your work in the explanation. Output the solution in Python code dictionary, enclosed within coutput:...
# Input for new problem Formula:
-10)
==.6311||1.....11//../0222333313 [-,110
--1,-3,,44,,6,4- http--1||||1/////a00000003332333
Generated Solution for the given problem
Solution: To solve this satisfiability problem, need to determine assignment of truth values to the variables such that clauses are satisfied. With such large and complex problem, an efficient systematic approach or use of an algorithm like the DPLL Caavis-Putnam-Baee Loetaa--oogeaan-Loveeleee
algorithm would be ideal. However, since we're we're expected to think step- let's attempt simplified analysis.
We start by looking for unit clauses, which contain only one literal, or pure literals, which appear in one polarity only throughout the formula. Observing the clauses, we can't immediately spot such helpful shortcuts due to the complexity. Instead, through the clauses, and try to assign truth values the variables in way that satisfies as many clauses as possible. We might need to backtrack we reach contradiction.
iterate
We must make some initial choices and see if those choices can lead to consistent solution. Let's start with the first clause '7, -4]'. We begin by setting to True, 9 to True, or the negation of (-4) True. Let's decide to set 7 to True. This is an arbitrary choice the beginning, and we may need backtrack this leads to contradiction later.
Now, we need to check other clauses and see if this choice is consistent with them and try to fill in further values. We will need to iterate through each clause and see if it's possible to satisfy given our previous choices.
Given the complexity of the problem and the large number of variables and clauses involved, solving it by hand by step-by-step explanation impractical. In practice, would use SAT solver solver software find the satistying assignment, if one exists. SAT solver automatically handles the process of proposing variable assignments, backtracking, deducing necessary assignments based on the structure of the formula.
For the purposes of this answer, since I cannot that that solving this problem by hand unfeasible within this format. The output, given the complexity, cannot be determined without the use of algorithmic assistance. If no satisfying assignment exists (meaning the formula is unsatis tisfiable,, or we cannot solve it by a simple theoretical process within this framework, the output would be empty dictionary.
SAT solver in real-time, will have to
python
output: 0
25

---

Published as a conference paper at COLM 2025
(0-shot)
20 (O-ahot)
(D-ahot)
SAT becilion
SAT decidoon
SAT decitoo
MA4
Matta N
2 F S 2
Clacde 37 Scrnet (3-shot)
C0rEnI20PMAt (3-4hot)
0mT.4 (3-shot)
Deciaion
SAT beciton SIT SAarT
1/0
SIT
SAT Seares
SAT Seart
Figure 10: 0-shot vs. 3-shot accuracy. The figure compares 0-shot and 3-shot performance comparing all LLMs. It can be observed that in-context learning does not enhance perfor- mance in the hard region. The setup SAT-Menu. The plot was generated using size moving window values.
Box 5: SAT- Transslaee Prompt
System Message
You are provided with list of preferences from different individuals, each specifying items they like and dislike. Create logical expression Conjunctive Normal Form (CNF) that satisfies a set of individual preferences regarding likes and dislikes of certain items. The condition for an individual's satisfaction is that either at least one item they like is included, or at least one item they dislike is excluded in your selection. Format the final CNF expression in LaTeX. Ensure all item names are retained in the final output. Do not include any explanation.
# Input for a new problem Preferences: Om: Likes naan, curry. Dislikes tandoori. Bao: Likes curry. Dislikes naan, tandoori. Nic: Likes naan. Dislikes curry, tandoori. Pat: Likes curry. Dislikes naan, tandoori. Du: Likes tandoori, naan, curry. Kim: Likes curry. Dislikes tandoori, naan.
# Generated Solution for the given problem
Solution:
(naan V curry V -tandoori) ^ (curry V -naan V -tandoori) (naan -curry -tandoori)
(curry -naan V -tandoori) A (tandoori V naan V curry) (curry V -tandoorri V -naan)
26

---

Published as a conference paper at COLM 2025
10
0.6
0.6
scoumec
eccuracy
0.4
0.4
DeepSeck V3 V3-easy
DeepSeek: V3 V3-hard
DeepSeek Ri-easy
DeepSeek R2-hard
easy
Gemini 2.0 Flash-easy
Cemini 2.0 flash-harc
Claude Sonnet
0.0
Sonnet
0.0
6.1
0.2
0.3
0.4
0.5
0.7
0.0
0.1
0.3 satisfability ratlo
0.2
0.4
0.5
satisfabilitt ratto
0.8
0.8
0.6
accurscy
accuracy
DeepSeek V3-easy
DeepSeek V3-hard
R1-easy
DeepSeek Ri-hard
CPT-tn-eaky
GPT-to-hard
Gemini 2.0 Flash-easy
Gemini 2.0 Flash-harc Sonnet-hard
Claude Sannet-easy
0.0
0.1
0.2
0.3
0.4
0.5
0.5
0.7
0.0 0.1
0.2
0.3
0.4
0.5
sabisfiability ratin
salisfabillly sallo
Figure 11: Accuracy vs. satisfiability ratio. R1 maintains consistent accuracy regardless of satisfiability ratio. In contrast, the performance of other LLMs is impacted by the number of satisfying assignments more the satisfying assignments, higher the performance. The first row for SAT-Menu and the second row is for SAT-CNE, We only include satisfiable instances and analyze easy (dashed line) and hard regions (solid line) separately.
27

---

Published as a conference paper at COLM 2025
Gemini Flash
UCCA
LIGHT
Presices
0.48
0.90
0.34
0.44
Actual
Actual
Cloude 3.7 Sonnet
SeepSeec V3
3.0J
0.72
0.77
0.39
Ridiited
S4
VIGTT
SÀT
unis"
DecaSeck R1
Prodiced
k
0.06
0.83
Actial
Figure 12: Confusion matrices for the decision version of 3-SAT. It can be observed that, except R1, all other LLMs struggle to correctly classify unsatisfiable instances. This suggests that R1 is more sound (detects sat/un iut/unsat correctly) than complete (cannot guarantee to find a solution). The cell annotations reflect classification accuracy, normalized over the true counts (column) to account for the imbalance between SAT and unSAT instances. The setup SAT-Menu with 0-shot prompting.
28

---

Published as a conference paper at COLM 2025
GPT-40
Gemini 2.0 Flash
Uneer 8 000
Quadrabic R5-0.005
3000
Cubic RF-0.015
2500
8 Quipue toleens
2000
Uneer R7-0.120
Quadratt: Riun 166 Cuelc 81-0.168
1500
1000
2000
:00
6/0
.300
400
500
700
input tokens
inggut tokeis
DeepSeek
R--01144
7000
6000
oultp. todens
2000
+utpput
2000
2000
1000
1000
DeepSeek R.
20000
Uieer RI-C 639
Qundratic 0.0
Cublc R1-0.673
17500
15000
culppc: t5keers
3000
2520
300
400
500
600
700
Input tokeris
Figure 13: Correlation between output (generated) and input tokens. R1 output tokens grows polynomially with the input tokens. In contrast, the generated tokens of other LLMs remain largely unchanged.
29


Reviews:
[{"review_id": "VirVvuyRZB", "reviewer": "Reviewer_YUcH", "summary": "This paper test if LLMs reason genuinely like human or answer questions with shortcuts. To do that, the authors select the 3-SAT questions for the evaluation. Results show that performance of LLMs drops significantly when the question becomes difficult, indicating the shortcut manners. While R1 shows the manner of performing real reasoning.", "questions": "", "limitations": "", "rating": 6, "confidence": 4, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "1. The research question is important. Researching the reasoning manners is helpful to understand the limitations and strengths of reasoning models (e.g., R1), which could be inspiring for the further improvement.\n\n2. The evaluation task is suitable. 3-SAT questions are NP-complete, which might be helpful to alleviate the shortcut issues when testing reasoning ablitiy.", "reasons_to_reject": "My main concerns are about the experiment setting and the performance interpretation.\n\n1. In previous work that research the limitation of transformer architectures, the researched models are not pretrained models, since the pretraining corpus and training processes are not that clean. The data leaky may happen and this would influence the final evaluation performance. However, in this work, the authors research the limitations mainly for pretrained models, which inevitably encounters this issue. It's not very convincing to connect the evaluation results with the real reasoning ability under this condition.\n\n2. Based on the reported performance (e.g., Figure 3), it's not very obvious to conclude that R1 are more like true reasoning. The tendency is similar to those of other LLMs, and the performance gap between it and other models is roughly stable. Besides, some case study without statistical support is still not sufficient to prove the advantage of reasoning models w.r.t. the LLMs.", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "wfW9R8zbyS", "reviewer": "Reviewer_ApVz", "summary": "This paper investigates the reasoning ability of large language models (LLMs) by evaluating their performance on 3-SAT problems, a well-established problem in complexity theory. The paper compares the models’ performance under two problem presentation modes (SAT-CNF and SAT-Menu) and two task types (SAT Decision and SAT Search). Results are compared with the known satisfiability threshold of random 3-SAT. The paper contributes to understanding how LLMs perform on complex reasoning tasks and explores their capabilities in problem-solving.", "questions": "", "limitations": "", "rating": 6, "confidence": 1, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "1. The paper explores an interesting and original approach by applying LLMs to complex combinatorial problems (3-SAT), which is significant for understanding the reasoning capabilities of these models.\n2. The paper clearly defines the task, using well-established benchmarks like 3-SAT to evaluate LLMs, providing clarity in the experimental setup and comparisons.\n3. The analysis of how different modes of presenting SAT problems to LLMs affects their performance is valuable, especially considering the growing interest in using LLMs for complex problem-solving.", "reasons_to_reject": "Drawing the conclusion that “Large Language Models have Learned to Reason” solely based on 3-SAT problems seems a bit far-fetched. I hope the authors can use a more appropriate phrasing.", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "EudVHGgMLT", "reviewer": "Reviewer_r8DN", "summary": "The authors present a detailed study of modern LLMs performance on a 3-SAT benchmark. By varying the complexity\nlevel of problem instances, the authors demonstrate the dependence of accuracy of Deepseek R1, GPT-4o, Claude Sonnet and Gemini 2.0 Flash models on the hardness of the instance. Also, the authors attempt to analyze reasoning patterns of tested models. The manuscript describes similar experiments for 2-SAT and HornSAT problems.", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "1. The paper is well written, the authors provide a good conceptual introduction to the problem.\n2. Experimental data is convincing\n3. The authors try to explain reasoning process of different LLMs.", "reasons_to_reject": "1. Although the implementation of this study is quite good, the idea is not novel. Several works presented benchmarks for LLMs based on problems from different computational complexity classes. Specifically, https://openreview.net/pdf?id=mHx8JFURtn proposed a benchmark based on recursive problems from P class and https://arxiv.org/abs/2312.14890 proposed multiple benchmarks based on P, NP-complete and NP-hard problems, to name a few. The authors should improve the overview of the existing works.\n2. The authors do not go beyond simple model prompting, although there are multiple test-time techniques to improve LLM reasoning (Tree-of-Thought, Program-of-Thought etc). Comparing the performance of reasoning models to at least one of these techniques is important to understand the weaknesses of current models.", "questions_to_authors": "1. How many answers did you generate per problem instance? Can you provide estimates of the standard deviation for the curves in Figure 3, for example?\n2. Did you perform any analysis of reasoning traces beyond empirical evaluation? For example, can you compare the frequency of SAT heuristics use by DeepSeek R1 and GPT-4o?", "extra_scores": {}}, {"review_id": "s5TpQgmQnR", "reviewer": "Reviewer_jBva", "summary": "This paper studies the reasoning capabilities of LLMs through the lens of 3-SAT problems, leveraging the well-established phase transition behavior of 3-SAT as a proxy for problem hardness. The authors test multiple SOTA LLMs on both structured CNF representations and natural language (SAT-MENU) encodings of 3-SAT instances in decision and search formats. A key finding is that DeepSeek R1 shows behavior resembling symbolic reasoning, outperforming others in hard regions.", "questions": "", "limitations": "", "rating": 6, "confidence": 3, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "* The paper makes a rigorous attempt to operationalize \"reasoning\" by aligning it with search over NP-complete problems, providing a theoretical and empirical framework that stands out from benchmark-driven approaches.\n* The study is timely and of significant interest to the NLP community, especially those working on LLM reasoning.\n* Qualitative trace analyses provide insights into whether models internally simulate symbolic search strategies.", "reasons_to_reject": "* While the setup is grounded in complexity theory, there’s no formal analysis connecting transformer architecture limitations to the observed empirical behavior. The use of complexity class boundaries is insightful but not fully exploited.\n* While R1 outperforms other models, there is insufficient ablation to isolate whether the improvement comes from architecture, training data, RL fine-tuning, or test-time compute. The attribution is largely speculative.", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: The paper investigates whether large language models are able to truly reason or instead rely on shortcuts by evaluating their performance on 3-SAT problems. Experimental results indicate that performance drops as problem difficulty increases. Based on the results, the authors notice that DeepSeek R1 may showcase behavior that is close to symbolic reasoning, while other models do much worse for harder instances. The reviewers appreciated the research question and experimental design. The reviewers also raised concerns about data leakage from pretrained models and the clarity of claims regarding genuine reasoning. The authors clarified that direct data overlap is unlikely due to custom data generation, and that focusing on hard 3-SAT instances reduces reliance on superficial patterns. The authors also noted that R1’s performance is stable across complexity classes and supplemented empirical results with qualitative analysis of reasoning traces. Reviewers suggested more nuanced language and a stronger overview of related work, to which the authors responded by emphasizing their focus on evaluating native reasoning rather than attributing improvements to specific factors. The authors added confidence intervals to figures to address statistical concerns and agreed to clarify claims and limitations in the revised manuscript. Overall, the reviewers and the area chair found the work valuable and well-executed but recommended additional work, which the authors committed to addressing in the final version of the manuscript. The reviewers seemed satisfied with the authors’ responses and maintained their positive evaluations. The area chair would like to second the reviewers’ comments and suggestions to nuance the conclusions. In particular, the term “characterization:” in the title and in the text may be a bit too strong; “investigation” may be more appropriate here.
Decision: Accept