Satisfiability Solving with LLMs: A Matched-Pair Evaluation of Reasoning Capability

• URL: http://arxiv.org/abs/2605.28602v1
• Date: Wed, 27 May 2026 15:18:45 GMT
• Title: Satisfiability Solving with LLMs: A Matched-Pair Evaluation of Reasoning Capability
• Abstract summary: Large language models (LLMs) are increasingly used for tasks that implicitly reduce to Boolean satisfiability (SAT)<n>We present a systematic study of LLMs on 2-SAT and 3-SAT, together with two canonical reductions, Vertex Cover and discrete 3D packing.
• Score: 8.964195566025824
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Large language models (LLMs) are increasingly used for tasks that implicitly reduce to Boolean satisfiability (SAT), yet their reasoning ability on SAT remains unclear. We present a systematic study of LLMs on 2-SAT and 3-SAT, together with two canonical reductions, Vertex Cover and discrete 3D packing, to probe representation-invariant reasoning. We first evaluate models using conventional metrics, including accuracy, precision, recall, and F1, as well as the SAT phase-transition setting. We find that these metrics can be misleading: many models obtain high scores by over-predicting satisfiable formulas, fail to reproduce the classical easy-hard-easy signature around the 3-SAT threshold, and degrade sharply as the number of variables grows. To address this problem, we introduce a paired-formula protocol based on minimally different satisfiable and unsatisfiable instances, together with Accurate Differentiation Rate (ADR), which requires both members of each pair to be classified correctly. ADR separates reasoning-oriented models from heuristic ones and correlates with witness validity. Beyond CNF, we test cross-representation consistency by converting CNF to Vertex Cover and 3-SAT to discrete 3D packing. Model decisions on CNF and on the corresponding graph or packing instances agree for most models on more than 80 percent of instances, suggesting stable decision rules across representations. Overall, our results show that SAT is a conservative probe for LLM reasoning, and that paired evaluation with ADR provides a more faithful and representation-robust assessment than conventional metrics.

Related papers

• Ensemble-Based Uncertainty Estimation for Code Correctness Estimation [36.53771380869671]
  We propose Ensemble Semantic Entropy (ESE), which estimates uncertainty by evaluating the consistency of samples aggregated across an ensemble of models.<n>Experiments on LiveCodeBench demonstrate that ESE correlates more strongly with program correctness than single-model semantic entropy.<n>We also propose a cascading test-time scaling framework Cas, which maintains performance while reducing FLOPs by 64.9% compared to single-model scaling.
  arXiv  Detail & Related papers  (2026-03-28T02:37:36Z)
• Test-Time Scaling with Diffusion Language Models via Reward-Guided Stitching [66.39914384073145]
  We propose a self-consistency framework that turns cheap diffusion-sampled reasoning into a reusable pool of step-level candidates.<n>We find that step-level recombination is most beneficial on harder problems.<n>Our training-free framework improves average accuracy by up to 2 across six math and coding tasks.
  arXiv  Detail & Related papers  (2026-02-26T11:08:39Z)
• Evaluating Robustness of Reasoning Models on Parameterized Logical Problems [20.78623024814435]
  Logic provides a controlled testbed for evaluating LLM-based reasoners.<n>Standard SAT-style benchmarks often conflate surface difficulty (length, wording, clause order) with the structural phenomena that actually determine satisfiability.<n>We introduce a diagnostic benchmark for 2-SAT built from parameterized families of structured 2--CNF formulas.
  arXiv  Detail & Related papers  (2026-02-13T06:54:25Z)
• RoParQ: Paraphrase-Aware Alignment of Large Language Models Towards Robustness to Paraphrased Questions [0.0]
  Large Language Models (LLMs) often exhibit inconsistent behavior when answering paraphrased questions.<n>We introduce RoParQ, a benchmark to evaluate cross-paraphrase consistency in closed-book multiple-choice QA.<n>We also propose XParaCon, a novel evaluation metric that quantifies a model's robustness.
  arXiv  Detail & Related papers  (2025-11-26T16:40:53Z)
• DistJoin: A Decoupled Join Cardinality Estimator based on Adaptive Neural Predicate Modulation [11.506172695239576]
  We introduce DistJoin, a join cardinality estimator based on efficient distribution prediction using multi-autoregressive models.<n>We demonstrate that DistJoin mitigates the highest accuracy, robustness to data updates, generality, and comparable update and inference speed relative to existing methods.
  arXiv  Detail & Related papers  (2025-03-12T02:07:08Z)
• Log Probabilities Are a Reliable Estimate of Semantic Plausibility in Base and Instruction-Tuned Language Models [50.15455336684986]
  We evaluate the effectiveness of LogProbs and basic prompting to measure semantic plausibility. We find that LogProbs offers a more reliable measure of semantic plausibility than direct zero-shot prompting. We conclude that, even in the era of prompt-based evaluations, LogProbs constitute a useful metric of semantic plausibility.
  arXiv  Detail & Related papers  (2024-03-21T22:08:44Z)
• Noisy-Correspondence Learning for Text-to-Image Person Re-identification [50.07634676709067]
  We propose a novel Robust Dual Embedding method (RDE) to learn robust visual-semantic associations even with noisy correspondences. Our method achieves state-of-the-art results both with and without synthetic noisy correspondences on three datasets.
  arXiv  Detail & Related papers  (2023-08-19T05:34:13Z)
• Explaining SAT Solving Using Causal Reasoning [30.469229388827443]
  We introduce CausalSAT, which employs causal reasoning to gain insights into the functioning of modern SAT solvers. We use CausalSAT to quantitatively verify hypotheses previously regarded as "rules of thumb" or empirical findings.
  arXiv  Detail & Related papers  (2023-06-09T22:53:16Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
  arXiv  Detail & Related papers  (2022-10-04T09:19:13Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Tractable Inference in Credal Sentential Decision Diagrams [116.6516175350871]
  Probabilistic sentential decision diagrams are logic circuits where the inputs of disjunctive gates are annotated by probability values. We develop the credal sentential decision diagrams, a generalisation of their probabilistic counterpart that allows for replacing the local probabilities with credal sets of mass functions. For a first empirical validation, we consider a simple application based on noisy seven-segment display images.
  arXiv  Detail & Related papers  (2020-08-19T16:04:34Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.