Reliable Reasoning with Large Language Models via Preference-Based Maximum Satisfiability
Pedro Orvalho, Marta Kwiatkowska, Guillem Alenyà, Felip Manyà
Abstract
Large Language Models (LLMs) excel at understanding natural language but struggle with optimisation tasks involving multiple constraints and user-defined preferences, which commonly arise in domains such as robotics. We propose a hybrid reasoning approach in which LLMs externalise reasoning through code generation. Given a natural language problem description, an LLM generates Python code that encodes user-defined constraints and preferences as a preference-based Maximum Satisfiability (MaxSAT) problem, which is then solved by an exact MaxSAT solver. To ensure correctness, solutions returned by the model-generated code are independently verified for feasibility and optimality against a canonical MaxSAT encoding, allowing for different encodings and multiple optimal solutions. We evaluate our approach using both open-source and closed-access LLMs on three families of preference-based reasoning tasks, and compare it against direct-answer, chain-of-thought, and program-of-thought baselines using the same models. While these baselines rarely produce feasible solutions, the MaxSAT-based pipeline achieves substantially higher acceptance rates, in some cases exceeding 80%. Our results demonstrate that LLM-driven code generation combined with preference-based MaxSAT enables solver-verifiable optimisation with respect to generated encodings, and substantially improves correctness under independently verified reference semantics.
AI Impact Assessments
(1 models)Scientific Impact Assessment
Core Contribution
This paper proposes a neuro-symbolic pipeline where LLMs translate natural language optimization problems into executable Python code that encodes weighted partial MaxSAT instances, which are then solved by an exact MaxSAT solver (RC2 via PySAT). The key novelty lies in targeting preference-based optimization — not just feasibility or planning — and introducing a canonical verification protocol that independently checks both feasibility and optimality of LLM-generated solutions against a reference MaxSAT encoding. The pipeline includes an optional intermediate planning step where the LLM first outlines variables, constraints, and preferences before generating code.
The contribution is best characterized as a methodological and empirical study rather than a new architecture. The individual components (LLM code generation, MaxSAT solving, verification) are established; the contribution is their specific combination for preference-aware optimization and the systematic empirical analysis across models, problem families, and preference configurations.
Methodological Rigor
Strengths in experimental design:
Weaknesses:
Potential Impact
The paper addresses a genuine practical need: enabling users to express complex optimization problems in natural language while obtaining formally verified solutions. The robotics and scheduling use cases are compelling.
Practical applications: The approach could benefit non-expert users who need to solve constraint optimization problems but lack formal modeling expertise. Domains include scheduling, resource allocation, logistics, and robotic task planning.
Limitations on impact: The restriction to Boolean optimization (SAT/MaxSAT) is significant. Many real-world optimization problems involve continuous variables, mixed-integer programming, or stochastic elements. The paper positions MaxSAT as natural for "predominantly Boolean" problems, but this narrows the applicability considerably. Integration with broader optimization frameworks (MIP solvers, CP solvers) would substantially increase practical relevance.
The acceptance rates, while much better than baselines, are still concerning for deployment: even the best configuration (Gemini-3.1-Pro with planning on set cover) achieves only 87%. For safety-critical robotics applications, 13-80% failure rates are problematic.
Timeliness & Relevance
The paper is timely, sitting at the intersection of several active research threads: LLM reasoning limitations, neuro-symbolic AI, and "vibe coding." The recent explosion of LLM-based coding tools makes the code-generation-as-reasoning paradigm practically relevant. The paper correctly identifies that LLMs should serve as interfaces rather than reasoners for optimization tasks — a perspective gaining traction in the community.
The work builds naturally on SATLM, Logic-LM, LLMFP, and ConstraintLLM, extending the neuro-symbolic paradigm specifically to preference-based optimization. The distinction from prior work (preference-awareness, weighted soft constraints, optimality verification) is clear but incremental.
Strengths
1. Clear problem framing: The motivating example effectively illustrates why LLMs fail at optimization and how MaxSAT solvers address this.
2. Principled verification: The canonical encoding approach for evaluation is methodologically sound and allows fair cross-model comparison.
3. Comprehensive ablation: The analysis of planning steps, preference variants, and cross-model plan transfer provides useful insights.
4. Practical design: Using PySAT as the interface is pragmatic — it's a well-maintained Python library that LLMs can reasonably learn to use from prompt examples.
5. Honest limitations: The paper forthrightly discusses model-dependence, the gap between encoded and intended semantics, and benchmark limitations.
Limitations
1. Limited problem scope: Only three Boolean optimization families are tested. Real-world preference-based problems often involve numeric, temporal, or continuous constraints.
2. No deeper error analysis: Understanding *why* encodings fail would be more valuable than aggregate acceptance rates.
3. Incremental novelty: The core idea of LLM + formal solver is well-established (SATLM, Logic-LM, LLMFP, ConstraintLLM). The extension to MaxSAT with preferences is natural but not conceptually surprising.
4. Missing comparisons: No comparison against ConstraintLLM or LLMFP, which address related problems with CP and SMT solvers respectively.
5. Scalability unclear: All instances appear to be small (6 jobs, small graphs). Whether the approach scales to larger, more realistic instances is untested.
6. No user study: The paper motivates the work through user-facing scenarios but provides no evidence of usability with actual users.
7. Reproducibility concerns: The benchmark and code availability are not explicitly discussed, though prompts are provided.
Overall Assessment
This is a competent empirical study that applies the established neuro-symbolic paradigm (LLM for parsing, solver for reasoning) to preference-based MaxSAT optimization. The results convincingly demonstrate that externalizing optimization to MaxSAT solvers substantially outperforms LLM-only approaches, which is expected but worth documenting rigorously. The canonical verification protocol is a useful methodological contribution. However, the novelty is incremental over prior work, the benchmark is limited in scale and scope, and the analysis could be deeper. The paper would benefit from larger-scale experiments, failure mode analysis, comparison with competing neuro-symbolic frameworks, and evaluation on problems beyond pure Boolean optimization.
Generated May 29, 2026
Comparison History (14)
Paper 2 has higher potential scientific impact due to a more novel and broadly applicable framework: using LLMs to generate formal MaxSAT encodings with independent feasibility/optimality verification. This directly addresses a central, timely problem—reliable, constraint-satisfying reasoning—and bridges NLP, formal methods, and robotics/operations research with solver-verifiable guarantees. Its methodological rigor is strengthened by canonical-encoding verification and comparisons to strong baselines. Paper 1 is impactful for privacy/bandwidth-efficient speech translation, but split inference and curriculum/data balancing are more incremental and narrower in cross-domain reach.
Paper 2 likely has higher scientific impact due to a clearer, more rigorous contribution: a solver-verifiable hybrid LLM+MaxSAT pipeline with independent feasibility/optimality checking against canonical semantics. This directly addresses correctness and reliability—key barriers for deploying LLM reasoning in safety- and constraint-critical domains (e.g., robotics, planning, configuration). The method leverages established optimization theory/tools, is broadly applicable to many preference/constraint problems, and offers strong empirical gains over common LLM baselines. Paper 1 is valuable but more domain-specific and benchmark-driven, with less emphasis on formal verification guarantees.
Paper 1 offers a more novel and broadly useful hybrid framework: translating natural-language constraints/preferences into MaxSAT with solver-verifiable optimality and independent checking against reference semantics. This directly improves reliability on constrained optimization—important for robotics, scheduling, planning, and other safety/operations domains—while providing a rigorous evaluation protocol (feasibility/optimality verification) beyond simple task success. Paper 2 introduces a timely benchmark for trajectory efficiency, but is primarily an evaluation/dataset contribution with narrower immediate applications and less methodological innovation than solver-grounded reasoning.
Paper 2 likely has higher impact: it introduces a broadly applicable, rigorous hybrid framework (LLM-to-code + exact MaxSAT) with independent feasibility/optimality verification, directly addressing reliability—one of the most urgent LLM limitations. The method is clearly actionable across many constraint-optimization domains (planning, scheduling, robotics, config, operations research) and leverages established solvers for guarantees, increasing methodological rigor and real-world deployability. Paper 1 is valuable but more specialized as a diagnostic tool for VLA models, with narrower immediate application scope and less direct performance/reliability gains.
Paper 2 addresses a fundamental limitation of LLMs in handling complex optimization and constraint-solving tasks by integrating them with exact MaxSAT solvers. This general-purpose hybrid reasoning framework has broad applicability across multiple fields, including robotics, operations research, and AI planning. In contrast, Paper 1, while demonstrating strong results and methodological rigor, focuses on a highly specific application (biological ontology curation). Therefore, Paper 2 has a significantly broader potential scientific impact.
Paper 2 has higher potential scientific impact because it challenges a fundamental assumption in literature search evaluation—that human citation lists are reliable ground truth—and provides compelling evidence of systematic biases (e.g., collaboration bias). This has broad implications across all scientific fields that rely on literature search and bibliometric evaluation. The Deep Research pipeline achieving 80%+ recall is practically significant, and the multi-axis evaluation framework could reshape how retrieval systems are benchmarked. Paper 1, while technically sound, addresses a narrower problem (LLM+MaxSAT for constraint reasoning) with more limited cross-field applicability.
Paper 1 introduces a highly innovative neuro-symbolic approach combining LLMs with MaxSAT solvers, directly addressing the critical issue of LLM reliability and hallucination in constrained optimization tasks. This methodological advancement provides verifiable correctness, which has profound implications for high-stakes fields like robotics and operations research. While Paper 2 offers a valuable practical benchmark for agent evaluation, Paper 1 presents a fundamental algorithmic solution that significantly advances the rigor and trustworthiness of LLM reasoning.
Paper 1 is more likely to have higher impact due to its novel, solver-verifiable hybrid methodology that directly improves LLM reliability on constrained optimization—an important, timely bottleneck for deploying LLMs in safety- and correctness-critical settings (e.g., robotics, planning, scheduling). Its use of MaxSAT with independent feasibility/optimality verification provides strong methodological rigor and a general pattern for integrating LLMs with formal methods. Paper 2 offers a valuable benchmark for personal-memory QA, but its primary contribution is diagnostic evaluation rather than a broadly applicable, provably-checkable reasoning mechanism.
Paper 1 provides a rigorous theoretical foundation for understanding and bounding compositional incoherence in multi-component LLM agents, introducing novel metrics and deterministic repair mechanisms. While Paper 2 offers a practical neuro-symbolic approach for optimization via MaxSAT, Paper 1's fundamental mathematical formalization addresses a deep, emerging problem in multi-agent AI systems, offering broader theoretical impact and stronger methodological rigor.
Paper 1 offers a highly rigorous, neuro-symbolic approach to solving a fundamental limitation of LLMs (complex reasoning and optimization) by pairing them with exact MaxSAT solvers. It includes empirical validation and addresses problems applicable across multiple domains like robotics and operations research. In contrast, Paper 2 presents a conceptual framework for educational chatbots lacking the same level of methodological rigor and broad technical impact.
Paper 1 identifies a novel and previously undocumented failure mode ('unfaithful capitulation') in reasoning models where chain-of-thought remains correct but answers flip under adversarial pressure. This has broad implications for AI safety, alignment, and deployment of reasoning models in interactive settings. The rigorous 2×2 framework, causal evidence across models, and the finding that naive defenses backfire make it highly impactful. Paper 2 presents a useful but more incremental hybrid approach combining LLMs with MaxSAT solvers. While practical, it addresses a narrower problem with less fundamental significance for the field.
Paper 1 proposes a highly innovative neuro-symbolic approach that bridges LLMs with exact MaxSAT solvers, addressing a critical weakness in LLMs: reliable constraint satisfaction and optimization. This has broad, immediate applications in fields requiring strict logical correctness, like robotics. Paper 2 offers a valuable but more incremental efficiency improvement for post-training via offline RL. Thus, Paper 1 demonstrates greater novelty and potential for cross-disciplinary impact.
Paper 2 introduces a novel, rigorous methodology combining LLMs with MaxSAT solvers, addressing a critical bottleneck in AI: reliable, verifiable reasoning and optimization. This hybrid approach has broad applicability across fields requiring strict constraint solving. Paper 1, while addressing a vital societal issue, is primarily a survey and conceptual framework. Paper 2's empirical validation, strict verification pipeline, and significant performance improvements over baselines give it stronger potential for immediate and widespread methodological impact in the rapidly advancing field of LLMs.
Paper 2 addresses a fundamental challenge in training Large Reasoning Models—improving Reinforcement Learning from Verifiable Rewards (RLVR). By introducing an adaptive weighting mechanism that prevents entropy collapse, it offers a core methodological improvement to LLM alignment and training. While Paper 1 presents a valuable neuro-symbolic approach (LLMs + MaxSAT) for constraint solving, Paper 2's focus on foundational RL techniques for open-ended QA has a broader potential impact across the AI community, as advancements in LLM training methodologies drive the capabilities of the next generation of AI systems.