Can Large Language Models Reason? A Characterization via 3-SAT

## Abstract

Abstract Large Language Models (LLMs) have been touted as AI models possessing advanced reasoning abilities. However, recent works have shown that LLMs often bypass true reasoning using shortcuts, sparking skepticism.
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 LLMs by varying the inherent hardness of the problem instances. Our experimental evidence shows that LLMs are incapable of performing true reasoning, as required for solving 3-SAT problems. Moreover, we observe significant performance variation based on the inherent hardness of the problems – performing poorly on harder instances and vice versa. Importantly, we show that integrating external reasoners can considerably enhance LLM performance. By following a principled experimental protocol, our study draws concrete conclusions and moves beyond the anecdotal evidence often found in LLM reasoning research.

## 1 Introduction

The success and versatility of Large Language Models (LLMs) have sparked widespread interest and debate on whether LLMs are capable of reasoning.
The answer to this question may depend on the perspective on reasoning one takes, whether it is more oriented toward common sense reasoning (Davis & Marcus, ) or towards logical or deductive reasoning (Genesereth & Nilsson, ). We will adhere to Leon Bottou’s definition, which defines reasoning as “*algebraically manipulating previously acquired knowledge in order to answer a new question*” (Bottou, ). This is aligned with Russell and Norvig’s description of artificial intelligence as rational thinking (Russell & Norvig, ).

Recent studies suggest that LLMs are inherently capable of zero-shot reasoning (Kojima et al., ) (i.e. performing multistep inference processes in previously unseen situations). This ability has been shown to *emerge* and improve with scale (Wei et al., ; Srivastava et al., ), and can be further enhanced by using smart prompting techniques that encourage LLMs to think step-by-step (Kojima et al., ; Wei et al., ; Zhou et al., ; Yao et al., ; Prasad et al., ). Demonstrations include, inter alia, planning (Huang et al., ; Ahn et al., ; Singh et al., ; Liang et al., ; Huang et al., ; Hazra et al., ), theorem proving (Jiang et al., ; Welleck et al., ; Yang et al., ), search and optimization (Yang et al., ; Romera-Paredes et al., ; Hazra et al., ), self-reflection (Yao et al., ; Madaan et al., ; Shinn et al., ), and tool usage (Shen et al., ; Schick et al., ).

Conversely, a growing body of research presents a more critical view of these emergent abilities. For instance, LLMs may exhibit limitations in consistent logical reasoning (Arkoudas, ; Saparov & He, ), effective planning (Valmeekam et al., ), and accurate self-evaluation of their outputs (Stechly et al., ). During training, language models can fit on statistical features (Zhang et al., ) or identify reasoning shortcuts, much like the *Clever Hans Cheat* (Bachmann & Nagarajan, ), thus bypassing true reasoning. There is also growing concern about dataset contamination(^1^11Data closely resembling the benchmark leaks into the training data.) from open-source benchmarks (Zhang et al., ) that can inflate the reasoning performance of LLMs.
During inference, the autoregressive nature of LLMs makes them prone to snowballing errors over time (Dziri et al., ). Furthermore, these models can often generate unfaithful and biased explanations in their chains of thought (Turpin et al., ). Additionally, their greedy approach to reasoning often falls short in contexts with multiple valid reasoning steps (Saparov & He, ). On the architectural side of LLMs, findings reveal that the transformer layer is incapable of function composition for large domains (Peng et al., ; Dziri et al., ). From a theoretical standpoint, transformer computations have been shown to lie in the complexity class log-uniform TC^0, which is too restrictive even for simple logical reasoning tasks such as 2-SAT(^2^22More specifically, TC^0 is more restrictive than the logarithmic memory class L (Papadimitriou, , Chapter 16), (Merrill & Sabharwal, ). Given that the 2-SAT problem is NL-complete (i.e., the class of non-deterministic logarithmic space algorithms), multi-layer transformers cannot solve 2-SAT instances, unless L$=$NL (Peng et al., ).). Given these limitations, it has been suggested that the emergent abilities are but a mere *mirage* stemming from the choice of metric (Schaeffer et al., ).
This inevitably leads to the question: \sayCan Large Language Models reason? And if so, to what extent? We answer these questions via the following contributions.

Figure: Figure 1: The 3-SAT problem, visualized using a variant of the SAT game (). In SAT, one must return a truth assignment to Boolean variables that satisfy a Boolean formula in conjunctive normal form (CNF) if one exists, and return unSAT otherwise. A row in the visualization represents a clause, which is a disjunction (connected by a logical OR $\lor$) of literals, wherein a literal can be positive ($X_{1}$) or negative ($\neg X_{1}$). An assignment satisfies a clause if one of its literals is assigned the value true. Since clauses are conjunctively connected (by a logical AND $\land$), all clauses must be satisfied for the formula to be satisfied. If no satisfying assignment exists, the formula is unsatisfiable.
Refer to caption: extracted/5947246/plots/sat_game.png

(1) Characterizing LLM-reasoning from a computational theory perspective. Adhering to Leon Bottou’s definition of reasoning, we propose an experimental framework centered on 3-SAT, to evaluate reasoning. The choice of 3-SAT, introduced in Figure 1, is not arbitrary – being a foundational problem in computational complexity, many reasoning problems in AI like logical reasoning, planning, and constraint satisfaction can be reduced to 3-SAT. This approach provides a more formal and robust evaluation of reasoning compared to common benchmarks, which only superficially capture reasoning abilities (Hendrycks et al., ; Chen et al., ; Hendrycks et al., ; Rein et al., ). Additionally, it bridges classical computational theory with modern AI, allowing us to assess if LLMs go beyond pattern recognition and exhibit true reasoning capabilities grounded in complexity theory.

(2) Studying Phase Transition Characteristics of LLMs. We investigate the phase transition characteristics of LLMs (Cheeseman et al., ) – i.e., how LLMs’ performance varies in the easy and hard regions of the problem space. This contrasts with commonly used reasoning benchmarks, which often evaluate LLMs without considering the performance variations based on *inherent hardness* of the problems.

(3) Comprehensive evaluation of state-of-the-art open-source and proprietary LLMs. We conducted extensive experiments across a range of state-of-the-art open-source LLMs, as well as proprietary LLMs. While we find that LLMs generally cannot reason, their performance varies significantly in different regions of problem space (i.e. phase transition characteristics), with GPT-4 significantly outperforming other models. Additionally, we demonstrate how integrating LLMs with external verifiers, such as in the LLM-Modulo Frameworks (Kambhampati et al., ), can enhance reasoning capabilities and improve performance on 3-SAT problems.

Figure: Figure 2: Random 3-SAT Phase Transitions (Cheeseman et al., ). Plotted in red is the probability of a randomly sampled 3-SAT formula being satisfied against the hardness $\alpha$ of the formula. We can observe a clear phase transition occurring at $\alpha_{c}\approx 4.267$ (marked by the green dotted line). We identify two easy regions, one on either side of $\alpha_{c}$. 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 one (left) or zero (right). The solid blue line shows the mean time taken by the MiniSAT solver (Eén & Sörensson, ) to solve a 3-SAT instance. Notably, there is a spike in the solver’s runtime near the critical $\alpha_{c}$ value. This is attributed to the absence of useful heuristics in this region, forcing the solver to resort to essentially exhaustive searches.
Refer to caption: x1.png

## 2 Preliminaries

### 2.1 Phase Transitions in Random 3-SAT

We study the reasoning capabilities of LLMs on random 3-SAT problems.
3-SAT constitutes one of the most fundamental problems in computer science as it is the prototypical NP-complete problem, lying at the foundation of computational complexity theory.
Moreover, various prevalent reasoning problems in artificial intelligence, such as planning and constraint satisfaction, can be reduced to solving 3-SAT problems (Garey & Johnson, ).

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 a *phase transition* in random 3-SAT problems (Cheeseman et al., ). When randomly sampling 3-SAT formulas, one can observe a sharp change in the probability of a 3-SAT formula being satisfiable when plotted against $\alpha=\nicefrac{{m}}{{n}}$, where $m$ is the number of clauses and $n$ is the number of variables. For random 3-SAT, this phase transition occurs at $\alpha_{c}\approx 4.267$ (Mertens et al., ; Ding et al., ), i.e. the point at which a 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 neighbourhood of the threshold (Hard), and the over-constrained region above the threshold (Easy), cf. Figure 2.

### 2.2 SAT Solvers

SAT solvers are tools to automatically verify the satisfiability of propositional logic formulas. The Davis–Putnam–Logemann–Loveland (DPLL) algorithm (Davis et al., ) is a key component of modern SAT solvers. It consists of a backtracking-based search algorithm, enriched with deductive rules and heuristics, to efficiently explore the search space and determine whether a formula is satisfiable. The core backtracking algorithm simply selects a literal and assigns a truth value to it. This step produces a simplified formula where all the parts made true by the assignment are removed. This step can be applied recursively until all clauses are removed, meaning that the original formula is satisfiable. In Figure 2 we show how the time to determine the satisfiability of a random 3-SAT formula varies in function of $\alpha$. Most prominently, we see a pronounced peak in time-to-solution around the $\alpha_{c}$.

Analogously to characterizing SAT solvers by their behavior on solving problems with varying $\alpha$, we study the reasoning capabilities of LLMs with respect to the phase transition in random 3-SAT problems.(^3^33A thought experiment in the same vein was also proposed by Kambhampati et al. ()). This contrasts with other works that characterize reasoning by evaluating performance on benchmark datasets (Cobbe et al., ; Hendrycks et al., ).

## 3 Related Work

Existing works have focused on improving the reasoning abilities of LLMs by combining them with verifiers and heuristics (Olausson et al., ; Liu et al., ; Lightman et al., ). In terms of solving SAT problems with LLMs, SATLM (Ye et al., ) proposes a satisfiability-aided language modeling using an LLM to parse an NL SAT input to a SAT problem specification which consists of a set of logical formulas, then obtain the solution by invoking a SAT solver. Similarly, AutoSAT (Sun et al., ) uses LLMs to optimize heuristics in SAT solvers. Our goal is *not* to build 3-SAT solvers powered by LLMs. On the contrary, we use the 3-SAT phase transition to assess the reasoning abilities of LLMs using a well-established experimental protocol.

Closest to our work is the NPHardEval Fan et al. (), which examines reasoning across various computational complexity classes, but we additionally explore phase transition characteristics and investigate how the performance varies with *inherent hardness* of problems. Moreover, our evaluation centers on the 3-SAT, a classic NP-complete problem known for its distinct phase transition characteristics, providing a clear framework for analyzing reasoning depth.

## 4 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 as SAT-Menu. As shown in Box 4.1, the prompt input to the LLM consists of a task outline, along with a specific scenario detailing the dietary preferences of a set of people. The LLM’s objective is to identify a 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 4.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 (CoT) (Wei et al., ) and in-context learning (Brown et al., ) (see Box C in Appendix for the full prompt).

Additionally, we introduce a second problem formulation where the LLM is directly given the underlying 3-SAT formula in 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 C in the Appendix.

To assess the reasoning capabilities of LLMs, we analyze their performance on two variants of the 3-SAT problem. The first variant is the 3-SAT Decision problem, where the LLM acts as a solver and must determine whether a given 3-SAT problem is satisfiable. If the problem has a satisfiable assignment, the LLM should respond with \sayyes and with \sayno if it is unsatisfiable. The second variant is the 3-SAT Search problem, where the LLM’s task extends beyond providing a simple \sayyes or \sayno response. If the formula is satisfiable, the LLM should also return an assignment to the variables that satisfies the formula. However, if the formula is found to be unsatisfiable, the LLM should once again respond with \sayno.

Due to the widespread adoption and best-in-class performance(^4^44[https://huggingface.co/spaces/lmsys/chatbot-arena-leaderboard](https://huggingface.co/spaces/lmsys/chatbot-arena-leaderboard))
we use GPT-4 Turbo (specifically, GPT-4 1106-preview model) as the main LLM reference to perform our experimental evaluation.
However, we also report extended comparisons of GPT-4 to additional state-of-the-art LLMs, including both open-source (Llama 2 70B chat-hf (Touvron et al., ), Mixtral $8\times 7$B (Jiang et al., )) as well as proprietary models (GPT-3.5 Turbo (OpenAI, ), Gemini 1.0 Pro (Google, ), PaLM 2 text-bison (Anil et al., )). The open-source models were run on 4 NVIDIA-DGX A-100 GPUs using a distributed (model parallel) framework. The generation configurations are listed in Appendix Table 2.

To verify the LLM-generated solutions for both SAT-Menu and SAT-CNF, we employed MiniSAT v2.2 (Eén & Sörensson, ) solver.

### 4.2 Dataset Generation

To generate 3-SAT data, we varied $\alpha=m/n$ as a parameter to guide the generation process. For each $n\in[1,10]$, we selected $\alpha\in[1,11]$ based on feasible values of $m$. The full range of values is provided in Table 1 in the Appendix. Each instance is labeled either as satisfiable or unsatisfiable using MiniSAT v2.2 (Eén & Sörensson, ). Additionally, each instance is annotated with model count (i.e. number of feasible solutions for a formula) using the D4 model counter (Lagniez & Marquis, ).

For SAT-Menu setup, we map each instance (i.e. CNF formula) to a menu selection puzzle. The goal is to select a combination of orderable and non-orderable food items in a way that satisfies everyone’s preferences. To this end, a 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. This approach is exemplified in Box C.

Our dataset consists of 60,000 formulas, among which 39,909 are satisfiable (SAT) and the remaining 20,091 are unsatisfiable (unSAT) instances. For our experiments, we randomly selected approximately 6,000 samples from this pool. Detailed statistics of our data distribution are provided in Appendix A.

## 5 Results

Figure: Figure 3: Accuracy of GPT-4 against $\alpha$ and the satisfiability ratio. [Left] Accuracy of GPT-4 against $\alpha$ for both SAT Decision and SAT Search. Notably, GPT-4’s accuracy for both variants exhibits a significant decline around the critical point ($\alpha_{c}\approx 4.267$) aligning with the hard region. The dip in the performance mimics the increased solving time of the MiniSAT solver in the hard region. The setting is SAT-CNF. [Right] Accuracy of GPT-4 against the satisfiability ratio. We only include satisfiable instances and analyse problems from the hard and easy regions separately. Note that in our dataset, the 3-SAT problems exhibited maximum satisfiability ratios of approximately $0.4$ for the hard region and $0.62$ for the easy regions. The plots were generated using a size 4 moving window on $\alpha$ values.
Refer to caption: x2.png

Figure: Figure 4: Comparing GPT-4 with SOTA LLMs. [Left] Phase transition characteristics for all LLMs. [Right] Comparison of unSAT accuracy (i.e. accuracy of correctly predicting unsatisfiable problems) on 3-SAT decision problem. GPT-4 outperforms all other models in detecting unsatisfiable problems. Both plots are on the search version of SAT-Menu setup with zero-shot prompting. The left plot was generated using a size 4 moving window on $\alpha$ values.
Refer to caption: extracted/5947246/plots/model_comparison_ablations.png

### 5.1 Can LLMs solve 3-SAT problems?

Accuracy: We evaluate GPT-4’s performance by measuring its accuracy (of solving for SAT Search and prediction for SAT Decision) across formulas with varying $\alpha$. We present these results in Figure 3 [Left]. GPT-4 demonstrates an apparent reasoning competence in the easy regions, while its accuracy significantly drops to $\approx 10\%$ in the hard region for SAT Search. We also observe that SAT Search poses a slightly greater challenge for GPT-4 than SAT Decision.

Satisfiability Ratio: In Figure 3 [Right] we also plot GPT-4’s performance against the *satisfiability ratio*, defined as $\frac{\text{model count}}{2^{n}}$, where model count is the number of satisfying assignments and $n$ is the number of variables. This ratio denotes the probability that a randomly selected variable assignment satisfies the given 3-SAT theory(^5^55Note that this is different from the probability that at least one satisfying assignment exists – two formulas can both be satisfiable but have different model counts and therefore different satisfiability ratios.). We can observe a clear dependence between the accuracy and the satisfiability ratio: formulas with more satisfying assignments tend to be easier for GPT-4 to solve. This holds across both easy and hard regions. Similar results were observed for other LLMs, as shown in Figure 7 in the Appendix.

Phase Transitions: In Figure 4 [Left], we can see that GPT-4 is the only model that exhibits solver-like phase transitions in the SAT Search problem. In contrast, other LLMs show a clear decline in performance in the high $\alpha$ region, displaying an Easy-Hard-Hard pattern. This is further supported in Figure 8 in the Appendix where we compare the phase transition characteristics across LLMs on both decision and search variants. While all LLMs perform significantly better on the decision variant, only GPT-4 consistently demonstrates an Easy-Hard-Easy phase transition in both. Moreover, GPT-4 is more accurate in detecting unsatisfiable instances, as shown in Figure 4 [Right] (and Figure 10 in the Appendix).

In-context Learning Finally, we explored in-context learning using three chain-of-thought input/output (I/O) demonstrations Brown et al. (). These were randomly selected from a set of correctly solved problem instances (by the LLM) and manually checked for consistency between solutions and their explanations. Each I/O example included the input and the output solution, along with its chain-of-thought explanation. From Figure 9 in Appendix, we observe performance gains in the initial Easy-Hard phase but note a decrease in the subsequent Easy phase.

Note, that in all the above experiments, the performance of LLMs remains low in the Hard region.

### 5.2 Can LLM-Modulo frameworks boost performance?

To enhance reasoning capabilities, recent studies have explored so-called LLM-Modulo frameworks coined by Kambhampati et al. (). The main idea is to augment LLMs with critics and verifiers (Lightman et al., ; Hazra et al., ), recognizing the ability of LLMs as *approximate* idea-generators for problems as against directly solving them. This approach is aligned with neurosymbolic techniques (De Raedt et al., ), 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 (pseudo)-natural language into a format that a 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 a 3-SAT solver to solve the translated instance (see Box C in Appendix).
We dub this approach SAT-Translate and plot its performance in Figure 5 [Left]. Other LLMs also display similar improvements in performance as shown in Figure 11 in the Appendix.

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, $\approx 100\%$ across the entire range of $\alpha$. 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 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 is primarily observed when they are equipped with an external solver. While not constituting a typical LLM-Modulo framework (requiring tighter integration), this is a simpler pipelined version explored in recent works (Ye et al., ; Wong et al., ).

Figure: Figure 5: [Left] The figure compares LLM-Modulo frameworks (denoted as SAT-Translate) – here, GPT-4 equipped with a solver – with standalone GPT-4 performance with SAT-Menu and SAT-CNF inputs. SAT-Translate approach (plotted in green) outperforms the rest, showing the significance of augmenting LLMs with symbolic solvers. [Right] The figure shows how the number of generated tokens by GPT-4 varies with the hardness ($\alpha$) of the problem – increasing in the hard region and vice versa.
Refer to caption: extracted/5947246/plots/tokens_and_modulo.png

## 6 Discussion

At first sight, our experimental evaluation can be interpreted as indicating that LLMs, specifically GPT-4, exhibit a certain degree of reasoning capabilities: in the easy regions, GPT-4 solves some 3-SAT problems. One might then argue that GPT-4 does not reach perfect accuracy in these regions because of the scale of the model, and that simply increasing this will resolve the issue. For the hard region, however, it is unlikely that scaling up the model will result in radical improvements.

To explain this, reconsider Figures 2 and the time vs. $\alpha$ plot specifically. The reason why MiniSAT is capable of solving problems in the easy regions faster than problems around $\alpha_{c}$ is due to the heuristics built into the solver that guide the search for satisfying solutions (e.g. unit propagation and clause learning (Marques-Silva & Sakallah, )). That is, heuristics work well when they can exploit statistical features in the problem instance to be solved.
To date, there are no known heuristics that work well around $\alpha_{c}$ (and they are unlikely to exist due to the NP-hardness of 3-SAT). Solvers therefore have to resort to brute force search around $\alpha_{c}$.

In this light, we can reinterpret the experimental performance of GPT-4 on 3-SAT problems: GPT-4’s apparent reasoning capabilities (in the easy regions) is due to the presence of statistical features that it can leach onto. For instance, GPT-4 may deem a problem unsatisfiable due to the high number of input tokens, which often works for overconstrained formulas (see Appendix B). Conversely, in the hard region, the drop in performance can be attributed to GPT-4’s – and by extension current transformer-based LLMs’ – inability to reason according to Bottou’s definition. A similar observation has been made for a computationally tractable class of problems (not NP-complete) using BERT-style language models (Zhang et al., ).

Our fine-grained empirical study also complements the theoretical results of LLM reasoning capabilities, c.f. log-uniform TC^0 complexity class. As these findings only provide bounds on worst-case performance, they have a rather limited significance with regard to average-case complexity (Coarfa et al., ) and, as such, a limited significance for the reasoning capabilities of LLMs in practice.

In this regard, it is interesting to note that recent works have demonstrated that $T$ chain-of-thought steps can enhance the sequential reasoning abilities of a fixed-size transformer. This enables transformers to solve problems beyond TC^0, up to those solvable by boolean circuits of size $T$ (Li et al., ). Similar ideas have been explored empirically in the form of \saypause tokens in Goyal et al. (). Based on this theory, one would expect the number of generated tokens (including that of CoT) to increase in the Hard. As shown in Figure 5 [Right], GPT-4 appears to follow this expected pattern by generating more tokens in the Hard region, consistent with the phase transition.
However, even though the number of generated patterns increases in the hard region, the performance of solving random 3-SAT problems drops significantly. An interesting observation is that other LLMs do not exhibit this increase in the number of generated tokens in the hard region. We report this in Figure 12 in the Appendix.

Even though the basic random 3-SAT phase transition provides a rigorous framework for studying the reasoning capabilities of LLMs, we need to point out that there exists many more results about 3-SAT that might be considered as well. For instance, it has been found that certain aspects of the hardness of 3-SAT instances cannot be explained using the easy-hard-easy regimes induced by the phase transition (Mu & Hoos, ). Nevertheless, the phase transition seems to be adequate in our settings as demonstrated by the drop in performance of LLMs in the vicinity of $\alpha_{c}$. It should, however, be noted that 3-SAT instances encountered in practice often fall into the easy regions. Therefore, decision problems of interest do not usually exhibit worst-case complexity.

## 7 Conclusion

A superficial analysis of the reasoning capabilities of LLMs suggests they possess strong and complex reasoning capabilities – a common fallacy (Bubeck et al., ). However, our detailed experimental analysis indicates that what appears as reasoning capabilities could be a mirage, with LLMs predominantly exploiting statistical features present in the data and would
explain why LLMs have been termed “statistical parrots” (Bender et al., ).

This is not to say that LLMs lack value – quite the opposite. LLMs are highly effective at translating problems into a formal language and then passing these problems on to solvers. This utility is demonstrated by the relatively superior performance of SAT-Translate over SAT-Menu and SAT-CNF. In a more general context, it would require that the class of the problem is recognized correctly – here 3-SAT – and that the right solvers are available.

Furthermore, LLMs can serve as valuable knowledge bases, leveraging their extensive common sense and world knowledge through natural language queries to guide search processes. This can be utilized by either solvers guiding LLMs (Hazra et al., ) or vice versa, where LLMs assist solvers (Wong et al., ).

## Reproducibility

We provide comprehensive instructions to ensure the reproducibility of the results. The dataset generation process and statistics are outlined in § 4.2 and Appendix A, the LLM configurations are listed in Appendix Table 2, and detailed prompts shown in Appendix C. Moreover, we also discuss limiting/failure cases in Appendix B and how they can be mitigated. We intend to open-source our code shortly.

## Acknowledgments

This work was supported by the Wallenberg AI Autonomous Systems and Software Program (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/062). The resources and services used in this work were provided by the VSC (Flemish Supercomputer Center), funded by the Research Foundation - Flanders (FWO) and the Flemish Government. We also thank Holger Hoos, Heikki Mannila, Paolo Frasconi, Pascal Van Hentenryck, Ross King, Giuseppe Marra, Pieter Delobelle, Hendrik Blockeel, and Raffaele Marino for their valuable feedback.

## Appendix

## Appendix A Dataset Statistics

Table 1 lists all values of the range of $\alpha$ corresponding to each $n$. For $\alpha$ values within the $(6,11]$ interval, we incremented $\alpha$ by $1$. For the $[1,6]$ interval, which contains the most “interesting problems,” we aimed for finer granularity by choosing the smallest possible $\alpha$ 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 $\alpha_{inc}=1$, and for $n=4$, it is $\alpha_{inc}=0.25$. For each $\alpha_{inc}$ we generated $300$ formulas.

The distribution of formulas according to the number of variables is detailed as follows: 3,000 formulas with 3 variables, 7,500 with 4 variables, 9,000 with 5 variables, 4,500 with 6 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 ($\alpha=m/n$) ranges in [1.1, 11.0]. For unSAT instances, the clauses range from 9 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 of clauses ($m$) is 33, and the mean $\alpha$ is 4.7. This diverse dataset provides a broad spectrum for analyzing the impact of variable and clause distribution on formula satisfiability.

**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 $\alpha$ value.**
| $n$ | Range of $\alpha$ |
| --- | --- |
| 3 | 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0, 10.0, 11.0 |
| 4 | 1.0, 1.25, 1.5, 1.75, 2.0, 2.25, 2.5, 2.75, 3.0, 3.25, 3.5, 3.75, 4.0, 4.25, 4.5, 4.75, 5.0, 5.25, 5.5, 5.75, 6.0, 7.0, 8.0, 9.0, 10.0, 11.0 |
| 5 | 1.0, 1.2, 1.4, 1.6, 1.8, 2.0, 2.2, 2.4, 2.6, 2.8, 3.0, 3.2, 3.4, 3.6, 3.8, 4.0, 4.2, 4.4, 4.6, 4.8, 5.0, 5.2, 5.4, 5.6, 5.8, 6.0, 7.0, 8.0, 9.0, 10.0, 11.0 |
| 6 | 1.0, 1.5, 2.0, 2.5, 3.0, 3.5, 4.0, 4.5, 5.0, 5.5, 6.0, 7.0, 8.0, 9.0, 10.0, 11.0 |
| 7 | 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0, 10.0, 11.0 |
| 8 | 1.0, 1.125, 1.25, 1.375, 1.5, 1.625, 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, 7.0, 8.0, 9.0, 10.0, 11.0 |
| 9 | 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0, 10.0, 11.0 |
| 10 | 1.0, 1.1, 1.2, 1.3, 1.4, 1.5, 1.6, 1.7, 1.8, 1.9, 2.0, 2.1, 2.2, 2.3, 2.4, 2.5, 2.6, 2.7, 2.8, 2.9, 3.0, 3.1, 3.2, 3.3, 3.4, 3.5, 3.6, 3.7, 3.8, 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.1, 5.2, 5.3, 5.4, 5.5, 5.6, 5.7, 5.8, 5.9, 6.0, 7.0, 8.0, 9.0, 10.0, 11.0 |

## Appendix B LLMs as Solvers: Failure Cases

**Table 2: Configuration Parameters**
| Parameter | Value |
| --- | --- |
| GPT-* |  |
| temperature | 1 |
| max_tokens | 4096 |
| top_p | 1 |
| frequency_penalty | 0 |
| presence_penalty | 0 |
| Llama 2 70B |  |
| 4-bit quantization | True |
| tokenizer type | Fast |
| max_new_tokens | 2048 |
| batch_size | 20 |
| Mixtral $8\times 7$B |  |
| 4-bit quantization | True |
| attention | Flash |
| max_new_tokens | 4096 |
| batch_size | 30 |

Here, we discuss some interesting failure cases we observed during our experiments. In the SAT-CNF context, it was observed that LLMs, including GPT-4, often opt to pass the task to an external SAT solver rather than solving it themselves. Additionally, when attempting to find a solution, these models tend to provide only a conceptual outline of the solution instead of a concrete answer, a tendency that becomes more pronounced with larger formulas. When prompted explicitly for a solution, GPT-4 might simplistically conclude that the problem is unsatisfiable due to its complexity, as shown in Box C. Although this reasoning is not entirely sound – as over-constrained formulas can still potentially be solvable – it appears that LLMs might be leveraging this as a statistical feature. Note, that the number of prompt tokens increases steeply from $\approx 500$ in the underconstrained region to $\approx 1200$ in the overconstrained regions.

In the SAT-Translate approach, it was observed that LLMs (with the exception of GPT-4) frequently deviated from the specific requirements of the prompt, generating solutions that did not adhere to the syntax expected by the solver. These inconsistencies in translation led to suboptimal accuracy levels within the LLM-Modulo frameworks.

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 to map the menu input to a 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.

## Appendix C Full Prompts

Here, we provide full prompts used in our experiments for SAT-Menu (Box C), SAT-CNF (Box C), and SAT-Translate (Box C).

Figure: Figure 7: LLM accuracy vs. satisfiability ratio. The figure shows how accuracy improves with satisfiability ratio (in log-scale) across all LLMs. The setup used is the search version of SAT-Menu with 0-shot prompting.
Refer to caption: x3.png

Figure: Figure 8: SAT Decision vs. SAT Search comparison. The figure illustrates the phase transitions in solving random 3-SAT problems, specifically comparing the decision and search variants. Although both variants fall under the same complexity class, empirical evidence shows that LLMs more readily solve the decision problem than the search problem. Among these models, only GPT-4 demonstrates the distinct Easy-Hard-Easy phase transition characteristic. The setup is SAT-CNF with 0-shot prompting. The plot was generated using a size 4 moving window on $\alpha$ values.
Refer to caption: x4.png

Figure: Figure 9: 0-shot vs. 3-shot accuracy. The figure compares 0-shot and 3-shot performance comparing all LLMs. It can be observed that, except GPT-4, in-context learning does not enhance performance for other LLMs. The setup is the search version SAT-Menu. The plot was generated using a size 4 moving window on $\alpha$ values.
Refer to caption: x5.png

Figure: Figure 10: Confusion matrices for 3-SAT Decision Problem. The figure compares the accuracy of all LLMs on the 3-SAT decision problem. It can be observed that, except GPT-4, all other LLMs struggle to correctly classify unsatisfiable instances. The cell annotations reflect classification accuracy, normalized over the true counts (column) to account for the imbalance between SAT and unSAT instances. The setup is SAT-Menu with 0-shot prompting.
Refer to caption: x6.png

Figure: Figure 11: LLM-Modulo Framework comparison. We compare the SAT Search performance of LLM-Modulo frameworks (SAT-Translate) with standalone LLM on SAT-Menu and SAT-CNF variants. Remarkably, the SAT-Translate approach (plotted in green) outperforms the rest, showing the significance of augmenting LLMs with symbolic solvers. The plot was generated using a size 4 moving window on $\alpha$ values.
Refer to caption: extracted/5947246/plots/combined_setups.png

Figure: Figure 12: # Generation tokens vs. $\alpha$. The figure shows how the number of generated tokens varies with the hardness of the problem. The setup used is the search version of SAT-Menu with 0-shot prompting. The plot was generated using a size 4 moving window on $\alpha$ values.
Refer to caption: extracted/5947246/plots/completion_tokens_vs_alpha.png

## Peer Reviews

confidence: 4
contribution: 3
initial_rating: 5
presentation: 2
questions: 1. I notice that, in figure 3, GPT-4 seemingly significantly worse than random guessing on the SAT decision problem around the critical point (which would imply for instance, that taking the opposite of its answer would be a better algorithm for the decision problem, giving about 70% accuracy right at alpha). Is this effect consistent/significant/predictable? Have the authors looked at why this is?
1. Given that these prompts are CoT prompts, have the authors looked at what sort of procedure the LLM claims to be following (and if it matches with the given examples)? Specifically, I'm curious if we can distinguish the LLM results from what we would get if instead we tested a noisy reasoner--a very simple example would be an implementation of DPLL where every each search step has some fixed epsilon probability of failure.
soundness: 3
strengths: 1. Contrasting previous work, the authors clearly define which notion of "reasoning" they are examining and choose a canonical, well-studied classical problem to examine LLM performance on. 
1. The introduction does a good job of covering most of major, relevant LLM reasoning-related previous work, situating the current work in the landscape of both positive and negative results.
1. The authors construct their evaluation set using a strong, well-studied random sampling procedure for 3-SAT problems, ensuring the distributional validity of their results, and allowing for more detailed analysis grounded in previous work.
1. The authors analyze much more than just accuracy, considering not only performance around the critical region, but also relative to another proxy for difficulty: the satisfiability ratio, thus strengthening their results.
1. The authors demonstrate how to boost performance in some cases by combining the LLM with an external solver.
1. The authors do their tests across a number of different models.
summary: The paper analyzes the algorithmic reasoning abilities of LLMs via the 3-SAT problem. The authors examine performance on instances of varying hardness as characterized by the phase transition of random 3-SAT. They test the LLM on three kinds of prompt: a representation of an integer CNF formulation, a natural language translation of the same, and a prompt that just asks the LLM to translate a natural language instance into LaTeX. They find that LLMs fail to robustly solve these problems, and SoTA systems perform worse on harder problems, but that--across many models--performance is much lower than the phase transition analysis would imply in high alpha regions.
weaknesses: ## Issues with Natural Language Prompt formulation
  
If I'm interpreting the SAT-MENU prompt correctly, then I believe it violates commonsense. The prompt asks for a list of orderable and a list of non-orderable foods that satisfies a group of people, or equivalently an assignment of "orderable" or "not orderable" to each food in a pre-specified list of foods. The immediate assumption is that satisfying this group of people has something to do with the actual act of ordering foods for the group somewhere down the line, e.g. that these lists will be used for ordering later on. However, given this or a similar assumption, the problem specification leads to some rather absurd possibilities. 
  
Consider "Jay dislikes pizza, pie, and nachos. Mary likes pizza and pie, but dislikes nachos." Is there an orderable list and non-orderable list which satisfies both Jay and Mary, using only pizza, pie, and nachos? A commonsensical answer would be no, because Jay doesn't like anything on the menu, but the structure of the problem is such that Jay is happy as long as one of the things he doesn't like isn't ordered. In particular, we have the following absurd-looking satisfying assignment: "orderable: nachos, pie. non-orderable: pizza" in which Jay is happy because pizza isn't orderable; whereas nachos, disfavored by both, *are* orderable. I know this is somewhat subjective, but this makes SAT-MENU more of a syntactic sugaring of the CNF prompt rather than a natural example of somewhere where this kind of reasoning needs to be done.
  
This likely speaks to a broader issue with the representations used here. The CNF formulation is a modeling convenience rather than a natural framing of real-world problems (see e.g. Stuckey 2013 "There Are No CNF Problems"). Analyzing SAT-CNF makes sense if we are interested in how well LLMs have acquired the ability to solve classical 3-SAT problems. SAT-MENU is the same problem with added distractors. Neither of them are well-justified as proxies for the kinds of natural language constraint satisfaction queries we might expect LLMs to actually be asked to solve. I would appreciate if the authors would clarify if the goal is to examine average-case reasoning performance (as alluded to in line 444) or to demonstrate the existence of a domain on which LLMs clearly fail to reason and resort to statistical shortcuts. If it is the former, I would be interested in seeing more plausible prompt reformulations.

## Complexity Class Claims
At lines 90-91 and 151, the authors claim that "logical reasoning, planning, and constraint satisfaction" can be reduced to 3-SAT. This is only true for limited forms of logical reasoning, e.g. the decision problem for first-order logic is in fact undecidable. Furthermore, planning also cannot in general be reduced this way: just the problem of plan existence (in STRIPS planning) is already PSPACE-complete. Note however that the (easier) *scheduling* phase is generally reducible to constraint satisfaction.

## Unclear Relationship to Cited Paper: Kambhampati 2024a
Lines 138-140 do not seem to match section 5.2. Emphasis mine:

> Additionally, we demonstrate how integrating LLMs with external **verifiers**, such as in the LLM-Modulo Frameworks (Kambhampati et al., 2024a), can enhance reasoning capabilities and improve performance on 3-SAT problems

Line 350 restates the claim:

> "The main idea is to augment LLMs with **critics and verifiers** (Lightman et al., 2024; Hazra et al., 2024b), recognizing the ability of LLMs as approximate idea-generators for problems as against directly solving them"

These quotes accurately reflect the LLM-Modulo framework as described in Kambhampati 2024a (quote from p6 of that paper): 

> "LLM-Modulo architecture is a 'Generate-Test' one that involves LLMs interacting with the external critics/verifiers **rather than a LLMs being just frontends to external solvers**" 

However, lines 355-356 describe the setup the authors tried in this paper, which contradicts both their previous summaries of their own work as well as the main idea of the framework they claim to be implementing. Section 5.2 describes how to use the LLM as a syntactic translator from the SAT-MENU format into one that MiniSAT can process, rather than using the LLM as a generator for proposed answers that are then filtered through sound verifiers/critics. Because of the problems presented (which are essentially already in CNF form) and the SAT solver in the loop, this seems to be a noisier analysis of the ability for the LLM to do syntactic translation, and doesn't tell anything about reasoning. (I say noisier because there is a chance that the generated translation was incorrect, but happened to have a satisfying assignment that also satisfies the real problem.)

If the authors are interested in the LLM-Modulo framework, perhaps one approach would be to compare how many generate-test iterations it takes for the model to output a satisfying assignment relative to the alpha region.

## Other Citation and Unclear Claim Issues/Nitpicks
1. The paper states that "emergent abilities have been shown to emerge" in line 39, but later (line 83) cites a paper claiming that emergent abilities are "a mere mirage," making the authors' position unclear.
1. Lines 80-81 cite Dziri 2023 for a claim about architectural limits of transformer layers, but that paper is an empirical evaluation of pre-trained models together with some (very broad) theoretical claims that are applicable to any autoregressive model, not just transformers. This citation doesn't seem to be relevant here and should likely be removed.
1. Line 182-183: Olausson 2024 and Liu 2023 are cited in the context of combining LLMs with verifiers and heuristics, but the systems proposed in those papers (LINC and LLM+P) combine translator LLMs with *solvers*, not verifiers. It's unclear why Lightman 2024 is cited, as it seems to be about process supervision at train time, rather than combining an LLM with a verifier at inference time.
1. Line 340: in-text citation was incorrectly formatted (citet should be citep).
1. The final paragraph of the conclusion (line 468-471) makes claims that seem unrelated to and unexamined by the content of the paper's body.

---

confidence: 4
contribution: 2
initial_rating: 5
presentation: 3
questions: None.
soundness: 3
strengths: It is worthwhile to experimentally test the limitations of LLMs via problems arising from complexity theory. I liked the fact that the authors consider the phase transition related to 3-SAT. The discussion on related works is thorough.
summary: The authors study the reasoning capabilities of various LLMs by studying how well they can solve the Boolean satisfiability problem. The authors consider two different encodings of 3-SAT instances to be given as input to LLMs. An encoding to a natural language problem (they construct a problem related to a group of people ordering food items with given constraints) and by directly imputing formulae in 3-CNF to the LLMs.

They generate several datasets of CNFs by using different fixed parameters for the ratio of the number of clauses and variables. By varying this constant the authors can control the proportion of satisfiable formulae in their datasets.

They also consider the task of using LLMs to transform inputs in their format to a format understandable by a SAT solver.

In general, they find that LLMs cannot solve 3-SAT, but that they can transform inputs in their format to a format understandable by a SAT solver.
weaknesses: The results are not surprising, as in general, current LLMs are not expressive enough (as mentioned by the authors) to decide 3-SAT. Moreover, LLMs have been recognised to be successful in transforming formats of diverse data, and hence it comes with no surprise that the integration of LLMs with SAT-solvers is successful. In summary, the authors only test how well various LLMs can solve 3-SAT. This kind of work is an excellent topic for a student project, but in my opinion does not suffice to be publishable in a top machine learning conference. 

There is not much theoretical contribution in the submission. While it is natural to consider 3-SAT as a problem to solve and to use different encodings to LLMs, there is nothing theoretically novel there. The technical contribution is to generate these inputs (taking the phase transformation of 3-SAT in mind) and tabulate the results with respect to different LLMs. I do not think that these contributions suffice for a publication in a top general conference in machine learning.

---

confidence: 3
contribution: 2
initial_rating: 6
presentation: 3
questions: - Why are instance in the dataset annotated with the number of satisfying models rather than just SAT/UNSAT information? 

- Have you considered extending this approach by any problems beyond 3-SAT? While I understand that the phase transition on random 3-SAT wrt. alpha is the key motivating factor for choosing 3-SAT, similar situations could maybe also arise in classic combinatorial problems over random graphs.
soundness: 3
strengths: - The paper proposes an approach beyond the common toy-like example based evidence often found LLM reasoning research and provides well-founded analysis of reasoning in LLMs. Beyond the 3-SAT   based analysis in particular, the general approach has potential to crate a broader range of LLM reasoning benchmarks. As such the submission could be important to this emerging area of research.

- As a secondary result, the submission demonstrate that LLMs are very capable of translating 3-SAt instances in textual form into input to SAT solvers. Although there is a small gap in the paper here in that it is not clear what happens when the input in the SAT-Menu format is provided that is not restricted to clauses with at most 3 terms, i.e., when it would be a general SAT instance beyond 3-SAT.

- The presentation is clear, the claims and methods are easily followable.
summary: This papers studies the question of whether LLMs can reason. Towards this question the authors propose a new method for studying reasoning capability, by evaluating the performance of LLMs in deciding satisfiability of 3-SAT instances.

This is motivated by a classic observation on the likelihood of random 3-SAT instances being satisfiable or unsatisfiable depending on the ratio alpha of clauses to variables in the instance. When alpha is low, the instance is almost surely satisfiable, and when the ratio is high, it is almost surely unsatisfiable. In the middle, there is a small range of this ratio where the satisfiability of random 3-SAT instances is hard to predict from statistical information.

The authors then compare this behaviour to the performance of various LLMs on random 3-SAT instances. As their key finding, they observe that the performance of GPT-4 is much better in the case of low or high alpha, suggesting that the LLM answers based on statistical/structural information rather than reasoning.
weaknesses: - The paper claims that these results counter previous works that suggest reasoning ability in LLMs. However, the results of this submission suggest that LLMs are effectively unable to reason about an NP-hard problem. Previous positive results such as those by Kojima et al. (2022) are on inherently simpler problems. The paper lacks an appropriate discussion on this mismatch and the role NP-complete problems in the current discourse on LLM reasoning ability.

- As mentioned above, I find the approach itself promising. But the paper lacks any discussion of building on this approach to provide a more complete picture on LLM reasoning limits. For example, it would be a natural next step to demonstrate similar behaviour of LLMs also for problems in lower complexity classes. But there is no discussion along these lines nor an attempt to frame the approach in a general fashion.

- The set of tested models seems slightly outdated for this submission cycle (GPT 4 Turbo, Gemini 1.0, Llama 2).

---

confidence: 4
contribution: 2
initial_rating: 5
presentation: 3
questions: See above comments.
soundness: 2
strengths: **Novelty:** While recent studies have examined the reasoning limitations of LLMs from a computational perspective, this paper provides new empirical findings through a statistical complexity analysis. One of the most noteworthy observations is the difficulty LLMs face in effectively addressing "simple" constraint satisfaction problems (CSPs). By "simple," I refer to CSP instances that involve no more than 10 variables, which are regarded as toy problems within the constraint programming community. For these instances, it appears that most LLMs do not significantly outperform a random baseline (Left part of Figure 4).
summary: This paper examines the reasoning capabilities of large language models (LLMs) through the perspective of statistical computational complexity. This framework analyzes computational complexity as a random variable influenced by specific order parameters of a given problem. The focus of this investigation is 3-SAT, a problem extensively studied in the AI literature for its phase transition phenomena. The authors demonstrate that state-of-the-art LLMs face significant challenges in solving random instances with up to 10 variables. Not only do LLMs struggle to resolve instances located in the phase-transition region, but they also often fail to address instances in the simpler regions that are either under-constrained or over-constrained. Additionally, the authors propose that an LLM-modulo SAT framework, which integrates an LLM architecture with a SAT solver, presents an alternative for tackling simple commonsense reasoning tasks that can be reframed as 3-SAT problems.
weaknesses: **Positioning:** Although I am convinced that the paper is conveying something new, the related work section could benefit from further elaboration, particularly in discussing the empirical results presented in this paper alongside recent studies that have theoretically and/or empirically explored the reasoning limitations of large language models (LLMs). Notably, Dziri et al. (2023) have experimentally demonstrated that the performance of Transformers on constraint reasoning tasks declines rapidly as the depth of the task increases. Furthermore, Peng et al. (2024) have shown that the satisfiability of Krom, Horn, or affine formulas cannot be determined by multi-layer Transformers unless L = NL. Hence, the new results concerning random 3-SAT instances are, at first glance, not particularly surprising.

**Clarity:** The first four sections are relatively clear, but I found the results in Section 5.1 and the significance of Section 5.2 confusing. In Section 5.1, why do the accuracy results for GPT-4 differ when comparing the left parts of Figure 3 and Figure 4?  I also found the experimental protocol in Section 5.2 somewhat perplexing. As I understand it, a constraint satisfaction problem described in natural language is first translated into a 3-SAT instance by a large language model (LLM) and then processed by a SAT solver. In this case, the “positive” results are not surprising at all, since the LLM is not being used to "reason" about the input problem; it is merely parsing the problem into a CNF expression.

**Contribution:** Based on the comments above, the main contribution of this paper is essentially limited to a statistical analysis of the accuracies of large language models (LLMs) on random instances of 3-SAT. By breaking down the distribution of instances into three typical regions, most LLMs struggle to solve instances in all these regions, even when the number of variables $n$ is small. Notably, we cannot conclusively state that GPT-4 behaves similarly to complete or local SAT algorithms for random 3-SAT; even for very easy instances ($\alpha \rightarrow 0$), its performance in finding a solution hovers around 70%. Therefore, a natural extension of this analysis would be to investigate the behavior of LLMs, particularly GPT-4, on simpler constraint satisfaction problems. This would help clarify their reasoning abilities. To this point, I would suggest examining random Krom instances (2-SAT), random Horn instances (HORN), and the intersection of these propositional classes (2-HORN-SAT). 

**Minor comment:** In Section 2.2, nowadays, complete SAT solvers use CDCL instead of DPLL (in its basic form).

Meta-review: **Summary:**
This paper studies reasoning ability of LLMs. For this purpose this paper experiments performance of LLMs in solving 3-SAT problems. Two different modes of presenting problem instances to LLMs are considered: one is SAT-CNF, where the prompts to be presented to an LLM are something like that shown in Box 3, and the other is SAT-Menu, where a SAT problem instance is reframed as a natural-language menu-selection problem as in Box 2. Two tasks are considered: in "SAT Decision" an LLM is asked to respond with "Yes/No" according to whether the presented instance is satisfiable or not, whereas in "SAT Search" an LLM should also return an assignment if the presented problem instance is SAT. The experimental results are compared with the known satisfiability threshold of random 3-SAT, which is $\alpha_c\approx4.27$.

**Strengths:**
The authors clearly define the notion of "reasoning" they examine, and take 3-SAT as a canonical, well-established problem from complexity theory, on which performance of LLMs is examined.

**Weaknesses:**
- Some reviewers expressed concern on the importance of the results.
- In addition to the concerns raised by the reviewers, I would add one more point. It is known, besides the satisfiability transition point $\alpha_c\approx4.27$, that there exist some other types of phase transition for 3-SAT as well (see, e.g., Krzakala et al. (2007)): for example, the dynamic phase transition point $\alpha_d\approx3.86$, above which the set of solutions decomposes into many disconnected clusters, and the condensation phase transition point (which is known to coincide with $\alpha_d$ for 3-SAT, and to be larger than $\alpha_d$ and smaller than $\alpha_c$ for $K$-SAT with $K\ge4$), above which the cluster sizes become uneven. One would expect that heuristic methods would be effective for $\alpha$ less than $\alpha_d$ but not for $\alpha$ larger than $\alpha_d$, making $\alpha_d$ a sound choice as the easy-hard boundary. (Note that these notions are defined in the asymptotic $n\to\infty$.) The authors should take into account these results in their analysis.

Krzakala et al., "Gibbs states and the set of solutions of random constraint satisfaction problems," PNAS, volume 104, pages 10318-10323, 2007.

**Reasons:**
Three reviewers rated this paper just below the acceptance threshold. My own evaluation is aligned with these reviewers in that, although this paper presents something interesting on reasoning abilities of LLMs, it would benefit from further revisions taking the review comments into account.

Additional points:
- Figure 2: Those plots (probability of satisfiability and solver running time versus $\alpha$) should depend on the number $n$ of variables, whose value is however not mentioned. Whether the probability of satisfiability is 1 or 0, which determines the hard region, should also depend on $n$ and the number of instances examined (CNF formulas): if more instances are examined one would have a narrower hardness region. Furthermore, the *true* probability of a random formula to be satisfiable is never equal to 0, since, given an arbitrary assignment, there always exists a formula which satisfies the given assignment, making the probability strictly positive for any $\alpha$.  It would make the use of the probability of satisfiability in defining the hardness region inappropriate.
- Figure 3 [Right]: Again, there should be $n$-dependence as above, which is not stated explicitly. I did not understand why the authors show two plots, one for "easy" and the other for "hard".
  - These two are not distinguished in Figure 7, which shows similar plots for other LLMs. It would make the significance of distinguishing "easy" and "hard" in Figure 3 unclear.
  - I did not understand either why the ranges of satisfiability ratios for the two plots overlap. One would expect, as a general trend, that the satisfiability ratio monotonically decreases as $\alpha$ becomes larger, so that the "easy" plot should have a gap in the satisfiability ratio values that corresponds to the range of the "hard" region.
- Figure 6 right: I guess that the multi-peak structure of the distributions of $\alpha$ values shown here would be an artefact arising from use of a kernel density estimator. This figure would provide a wrong impression as if there are probability density functions for the values of $\alpha$.

Decision: Reject