💻 computer science

MaxSAT-Based Feedback for Guiding Vision-Language Models in Sudoku

This paper proposes a neuro-symbolic framework that enhances Vision-Language Models' performance on Sudoku puzzles by using a MaxSAT oracle to validate candidate assignments and provide structured feedback, thereby enforcing logical consistency and improving solution accuracy.

Original authors: Pedro Orvalho, Guillem Alenyà, Felip Manyà

Published 2026-07-15

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Pedro Orvalho, Guillem Alenyà, Felip Manyà

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine you have a super-smart robot friend who is amazing at looking at pictures and guessing what's in them. You show it a picture of a Sudoku puzzle (that 9x9 grid where you fill in numbers 1 through 9), and it tries to guess the numbers. This robot is like a Vision-Language Model (VLM). It's great at "seeing" the grid and "reading" the clues, but it has a funny blind spot: it doesn't have a built-in rulebook for logic. It might guess a number that looks right but breaks the rules, like putting two 5s in the same row. It's like a talented artist who can paint a beautiful sky but accidentally paints two suns in the same spot because they forgot the laws of physics.

The paper introduces a new team-up to fix this. They pair the artistic robot with a strict, logical MaxSAT Oracle. Think of the MaxSAT Oracle as a super-organized referee who holds the official rulebook of Sudoku. The referee doesn't try to paint the picture; instead, it watches the robot's guesses and checks them against the rules.

Here is how the team-up works:

The Guess: The robot looks at the puzzle image and suggests where to put numbers.
The Check: The referee takes these suggestions. It treats the Sudoku rules as "hard laws" (you must follow them) and the robot's guesses as "soft suggestions" (we hope they are right, but we can change them if they break the laws).
The Fix: If the robot makes a mistake, the referee doesn't just say "Wrong!" It finds the biggest group of guesses that do work together and tells the robot, "Keep these, but change these specific ones." It then draws a picture on the puzzle showing exactly where the conflict is and explains it in words.
The Retry: The robot looks at the referee's notes, fixes its mistakes, and tries again.

The researchers tested this on a bunch of Sudoku puzzles, ranging from easy to hard. They used three different robots: two open-source ones (named Molmo2 and Qwen3-VL) and one very powerful, closed-source one (GPT-5.5).

What did they find?
Without the referee, the robots often got stuck or filled in numbers that didn't make sense. But when they added the MaxSAT referee:

The robots got much better at following the rules.
They solved way more puzzles. For example, the GPT-5.5 robot, when asked to solve the whole board at once, went from solving 45 puzzles to solving 73 puzzles. Its average completeness (how many cells it got right) jumped from 72.0% to 80.7%.
Even the open-source robots improved, though not quite as much as the big one. Molmo2 went from solving 17 puzzles to 28, and Qwen3-VL went from 10 to 13.

The paper suggests that this teamwork is especially helpful when the robot is almost right but makes a few logical slips. The referee helps clean up those slips to get a perfect solution.

What does the paper say this is NOT?
The authors are very clear: they are not trying to replace the robot with the referee. They aren't saying the referee should solve the puzzle all by itself (which it could do in a few seconds). The goal isn't to beat the referee's speed; it's to see if the referee can teach the robot to be more reliable. They also note that the harder puzzles (labeled "Difficulty 1") were still tougher than the easy ones, but the referee helped the robots handle them much better than before.

In short, the paper shows that giving a visual AI a logical "buddy" to check its work makes it a much better puzzle solver. It's a win for teamwork, proving that mixing a creative guesser with a strict rule-checker creates a smarter system than either could be alone.

Technical Summary: MaxSAT-Based Feedback for Guiding Vision-Language Models in Sudoku

Problem Statement
Vision-Language Models (VLMs) have demonstrated promising capabilities in structured visual reasoning tasks, including grid-based puzzles like Sudoku. However, despite their strong perceptual abilities, VLMs lack explicit mechanisms for enforcing logical consistency. They frequently rely on pattern recognition rather than principled constraint reasoning, leading to outputs that violate structural constraints (e.g., duplicate numbers in rows or columns) or exhibit unstable behavior when attempting to refine incorrect solutions. While Constraint Programming (CP) and Satisfiability (SAT) methods offer formal guarantees of soundness, they lack the perceptual flexibility and proposal-generation capabilities of modern VLMs. This paper addresses the question of whether formal constraint optimization can guide VLMs to solve visual logic puzzles more reliably.

Methodology
The authors propose a hybrid neuro-symbolic framework where a VLM acts as a proposal generator and a Maximum Satisfiability (MaxSAT) oracle acts as a consistency validator and refinement engine. The approach operates through an iterative interaction loop:

Formulation: The Sudoku problem is encoded as a Partial MaxSAT instance.
- Hard Clauses ( $\Phi_h$ ): Encode the fundamental Sudoku constraints (each cell contains exactly one digit; each digit appears exactly once in every row, column, and subgrid). These are non-negotiable.
- Soft Clauses ( $\Phi_s$ ): Encode the candidate placements proposed by the VLM as unit clauses.
Interaction Loop:
- The VLM generates candidate assignments (placing digits in cells) based on the puzzle image.
- These assignments are fed to the MaxSAT solver (specifically the RC2 solver from the PySAT toolkit).
- The solver computes an assignment that satisfies all hard clauses while maximizing the number of satisfied soft clauses (i.e., retaining as many VLM proposals as possible without violating constraints).
- Feedback Generation: If the VLM's proposals are inconsistent, the MaxSAT solver identifies the largest mutually consistent subset of assignments. The rejected assignments (those in the soft clause set but not in the optimal solution) are translated into structured feedback, including textual descriptions of inconsistencies and visual annotations highlighting conflicting cells on the puzzle image.
- The VLM uses this feedback to generate a refined proposal.
Protocols: The framework evaluates two interaction modes:
- Iterative Single-Placement: The VLM proposes one move at a time. MaxSAT validates it; if consistent, it is accepted; otherwise, it is rejected with feedback.
- Full-Board Refinement: The VLM proposes a complete board state. MaxSAT identifies the largest consistent subset of the entire board, rejecting only the conflicting cells, and returns feedback for a global refinement.

Key Contributions

A Neuro-Symbolic Framework: A novel architecture for validating and refining VLM-generated Sudoku solutions using a MaxSAT oracle, establishing a clear division of labor where the neural component handles perception and the symbolic component enforces logical consistency.
Partial MaxSAT Integration: The integration of partial MaxSAT into the VLM solving loop, treating model-generated placements as soft constraints. This allows the system to identify and repair the largest mutually consistent subset of a proposal rather than discarding the entire output.
Empirical Evaluation: A comprehensive evaluation across multiple open-source (Molmo2, Qwen3-VL) and closed-access (GPT-5.5) VLMs on a benchmark Sudoku dataset, demonstrating the efficacy of constraint-guided feedback.

Results
Experiments were conducted on 200 Sudoku instances (100 each of difficulty levels 0 and 1). The results indicate that MaxSAT-based feedback significantly improves logical consistency and solve rates compared to validity-only feedback:

Full-Board Refinement: This mode yielded the strongest gains. For GPT-5.5, the solve rate increased from 22.5% (validity-only) to 36.5% with MaxSAT feedback. The average completeness (AC) of the final board rose from 72.0% to 80.7%. Notably, for harder puzzles (Difficulty 1), the number of solved instances more than doubled (from 10 to 21), and AC improved from 62.2% to 76.7%.
Iterative Solving: MaxSAT feedback also improved step-by-step solving, doubling the number of solved instances for GPT-5.5 (from 21 to 44) and increasing AC from 44.8% to 52.2%.
Model Variance: While all models benefited, the proprietary GPT-5.5 showed the most substantial improvements, suggesting that symbolic refinement is most effective when the initial neural proposals are already close to global consistency. Open-source models showed more modest gains but still demonstrated improved logical consistency.

Significance and Claims
The paper claims that integrating symbolic optimization into the VLM solving loop enhances the reliability of vision-language reasoning without replacing the neural model. The authors emphasize that their goal is not to outperform specialized symbolic solvers (which solve the dataset in seconds), but to study whether symbolic techniques can guide general-purpose VLMs toward consistent solutions.

The findings suggest that symbolic refinement acts as a powerful corrective mechanism, particularly for "globally coherent but partially inconsistent" neural predictions. By delegating logical consistency checking to the MaxSAT oracle, the system ensures that every accepted placement is formally verified. The work highlights the complementary strengths of neural perception and symbolic optimization, advancing the synergy between statistical and symbolic artificial intelligence in structured reasoning tasks. The authors remain modest, noting that while symbolic refinement is not a complete remedy for all VLM limitations, it significantly mitigates logical errors and improves solution quality, especially in full-board scenarios.

More like this