基于 MaxSAT 的反馈引导视觉语言模型解决数独问题

视觉语言模型（VLM）在结构化视觉推理任务中表现优异，但缺乏强制逻辑一致性的机制，常生成违反约束的解。本文提出一种神经符号方法，通过最大可满足性（MaxSAT）预言机将形式化约束推理融入 VLM 求解过程。该符号组件作为一致性验证器与优化引擎，将 VLM 生成的候选位置编码为软子句，数独约束作为硬子句。当出现不一致时，MaxSAT 求解器识别最大一致子集，并转化为结构化文本与视觉反馈以指导后续修正。实验表明，该方法显著提升了逻辑一致性与求解率。