Abstract
Vision-Language Models (VLMs) have recently shown promising performance on structured visual reasoning tasks, including grid-based puzzles. However, despite strong perceptual capabilities, these models lack explicit mechanisms for enforcing logical consistency and frequently generate assignments that violate underlying constraints. In this paper, we propose a neuro-symbolic approach that integrates formal constraint reasoning into the VLM solving process via a Maximum Satisfiability (MaxSAT) oracle.
Method
Rather than computing solutions directly, the symbolic component acts as a consistency validator and refinement engine. Candidate placements generated by the VLM are encoded as soft clauses in a partial MaxSAT formulation, while Sudoku constraints remain hard clauses.
When inconsistencies arise, the MaxSAT solver identifies a largest mutually consistent subset of assignments, which is then translated into structured textual and visual feedback to guide subsequent refinements.
Evaluation
We evaluate our approach on a Sudoku dataset across multiple open-source and closed-access VLMs. Results show that MaxSAT-based feedback improves logical consistency and increases the number of solved instances, particularly in full-board refinement mode.
These findings demonstrate that symbolic optimisation can enhance the reliability of vision-language reasoning.
Blogger's Review: This study successfully enhances the performance of vision-language models in solving Sudoku through the introduction of MaxSAT feedback mechanisms, showcasing the potential of neuro-symbolic methods in complex reasoning tasks, which merits attention for broader applications.