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

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

REVIEW 4 major objections 4 minor 1 cited by

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

T0 review · 4 major / 4 minor · reviewed 2026-08-02 · deepseek-v4-flash

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

Pith's one-line read A partial MaxSAT oracle that returns the largest mutually consistent subset of a vision-language model's Sudoku placements lifts solved puzzles from 45 to 73 for the strongest model, and improves every tested model.

desk verdict Strong empirical template with a core formal gap: the paper never says the puzzle's givens are hard clauses, so the 'formally verified' claim is not established. read the letter →

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

Pedro Orvalho , Guillem Alenyà , Felip Manyà This is my paper · ORCID

classification cs.AIcs.LO

keywords MaxSATPartialNeuro-symbolicAIVision-languagemodelSudokuLogicalconsistencyConstraintsatisfactionFeedbackrefinement

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper tries to establish that a formal constraint-optimization layer can repair the structured outputs of vision-language models. The authors encode Sudoku rules as hard clauses and each VLM-proposed digit placement as a soft clause in a partial MaxSAT instance; each round, the solver keeps the largest consistent portion of the model's placements and turns the rejected ones into textual and visual feedback for the next attempt. On 200 puzzles across three VLMs, every model improves on both solved instances and average completeness when feedback is MaxSAT-based rather than validity-only, with the strongest result being the full-board mode of the best-performing model, which rises from 45 to 73 solved puzzles and from 72.0% to 80.7% completeness. If this is right, a cheap symbolic oracle can turn near-miss neural predictions into formally certified solutions while keeping the VLM as the primary reasoning agent.

What carries the argument

The load-bearing object is the partial MaxSAT formulation. Hard clauses encode the generic Sudoku constraints (each cell exactly one digit, each digit once per row, column, and 3x3 subgrid), and soft unit clauses encode the VLM's proposed placements. The MaxSAT solver returns an assignment that satisfies all hard clauses and violates as few soft clauses as possible; the violated soft clauses point to a minimal set of conflicting placements, which become the corrective feedback. This turns a single binary validity check into an optimisation that identifies the most plausible consistent subset and tells the model where it went wrong.

What would settle it

Inspect the input to the MaxSAT solver for a specific puzzle: if the initial clues are not present as hard unit clauses, the solver will return a valid Sudoku board that can disagree with the image's givens; a single such accepted board would refute the claim that every accepted placement is formally verified. A re-run of the full-board experiment with the clues deliberately excluded from the hard clauses would show this directly.

Watch

Extended reading notes

Core claim

The central claim is that integrating partial MaxSAT into the VLM solving loop significantly improves logical consistency, robustness, and solution quality. The mechanism is a neuro-symbolic interaction loop: the VLM proposes placements, the MaxSAT oracle finds an assignment that satisfies all Sudoku constraints while maximising agreement with the proposals, and the placements it rejects are converted into structured feedback. In full-board mode, the oracle extracts the largest mutually consistent subset of the proposed complete board. The empirical evaluation shows that every tested VLM improves under MaxSAT feedback in both step-by-step and full-board modes, with the largest gain when the

Load-bearing premise

The load-bearing premise, left unstated in Sections 3 and 4, is that the puzzle's given clues and any already-accepted placements are encoded as hard clauses in the MaxSAT formulation; the text only documents the generic cell/row/column/subgrid constraints as hard, so without the givens the oracle could certify a valid Sudoku board that does not match the puzzle.

Editorial extensions

If this is right

The gain is achieved purely at inference time; no VLM retraining or fine-tuning is required, so the approach can be bolted onto any existing model that can output structured placements.
Full-board refinement outperforms step-by-step interaction, indicating that a globally structured but imperfect prediction is easier for MaxSAT to repair than a sequence of single placements.
MaxSAT feedback shrinks the difficulty gap: for the strongest model, difficulty-1 solved instances more than double (from 10 to 21 in full-board mode), and average completeness on hard puzzles rises from 62.2% to 76.7%.
The effectiveness of the oracle depends on the quality of the initial proposal: the proprietary model, which is already closer to global consistency, benefits far more than the open-source models, suggesting that symbolic refinement amplifies existing competence rather than replacing it.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The paper never states that the puzzle's given clues are encoded as hard clauses in the MaxSAT formulation; if they are not, the oracle could certify a valid Sudoku board that disagrees with the image. This is an omitted implementation detail that is load-bearing for the claim that every accepted placement is formally verified.
A testable extension is to feed the same loop different structured puzzles—Kakuro, KenKen, or nonograms—whose rules are also easily expressed as hard clauses; the predicted pattern is the same: large gains when the VLM is near-consistent, smaller gains when it is far off.
Because the symbolic layer is cheap, a natural next step is to ask the VLM for several alternative full-board proposals per round and let the MaxSAT oracle pick the best consistent subset, increasing the chance of finding a complete solution per API call.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Desk Editor's Note

read the letter

Here's the quick take: the idea is a good one and the empirical gains look plausible, but the paper hasn't actually specified the formal model it relies on. The MaxSAT oracle is supposed to verify VLM proposals against the puzzle, yet the hard clauses are defined only for the generic Sudoku rules—cells, rows, columns, subgrids. The given clues never appear as hard units, and the iterative loop doesn't say whether accepted placements are added to the hard set. Without that, 'formally verified' can't mean what the paper says it means.

What's new and worth noticing: the partial-MaxSAT-as-feedback setup, where the oracle returns the largest consistent subset of the VLM's proposed moves, is a clean template. It's not in the cited prior work, which mostly targets text-based LLM+solver pipelines or MaxSAT for code repair. The evaluation is systematic across three VLMs, two interaction modes, and 200 puzzles, and the pattern is consistent: every model improves on both solve rate and completeness with MaxSAT feedback. GPT-5.5 going from 45 to 73 solved in full-board mode is a big jump.

The soft spots are real. The biggest is the encoding gap I already mentioned. I think the solve-rate numbers are probably not inflated—since the final board is compared to ground truth, returning a different valid board would fail the AC check—but the feedback signals could be wrong if the oracle doesn't know the givens, and the paper's core guarantee is unverified. The authors need to state explicitly that givens are hard clauses and that accepted placements in step-by-step mode become hard units, or the claim should be softened. Second, the baseline is weak: validity-only feedback says 'your placement is logically incorrect' with no conflict information, while MaxSAT feedback names the conflicting cells and highlights them visually. Part of the gain could just be more informative feedback, not specifically the MaxSAT subset selection. A control with random or generic conflict hints would separate those. Third, there's no code or exact rendering details, so independent replication is hard. Temperature zero makes error bars unnecessary, but I'd still like a few details on image preprocessing and how the board state is represented.

This is written for people working on neuro-symbolic VLM systems who want a quick way to inject hard constraints into a perception loop. It's a reasonable contribution to that subfield.

I'd send it to peer review, but I'd ask for a revised manuscript that fixes the formal encoding, adds the control, and releases the artifacts. The idea is useful enough that it deserves the feedback.

Referee Report

4 major / 4 minor

Summary. The paper proposes a neuro-symbolic Sudoku-solving loop in which a VLM reads a Sudoku image and proposes placements, and a partial MaxSAT oracle treats those placements as soft unit clauses while Sudoku constraints are hard. The solver returns a largest mutually consistent subset; conflicts are translated into textual/visual feedback, and the loop repeats in either step-by-step (single placement per iteration) or full-board (complete board per iteration) mode. The authors evaluate GPT-5.5, Molmo2, and Qwen3-VL on 200 puzzles (100 difficulty 0 and 100 difficulty 1), comparing validity-only feedback with MaxSAT feedback. They report improvements in solved instances and average completeness, with the strongest gains for GPT-5.5 in full-board mode (45 to 73 solved; AC 72.0% to 80.7%). The central claim is that integrating partial MaxSAT into the VLM loop significantly improves logical consistency, robustness, and solution quality.

Significance. If the results hold, the paper provides a useful controlled demonstration of how a formal oracle can refine VLM-generated structured outputs, with a clean division of labor: the VLM proposes, the MaxSAT oracle validates and provides corrective feedback. The fixed dataset split, multiple VLMs, and comparison against validity-only feedback are strengths. The paper does not overclaim competitiveness with symbolic solvers. However, the formal verification guarantee is underspecified: the encoding as written omits puzzle givens and does not state that accepted placements become hard clauses, which directly affects whether the results measure solving the presented puzzles. In addition, the empirical claims are based on point estimates without uncertainty quantification. These issues are load-bearing but appear fixable in revision.

major comments (4)

[§3, §4.2] The formal encoding omits the puzzle givens. Section 3 defines hard clauses only for cell, row, column, and subgrid constraints; Section 4 states that Φ_h contains 'the hard clauses encoding all Sudoku constraints' but never states that each given digit is encoded as a unit hard clause. Without this, the MaxSAT oracle can certify a valid 9×9 Sudoku grid that is not the unique solution of the presented puzzle. Consequently, 'every accepted placement is formally verified' is only verification against generic Sudoku rules, not against the actual puzzle, and the solved/AC metrics in Table 1 become ambiguous. Please state explicitly, and ensure in the implementation, that the givens are hard clauses.
[§4.1] In iterative mode, an accepted placement is 'permanently added to the board state' but the manuscript never says it is added to Φ_h. If it is not, later MaxSAT optima may violate an earlier accepted placement, because soft unit clauses can be dropped when a new conflicting placement is proposed. The guarantee that 'every accepted placement is formally verified' is then only per-step and not cumulative. Specify whether accepted placements become hard clauses; if they do not, the formal verification claim is false.
[§5.4, Table 1] All conclusions rest on point estimates without uncertainty quantification. For example, the full-board MaxSAT vs validity-only comparison for Qwen3-VL is 13 vs 10 solved puzzles out of 200; the paper reports no confidence intervals, standard errors, or hypothesis tests. The phrase 'significantly improves' in Section 5.5 is therefore not supported statistically. Add confidence intervals or significance tests (e.g., McNemar's test for paired solve counts), or soften the causal claims to observed improvements.
[§4.2, §5.4] The metric 'solved' is never defined in Section 5.4. If 'solved' means average completeness of 100%, then a MaxSAT output that satisfies only the generic Sudoku constraints but disagrees with the givens will not be counted as solved; however, the termination condition in Section 4.2 treats any 'complete and logically consistent solution' as success. This mismatch needs to be resolved, and the definition of 'solved' should be stated explicitly (e.g., full match to the ground-truth solution).

minor comments (4)

[§3] The subgrid constraint formula appears to be missing summation notation or is poorly rendered; please fix the typesetting so the at-most-one/at-least-one encoding is unambiguous.
[§5.3] Qwen3-VL is cited to reference [31], which is a Qwen3 Technical Report; please verify that this is the correct citation for the VLM variant used.
[Appendix A] The validity-only feedback prompt says 'Your placement is logically incorrect' but does not explain how validity is checked. If it uses the same MaxSAT oracle or a lighter local check, this should be stated to make the comparison meaningful.
[§5.2] The statement that the MaxSAT solver solves all instances 'in a few seconds' would benefit from a precise average or maximum runtime, especially since the paper does not report computational overhead of the feedback loop.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the MaxSAT-feedback gains are empirical and benchmarked against ground truth; the only self-citations are contextual and not load-bearing.

full rationale

The paper's central claim is an empirical intervention: a VLM proposes placements, a MaxSAT oracle validates/refines them, and performance is measured by solved-instance count and average completeness against the dataset's ground-truth solutions (Section 5.2, Table 1). No parameter is fitted to the test data, and no predicted quantity is defined as the same quantity being derived. The MaxSAT encoding in Section 3 is standard and attributed to an external source [19]; the soft clauses are exactly the VLM's proposed placements, so the oracle's accepted subset is not a free construction equivalent to the input. The only self-references are [23,24] in the related-work paragraph on MaxSAT-guided neural systems; they motivate the research line but do not support the present empirical results, so they are not load-bearing circularity. One specification gap is worth flagging as a correctness risk, not as circularity: Sections 3 and 4 never explicitly state that puzzle givens or previously accepted placements are encoded as hard clauses, so if the implementation follows the text literally, the oracle could certify a board satisfying generic Sudoku constraints but not the actual givens, threatening the external validity of 'solved' counts. However, full-board completion still requires the VLM to propose a complete assignment, and the reported AC metric is anchored to ground-truth solutions; hence the claimed improvement does not reduce by construction to the MaxSAT oracle's own output. The derivation chain is therefore self-contained with respect to circularity.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The central empirical claim rests on a standard SAT encoding, dataset correctness, and parseable VLM output, plus two unstated implementation assumptions: puzzle givens must be hard clauses, and accepted placements must become hard clauses in the iterative loop. No new physical or mathematical entities are introduced, and no parameters are fitted to data.

assumptions (5)

standard math The standard exactly-one CNF encoding of Sudoku constraints is logically faithful.
Section 3 uses pairwise at-least-one and at-most-one clauses; this is a well-known encoding.
domain assumption The dataset provides correct difficulty labels and unique ground-truth solutions corresponding to the puzzle images.
Section 5.2 defines 'solved' as matching ground truth on the HuggingFace dataset subset.
ad hoc to paper The puzzle's given clues are included as hard clauses in the implementation.
Never stated in Sections 3-4; without it, the oracle can certify valid Sudoku boards that do not match the given puzzle.
ad hoc to paper Already-accepted placements are made hard clauses in the step-by-step loop.
Section 4.1 says accepted placements are 'permanently added' but only describes adding soft clauses to the MaxSAT instance.
domain assumption VLM outputs parse reliably into the required <ANSWER> placement format.
Appendix A defines the format, but the paper reports no parsing success rate or handling of malformed outputs.

how reviews work

0 comments

Cite this review

Pith. "Pith review of MaxSAT-Based Feedback for Guiding Vision-Language Models in Sudoku." pith.science (2026). https://pith.science/paper/RXZM7NFH

@misc{pith2026260712711,
  author       = {Pith},
  title        = {Pith review of: MaxSAT-Based Feedback for Guiding Vision-Language Models in Sudoku},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/RXZM7NFH}},
  note         = {Machine review of arXiv:2607.12711}
}

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.

Figures

Figures reproduced from arXiv: 2607.12711 by the authors.

**Figure 1.** Neuro-symbolic interaction loop for Sudoku solving. The VLM proposes candidate placements, which are validated by a MaxSAT oracle. When conflicts are detected, constraint-derived feedback is highlighted in the puzzle and returned to guide subsequent refinements. – Row Constraints. Each digit must appear exactly once in every row: ∀r, d ∈ {1, . . . , n} : Pn c=1 Xr,c,d = 1. – Column Constraints. Each digit must app… view at source ↗

Review history (2 revisions) →

Discussion (0). Continue with ORCID to comment.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Recursive Vision Language Models for General Symbolic Reasoning
cs.CV 2026-08 conditional novelty 5.0 of 10

R-Qwen, a LoRA-adapted Qwen model that iteratively refines explicit candidate solutions under constraint projection, outperforms prior recursive models and zero-shot frontier LLMs on eight symbolic reasoning benchmarks.

Reference graph

Works this paper leans on

33 extracted references · 3 linked inside Pith · cited by 1 Pith paper

[1]

In: Biere, A., Heule, M., van Maaren, H., Walsh, T

Bacchus, F., Järvisalo, M., Martins, R.: Maximum satisfiability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 929–991. IOS Press (2021)

2021
[2]

(eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol

Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)

2009
[3]

In: ECAI

Bogaerts, B., Gamba, E., Claes, J., Guns, T.: Step-wise explanations of constraint satisfaction problems. In: ECAI. vol. 325, pp. 640–647. IOS Press (2020)

2020
[4]

arXiv preprint arXiv:2601.10611 (2026)

Clark, C., Zhang, J., Ma, Z., Park, J.S., Salehi, M., Tripathi, R., Lee, S., Ren, Z., Kim, C.D., Yang, Y., et al.: Molmo2: Open weights and data for vision-language models with video understanding and grounding. arXiv preprint arXiv:2601.10611 (2026)

arXiv 2026
[5]

CoRRabs/2511.10436(2025)

Foschini, M., Defresne, M., Gamba, E., Bogaerts, B., Guns, T.: Preference elicita- tion for step-wise explanations in logic puzzles. CoRRabs/2511.10436(2025)

arXiv 2025
[6]

In: ICML

Gao, L., Madaan, A., Zhou, S., Alon, U., Liu, P., Yang, Y., Callan, J., Neubig, G.: Pal: Program-aided language models. In: ICML. pp. 10764–10799. PMLR (2023)

2023
[7]

Guns, T., Gamba, E., Mulamba, M., Bleukx, I., Berden, S., Pesa, M.: Sudoku assistant-anai-poweredapptohelpsolvepen-and-papersudokus.In:AAAI(2023)

2023
[8]

In: NAACL (2025)

Hao, Y., Chen, Y., Zhang, Y., Fan, C.: Large language models can solve real-world planning rigorously with formal verification tools. In: NAACL (2025)

2025

Show all 33 references

[9]

In: ICLR (2025)

Hao, Y., Zhang, Y., Fan, C.: Planning anything with rigor: General-purpose zero- shot planning with llm-based formalized programming. In: ICLR (2025)

2025
[10]

HuggingFace: .https://huggingface.co(2026), [Online; accessed 15-May-2026]

2026
[11]

from HuggingFace, S.D.: .https://huggingface.co/datasets/Ritvik19/ Sudoku-Dataset(2026), [Online; accessed 15-May-2026]

2026
[12]

In: IJCAI

Ignatiev, A.: Towards trustable explainable AI. In: IJCAI. pp. 5154–5158 (2020)

2020
[13]

In: SAT (2018)

Ignatiev, A., Morgado, A., Marques-Silva, J.: PySAT: A python toolkit for proto- typing with SAT oracles. In: SAT (2018)

2018
[14]

Ignatiev, A., Morgado, A., Marques-Silva, J.: RC2: an efficient MaxSAT solver. J. Satisf. Boolean Model. Comput.11(1), 53–64 (2019) MaxSAT-Based Feedback for Guiding Vision-Language Models in Sudoku 13

2019
[15]

In: IJCAR (2018)

Ignatiev, A., Pereira, F., Narodytska, N., Marques-Silva, J.: A sat-based approach to learn explainable decision sets. In: IJCAR (2018)

2018
[16]

In: ICML (2024)

Kambhampati, S., Valmeekam, K., Guan, L., Verma, M., Stechly, K., Bhambri, S., Saldyt, L.P., Murthy, A.B.: Position: Llms can’t plan, but can help planning in llm-modulo frameworks. In: ICML (2024)

2024
[17]

In: Handbook of satisfia- bility, pp

Li, C.M., Manya, F.: Maxsat, hard and soft constraints. In: Handbook of satisfia- bility, pp. 613–631. IOS Press (2009)

2009
[18]

In: ICML (2025)

Lin, B.Y., Le Bras, R., Richardson, K., Sabharwal, A., Poovendran, R., Clark, P., Choi, Y.: Zebralogic: On the scaling limits of llms for logical reasoning. In: ICML (2025)

2025
[19]

In: International Symposium on Artificial Intelligence and Mathematics (2006)

Lynce, I., Ouaknine, J.: Sudoku as a SAT problem. In: International Symposium on Artificial Intelligence and Mathematics (2006)

2006
[20]

Frontiers Artif

Marques-Silva, J., Ignatiev, A.: No silver bullet: interpretable ML models must be explained. Frontiers Artif. Intell.6(2023)

2023
[21]

Constraints An Int

Mulamba, M., Mandi, J., Mahmutogullari, A.I., Guns, T.: Perception-based con- straint solving for sudoku images. Constraints An Int. J.29(1-2), 112–151 (2024)

2024
[22]

OpenAI: GPT5.5https://openai.com/index/introducing-gpt-5-5/(2026), re- leased: 2026-04-23

2026
[23]

In: AAAI (2025)

Orvalho, P., Janota, M., Manquinho, V.M.: Counterexample Guided Program Re- pair Using Zero-Shot Learning and MaxSAT-based Fault Localization. In: AAAI (2025)

2025
[24]

CoRRabs/2508.08171(2025)

Orvalho, P., Kwiatkowska, M.: PyVeritas: On Verifying Python via LLM-Based Transpilation and Bounded Model Checking for C. CoRRabs/2508.08171(2025)

2025 arXiv
[25]

In: EMNLP (2023)

Pan, L., Albalak, A., Wang, X., Wang, W.: Logic-lm: Empowering large language models with symbolic solvers for faithful logical reasoning. In: EMNLP (2023)

2023
[26]

(eds.): Handbook of Constraint Programming, Foundations of Artificial Intelligence, vol

Rossi, F., van Beek, P., Walsh, T. (eds.): Handbook of Constraint Programming, Foundations of Artificial Intelligence, vol. 2. Elsevier (2006)

2006
[27]

Shi, W., Liu, M., Zhang, W., Shi, L., Jia, F., Ma, F., Zhang, J.: Constraintllm: A neuro-symbolicframeworkforindustrial-levelconstraintprogramming.In:EMNLP (2025)

2025
[28]

In: NeurIPS 2025 (2025)

Shojaee, P., Mirzadeh, I., Alizadeh, K., Horton, M., Bengio, S., Farajtabar, M.: The illusion of thinking: Understanding the strengths and limitations of reasoning models via the lens of problem complexity. In: NeurIPS 2025 (2025)

2025
[29]

Sudoku: .https://en.wikipedia.org/wiki/Sudoku(2026), [Online; accessed 15- May-2026]

2026
[30]

In: NeurIPS (2025)

Xu, J., Fei, H., Zhang, Y., Pan, L., Huang, Q., Liu, Q., Nakov, P., Kan, M.Y., Wang, W.Y., Lee, M.L., et al.: Muslr: Multimodal symbolic logical reasoning. In: NeurIPS (2025)

2025
[31]

arXiv preprint arXiv:2505.09388 (2025)

Yang, A., Li, A., Yang, B., Zhang, B., Hui, B., Zheng, B., Yu, B., Gao, C., Huang, C., Lv, C., et al.: Qwen3 technical report. arXiv preprint arXiv:2505.09388 (2025)

2025 arXiv
[32]

IEICE transactions on fundamentals of electronics, com- munications and computer sciences (2003)

Yato, T., Seta, T.: Complexity and completeness of finding another solution and its application to puzzles. IEICE transactions on fundamentals of electronics, com- munications and computer sciences (2003)

2003
[33]

NeurIPS (2023) 14 P

Ye, X., Chen, Q., Dillig, I., Durrett, G.: Satlm: Satisfiability-aided language models using declarative prompting. NeurIPS (2023) 14 P. Orvalho, et al. A Prompt Templates This appendix presents the prompt templates used to evaluate Vision–Language Models across the Sudoku sol...

2023

Pith tools

Reviewed August 2, 2026 · model on record in the stance chip above.

[1] [1]

In: Biere, A., Heule, M., van Maaren, H., Walsh, T

Bacchus, F., Järvisalo, M., Martins, R.: Maximum satisfiability. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability - Second Edition, Frontiers in Artificial Intelligence and Applications, vol. 336, pp. 929–991. IOS Press (2021)

2021

[2] [2]

(eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol

Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. IOS Press (2009)

2009

[3] [3]

In: ECAI

Bogaerts, B., Gamba, E., Claes, J., Guns, T.: Step-wise explanations of constraint satisfaction problems. In: ECAI. vol. 325, pp. 640–647. IOS Press (2020)

2020

[4] [4]

arXiv preprint arXiv:2601.10611 (2026)

Clark, C., Zhang, J., Ma, Z., Park, J.S., Salehi, M., Tripathi, R., Lee, S., Ren, Z., Kim, C.D., Yang, Y., et al.: Molmo2: Open weights and data for vision-language models with video understanding and grounding. arXiv preprint arXiv:2601.10611 (2026)

arXiv 2026

[5] [5]

CoRRabs/2511.10436(2025)

Foschini, M., Defresne, M., Gamba, E., Bogaerts, B., Guns, T.: Preference elicita- tion for step-wise explanations in logic puzzles. CoRRabs/2511.10436(2025)

arXiv 2025

[6] [6]

In: ICML

Gao, L., Madaan, A., Zhou, S., Alon, U., Liu, P., Yang, Y., Callan, J., Neubig, G.: Pal: Program-aided language models. In: ICML. pp. 10764–10799. PMLR (2023)

2023

[7] [7]

Guns, T., Gamba, E., Mulamba, M., Bleukx, I., Berden, S., Pesa, M.: Sudoku assistant-anai-poweredapptohelpsolvepen-and-papersudokus.In:AAAI(2023)

2023

[8] [8]

In: NAACL (2025)

Hao, Y., Chen, Y., Zhang, Y., Fan, C.: Large language models can solve real-world planning rigorously with formal verification tools. In: NAACL (2025)

2025