Reliable Reasoning with Large Language Models via Preference-Based Maximum Satisfiability

Technical Summary: Reliable Reasoning with Large Language Models via Preference-Based Maximum Satisfiability

Problem Statement

Large Language Models (LLMs) demonstrate strong capabilities in natural language understanding and code generation but exhibit significant unreliability when tasked with complex optimization problems involving multiple constraints and user-defined preferences. In domains such as robotics and logistics, where correctness and provable optimality are critical, LLMs often fail to satisfy hard constraints or minimize objective functions when relying solely on internal reasoning (e.g., Chain-of-Thought) or direct answer generation. These failures stem from the combinatorial nature of optimization and the LLM's inability to perform exact reasoning, leading to infeasible or sub-optimal solutions that are difficult to verify. Furthermore, existing formal methods like Maximum Satisfiability (MaxSAT) require users to express preferences in specialized, rigid languages (e.g., PDDL), creating a barrier to entry for non-experts.

Methodology

The paper proposes a hybrid neuro-symbolic approach that externalizes reasoning from the LLM to a formal solver. The core paradigm, referred to as "vibe coding," involves the LLM translating natural language problem descriptions into executable Python code, which is then solved by an exact MaxSAT solver.

The proposed pipeline consists of the following stages:

1. Intermediate Planning: Before generating code, the LLM is prompted to produce a structured, symbolic description of the decision variables, hard constraints, and soft preferences. This step aims to improve modeling accuracy by forcing a systematic breakdown of the problem.
2. Code Generation: The LLM generates Python code using the PySAT API to encode the problem as a weighted partial MaxSAT instance. Hard constraints are encoded as hard clauses, while user preferences are encoded as weighted soft clauses.
3. MaxSAT Solving: The generated code is executed to invoke a MaxSAT solver (specifically RC2 from PySAT). The solver guarantees that the returned assignment is feasible (satisfies all hard clauses) and optimal (minimizes the total weight of unsatisfied soft clauses) with respect to the encoded problem.
4. Verification: To evaluate the system without relying on the LLM's internal reasoning, the authors construct a "canonical" MaxSAT encoding for each problem instance. This canonical encoding serves as a ground truth for verification only. The solution produced by the LLM-generated code is verified against this canonical encoding to check:
   • Feasibility: Does the solution satisfy all hard constraints?
   • Optimality: Does the solution achieve the same objective value as the canonical optimal solution?
   • Note: This verification allows for alternative encodings and multiple optimal solutions, provided they are correct under the reference semantics.
5. Feedback Loop: If the code fails to execute or produces an error, the error message is returned to the LLM for refinement. Crucially, the canonical verification results (feasibility/optimality checks) are not used as feedback to the model during the generation process to prevent data leakage or overfitting to the reference.

Key Contributions

• Neuro-Symbolic Framework: The authors present a method where LLMs act as natural language interfaces to weighted partial MaxSAT solvers, translating user intent into formal MaxSAT formulations via code generation.
• Independent Verification: The study introduces an evaluation protocol that verifies LLM-generated solutions against a canonical encoding for both feasibility and optimality, decoupling solution validity from the correctness of the LLM's internal reasoning.
• Empirical Analysis of Preferences: The paper analyzes how different user-defined preference configurations impact LLM reasoning performance across various constraint optimization problems.
• Intermediate Planning Evaluation: The work investigates the efficacy of an intermediate planning step, finding that it improves performance for stronger models but may introduce error propagation for weaker ones.

Experimental Results

The approach was evaluated on three families of preference-based reasoning tasks: Maximum Independent Set (MIS), Scheduling, and Set Cover. The dataset comprised 300 instances (25 per family × 4 preference variants) tested on four LLMs (GEMINI-3.1-PRO, GPT-5.5, LLAMA3.3, and QWEN3-CODER).

• Baseline Performance: Direct-answer and Chain-of-Thought (CoT) baselines performed poorly, often achieving 0% acceptance rates on MIS and Scheduling tasks. Program-of-Thought (PoT) baselines showed slight improvements but remained significantly lower than the MaxSAT-based approach.
• MaxSAT Pipeline Performance: The proposed MaxSAT-based pipeline achieved substantially higher acceptance rates. For strong models like GEMINI-3.1-PRO and GPT-5.5, acceptance rates exceeded 80% on Set Cover tasks and reached approximately 56–59% on Scheduling and MIS tasks when intermediate planning was used.
• Impact of Planning: Intermediate planning consistently improved performance for the strongest models (e.g., GEMINI-3.1-PRO improved from 36% to 56% on MIS). However, for weaker models (LLAMA3.3, QWEN3-CODER), planning sometimes degraded performance, suggesting that error propagation can occur if the model cannot faithfully translate the plan into executable code.
• Preference Sensitivity: While user preferences generally reduced acceptance rates compared to the "no preference" setting, the MaxSAT-based approach remained more robust than baselines across all preference variants.

Significance and Claims

The paper claims that its primary contribution is not a new solver architecture, but an empirical and methodological demonstration of using LLMs as interfaces to formal solvers for preference-aware optimization. The authors assert that:

1. Externalization is Key: LLMs should not be trusted to perform optimization reasoning internally; instead, they are highly effective at translating natural language constraints into executable code.
2. Reliability via Solvers: By delegating the optimization and verification to sound and complete MaxSAT solvers, the system achieves formal guarantees of feasibility and optimality that pure LLM reasoning cannot provide.
3. Robustness: The combination of LLM-driven semantic interpretation and MaxSAT solving enables robust, verifiable decision-making that accommodates user preferences without requiring specialized domain languages.

The authors conclude that separating semantic interpretation (LLM) from formal optimization (MaxSAT solver) is a promising direction for building reliable, user-facing decision-making systems, particularly in fields where correctness is paramount. They note that future work will explore interactive settings where users can iteratively refine preferences with the support of this neuro-symbolic loop.