CP-SAT求解器值溢出是否返回INFEASIBILITY及模型扩展咨询

关于变量定义域的纠正 #

CP-SAT的整数变量基于64位有符号整数，最大正取值为9223372036854775807（19位数字），最小负取值为-9223372036854775808。你之前尝试设置18位失败，大概率是因为输入的数值超过了64位有符号整数的上限（比如1000000000000000000是19位数字，超出了上限）。

问题解答 #

• 问题1：当target_prod的值超过其上界时，求解器是否会返回INFEASIBILITY？
  是的。如果模型的约束逻辑推导出target_prod必须大于设定的上界（或小于下界），求解器会直接返回INFEASIBILITY，因为不存在满足所有约束的可行解。

• 问题2：有无方法将乘积分配到多个变量以实现模型的扩展？
  可以通过拆分乘积为多段变量的方式实现，常用两种思路：

  1. 十进制拆分：把大乘积拆分为高位和低位变量，利用算术约束关联。例如计算a * b，拆分出high（高位）和low（低位，存储低k位数值），添加约束：

     model.Add(a * b == high * 10**k + low)
     model.Add(low >= 0)
     model.Add(low < 10**k)
     

  2. 二进制拆分：基于2的幂拆分乘积，利用位运算相关约束关联多个变量，适合需要处理二进制位场景的需求。
     两种方式都能让多个变量共同承载超过单个变量上限的乘积结果。

• 问题3：将定义域改为(-99999999999999999, 99999999999999999)时，求解器是否支持该设置？
  完全支持。这个范围落在CP-SAT 64位有符号整数的取值区间内，直接用以下代码创建变量即可：

  target_prod = model.NewIntVar(-99999999999999999, 99999999999999999, 'target_prod')
  

  求解器可以正常处理带符号的整数乘积约束。

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