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

Felip Many\`a; Guillem Aleny\`a; Pedro Orvalho

MaxSAT feedback turns VLM Sudoku guesses into a largest consistent subset and guides refinements until more boards solve.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · grok-4.5

2026-07-15 03:55 UTC pith:RXZM7NFH

load-bearing objection Abstract-only neuro-symbolic VLM+MaxSAT feedback for Sudoku; plausible method, uncheckable empirical claim until numbers and ablations appear. the 3 major comments →

arxiv 2607.12711 v2 pith:RXZM7NFH submitted 2026-07-14 cs.AI cs.LO

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

Pedro Orvalho , Guillem Aleny\`a , Felip Many\`a This is my paper

classification cs.AI cs.LO

keywords MaxSATvision-language modelsSudokuneuro-symbolic reasoningconstraint feedbacklogical consistencypartial MaxSATvisual reasoning

verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Vision-language models can read Sudoku grids and propose cell placements, yet they routinely break the game rules because they have no built-in logical checker. This paper claims that a Maximum Satisfiability (MaxSAT) oracle can fix that gap without replacing the model: every candidate placement the VLM suggests becomes a soft clause, while the true Sudoku rules stay hard clauses. When the board is inconsistent the solver returns the largest mutually consistent subset of those placements; that subset is turned into short textual and visual feedback that the VLM uses on the next pass. The authors report that the loop measurably raises logical consistency and the number of fully solved boards, especially when the model is allowed to revise the entire grid at once. A sympathetic reader cares because the same pattern—soft model proposals plus hard domain constraints—could be reused for any visual reasoning task that has a clear formal specification.

Core claim

Encoding VLM candidate placements as soft clauses and Sudoku constraints as hard clauses lets a partial MaxSAT solver extract a largest consistent subset; converting that subset into structured textual and visual feedback measurably improves both logical consistency and the number of fully solved Sudoku instances, particularly under full-board refinement.

What carries the argument

Partial MaxSAT formulation in which VLM assignments are soft clauses and Sudoku rules are hard clauses; the solver returns a maximum-cardinality consistent subset that is rendered as the next round of feedback.

Load-bearing premise

That the largest mutually consistent subset of the model’s own guesses, once shown back as text and images, gives the VLM enough signal to fix remaining errors instead of reintroducing new ones or stalling.

What would settle it

Run the same VLMs on a held-out Sudoku set with and without the MaxSAT feedback loop; if the number of fully solved boards and the rate of constraint violations do not improve under full-board refinement, the central claim fails.

Watch this falsifier — get emailed when new claim-graph text bears on it.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Desk Editor's Note

Abstract-only neuro-symbolic VLM+MaxSAT feedback for Sudoku; plausible method, uncheckable empirical claim until numbers and ablations appear.

read the letter

The one thing to know: this is a clean neuro-symbolic loop for Sudoku—VLM proposals as soft clauses, Sudoku rules as hard, MaxSAT returning a largest consistent subset as textual/visual feedback—and the abstract claims better consistency and more solved boards, especially in full-board mode. That is the whole paper as we have it.

What is actually new is the specific integration and the feedback framing, not the ingredients. VLMs plus SAT/MaxSAT oracles and iterative tool use already exist; encoding model outputs soft and domain constraints hard is the natural formulation. Still, treating the solver as a refinement engine rather than a pure solver, and closing the loop with structured feedback, is a legitimate methodological contribution for the structured-visual-reasoning niche. Circularity is not the issue: the hard constraints are external and independent.

The soft spot is exactly the one the stress-test flags, and it is load-bearing. We have no numbers, baselines, error bars, or ablation of feedback versus pure MaxSAT post-filtering. If the gains mostly come from the oracle discarding inconsistent cells rather than the VLM actually revising its next generation from the feedback, the “guiding” claim collapses to ordinary constraint filtering. The abstract’s weakest assumption—that the consistent subset is informative enough for the model to correct rather than re-introduce errors or stall—is untested in the text we have. Soundness is therefore provisional; the claim is only weakly supported until the full experiments land.

Who it is for: people already working on tool-augmented VLMs or neuro-symbolic constraint reasoning on visual puzzles. Not a foundational change to VLMs or combinatorial optimisation. It deserves a serious referee once the full paper, metrics, and preferably code/data are available; abstract-only is not enough to desk-accept, but the setup is coherent enough that I would not desk-reject on principle. I would not bring it to reading group yet and would not cite it until I can see the tables. If the ablations cleanly separate guidance from filtering and the gains hold across models, it becomes a useful citation in that niche. For now: wait for the full text, then send to review.

Referee Report

3 major / 3 minor

Summary. The manuscript proposes a neuro-symbolic pipeline in which a Vision–Language Model proposes Sudoku cell assignments that are encoded as soft clauses in a partial MaxSAT instance, while the standard Sudoku rules remain hard clauses. When the soft set is inconsistent with the hard constraints, the MaxSAT solver returns a largest mutually consistent subset of the VLM’s assignments; that subset is rendered as structured textual and visual feedback to drive iterative refinement. The abstract reports that this MaxSAT-based feedback improves logical consistency and raises the number of fully solved boards across multiple open-source and closed-access VLMs, with the largest gains claimed in a full-board refinement mode.

Significance. If the empirical claims survive proper controls, the work would supply a clean, reusable pattern for using symbolic optimisation as a refinement engine rather than a pure post-hoc filter for VLMs on constraint-heavy visual tasks. The soft/hard clause separation is conceptually sound and non-circular: Sudoku rules are independent of the model, and MaxSAT maximises consistency against those external rules. Multi-VLM evaluation and dual textual/visual feedback are strengths worth retaining. The contribution’s weight, however, rests entirely on whether the reported gains are caused by the VLM actually using the feedback, which the abstract alone cannot establish.

major comments (3)

[Abstract] The central empirical claim—that MaxSAT-based feedback improves logical consistency and increases solved instances—cannot be evaluated from the abstract. No success rates, baselines, absolute or relative gains, error bars, or statistical tests are supplied. Without these quantities the claim remains an assertion rather than a result.
[Abstract] The load-bearing causal claim is that structured MaxSAT feedback guides subsequent VLM refinements. The abstract does not describe an ablation that separates (i) iterative VLM generation conditioned on MaxSAT feedback from (ii) single-shot VLM output followed by pure MaxSAT filtering of inconsistent cells. If gains largely reduce to (ii), the neuro-symbolic “guiding” contribution collapses to ordinary constraint post-processing. This control is essential for the paper’s thesis.
[Abstract] The method rests on the assumption that the largest mutually consistent subset, once translated into textual and visual feedback, is informative enough for the VLM to correct remaining errors rather than re-introduce inconsistencies or stall. The abstract reports neither iteration statistics, failure-mode analysis, nor cases in which feedback is ignored or harmful. Without that evidence the weakest link of the pipeline is untested.

minor comments (3)

[Abstract] “Particularly in full-board refinement mode” implies multiple operating modes; these modes should be named and briefly defined already in the abstract so readers can interpret the claimed differential gains.
[Abstract] The abstract refers to “multiple open-source and closed-access VLMs” without naming them; listing the models (or at least their families and scales) would let readers judge the breadth of the evaluation.
[Abstract] Hyphenation of “Vision–Language” / “vision-language” should be made consistent once the full manuscript is available.

Circularity Check

0 steps flagged

No circularity: MaxSAT feedback uses external Sudoku hard constraints; abstract-only review finds no self-definitional or fitted-prediction loop.

full rationale

Only the abstract is available. The claimed method encodes VLM candidate placements as soft clauses and Sudoku rules as hard clauses; the partial MaxSAT solver returns a largest mutually consistent subset that is rendered as textual/visual feedback for the VLM. Sudoku constraints are independent external rules, not defined from the VLM outputs or from any fitted target of the paper. No equations, uniqueness theorems, self-citations, or parameter fits appear in the abstract that would make a reported 'prediction' or 'first-principles result' equivalent to its inputs by construction. Empirical gains (improved consistency, more solved instances) are presented as experimental outcomes against external VLM baselines, not as tautologies. Residual experimental risks (e.g., feedback-format tuning) cannot be verified from the abstract and do not constitute circularity under the stated criteria. Therefore score 0 with empty steps is the correct finding.

Axiom & Free-Parameter Ledger

0 free parameters · 3 axioms · 0 invented entities

Abstract-only; no free parameters, formal axioms, or invented entities are introduced beyond standard MaxSAT and Sudoku. The method relies on ordinary domain assumptions that Sudoku rules are correctly encodable as hard clauses and that VLMs can consume structured feedback.

axioms (3)

domain assumption Sudoku row/column/block uniqueness and given-cell constraints can be encoded as hard clauses in a partial MaxSAT instance.
Standard and well-known; required for the hard-clause side of the formulation.
domain assumption VLM-generated candidate placements can be treated as soft clauses whose weights reflect model confidence or uniform preference.
Core modelling choice stated in the abstract; weight assignment details are not given.
ad hoc to paper A largest consistent subset of soft assignments, rendered as text/visual feedback, is useful for subsequent VLM refinement.
Empirical hypothesis of the feedback loop; not independently justified in the abstract.

pith-pipeline@v1.1.0-grok45 · 6104 in / 2125 out tokens · 14834 ms · 2026-07-15T03:55:56.977337+00:00 · methodology

0 comments

read the original abstract

Vision--Language Models (VLMs) have recently demonstrated 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. 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. 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.

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

Core claim

What carries the argument

Load-bearing premise

What would settle it

discussion (0)