如何定位CP-SAT求解器因参数调整导致INFEASIBLE的约束/变量？

当前日志无法直接定位导致不可行的具体约束或变量，原因如下：

• 不可行性是在预求解阶段的探测（probing）步骤中被发现，但日志未输出具体冲突的约束或变量信息。
• SufficientAssumptionsForInfeasibility = [] 表明求解器未生成不可行性的充分假设集，无法直接回溯到原始冲突约束。
• 预求解阶段执行了大量模型化简操作（如线性化、变量域缩减、等价约束替换等），原始约束已被转换或合并，日志中的预求解规则应用记录仅反映化简过程，无法对应到原始模型的具体约束。

可行的排查方法 #

• 给关键约束添加假设标记：针对与调整参数相关的核心约束，添加假设（Assumptions）并启用求解器的不可行性证明生成功能，求解器会返回导致不可行的假设子集，以此对应到原始约束。
• 逐步简化模型定位：
  • 先保留与调整参数直接相关的约束，移除非核心约束，验证是否仍不可行，逐步缩小排查范围。
  • 将参数从可行值逐步增大，找到刚好触发不可行的临界点，分析该点下约束的逻辑矛盾。
• 启用详细日志：调整求解器参数，开启log_presolve_details为true，获取预求解和探测阶段的变量域变化、约束推导细节，从中寻找冲突线索。
• 重点检查参数关联约束：聚焦依赖该参数的约束（如参数作为上下限、参与乘积/除法运算的约束），检查参数增大后是否导致变量域出现互斥要求（如变量需同时满足x > A和x < B且A >= B）。

内容的提问来源于stack exchange，提问作者Ken Adams