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

Researchers present a systematic evaluation of large language models' reasoning capabilities on Boolean satisfiability problems, introducing a paired-formula protocol with Accurate Differentiation Rate (ADR) metric that reveals conventional accuracy metrics can be misleading, as models often succeed through heuristics rather than genuine reasoning.

This research addresses a fundamental gap in understanding LLM capabilities beyond surface-level performance metrics. While LLMs are increasingly deployed for complex reasoning tasks, their actual problem-solving abilities remain poorly characterized. The study uses SAT problems—a canonical NP-complete problem class—as a rigorous probe for reasoning capability, revealing that models achieve artificially inflated scores by systematically over-predicting satisfiable instances rather than developing robust solution strategies.

The work's significance lies in demonstrating that traditional evaluation metrics (accuracy, precision, recall, F1) fail to capture meaningful reasoning distinctions. The classical easy-hard-easy phase-transition signature in 3-SAT provides a ground truth that most models fail to reproduce, indicating they lack representation-invariant understanding. The paired-formula protocol with ADR represents a methodological advance by requiring correct classification of minimally different satisfiable-unsatisfiable pairs, effectively filtering out shallow pattern-matching from genuine reasoning.

For the broader AI development community, these findings suggest current evaluation frameworks systematically overstate model capabilities in logical reasoning tasks. This matters significantly for applications relying on LLMs for verification, constraint solving, and formal reasoning—areas where heuristic performance is insufficient. The cross-representation consistency testing (CNF to Vertex Cover conversion) indicates models develop some stable decision rules, though not necessarily valid ones.

Looking forward, this work should catalyze development of more rigorous evaluation benchmarks. The ADR metric and paired-formula approach provide templates for assessing reasoning in other domains. Researchers should investigate whether training methods can improve representation-invariant reasoning or whether fundamental architectural changes are required for genuine SAT solving capability.

• →Conventional metrics mislead by rewarding models that over-predict satisfiability rather than demonstrating genuine reasoning
• →The Accurate Differentiation Rate (ADR) metric on paired formulas better separates heuristic behavior from authentic logical reasoning
• →LLM performance degrades sharply with variable count and fails to reproduce classical SAT phase-transition signatures
• →Models maintain 80%+ cross-representation consistency despite systematic reasoning failures, suggesting stable but incorrect decision rules
• →SAT problems provide conservative, rigorous probes for assessing LLM reasoning capabilities relative to conventional benchmarks