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

Research Approach

This paper introduces a neuro-symbolic framework designed to address the tendency of Vision-Language Models (VLMs) to generate logically inconsistent outputs when solving grid-based puzzles like Sudoku. While VLMs excel at perceptual tasks, they lack built-in mechanisms for formal logic. The authors propose a hybrid architecture where a VLM acts as a proposal generator, and a Maximum Satisfiability (MaxSAT) oracle acts as a consistency validator and refinement engine.

Methodology

The system operates by encoding Sudoku rules as hard clauses and VLM-generated digit placements as soft clauses within a partial MaxSAT formulation. When the VLM proposes a board configuration, the MaxSAT solver identifies the largest subset of these placements that satisfies all Sudoku constraints. If inconsistencies are found, the system translates the solver's output into structured textual and visual feedback, highlighting the conflicting cells. This feedback is then fed back to the VLM to guide iterative refinement until a valid solution is reached or a termination condition is met.

Key Findings

The researchers evaluated this approach using both open-source (Qwen3-VL, Molmo2) and closed-access (GPT-5.5) models on a benchmark dataset. The results demonstrate that MaxSAT-based feedback consistently improves both the number of solved instances and the overall logical completeness of the boards. The most significant gains were observed in the full-board refinement mode, where the symbolic oracle effectively repaired globally inconsistent neural predictions. The approach proved particularly effective at helping models recover from errors in more difficult puzzle instances.

This work provides a scalable template for enhancing the reliability of general-purpose VLMs in domains requiring strict adherence to formal rules. By offloading logical verification to a symbolic solver, the framework allows neural models to focus on their strengths—perception and heuristic generation—without needing to be retrained for logical consistency. This demonstrates that neuro-symbolic integration is a viable path toward making large-scale vision models more robust for structured reasoning tasks.