在MiniZinc中如何表达特定砝码组合的存在性约束？

首先明确称重逻辑：这类谜题中砝码可放在物品同侧（抵消重量）、配重侧（增加配重）或不使用，对应每个砝码的状态为-1、0、1。我们需要确保对1到40的每一个重量w，都存在一组状态组合，使得砝码重量与状态的乘积之和等于w。

建模步骤 #

1. 变量定义

   • 4个砝码的重量变量：array[1..4] of var 1..40: weights;
   • 针对每个目标重量w的状态变量数组：array[1..4, 1..40] of var -1..1: status;

2. 核心约束

   • 总重量约束：sum(weights) = 40;
   • 可称量所有重量的约束：用forall遍历所有目标重量，结合状态变量的约束实现“存在组合”的逻辑：

     forall(w in 1..40) (
         sum(weights[i] * status[i, w] for i in 1..4) = w
     )
     

   • 可选优化：强制砝码升序排列，避免重复解：constraint weights[1] <= weights[2] <= weights[3] <= weights[4];

完整示例代码 #

array[1..4] of var 1..40: weights;
array[1..4, 1..40] of var -1..1: status;

% 总重量必须为40kg
constraint sum(weights) = 40;

% 升序排列减少重复解
constraint weights[1] <= weights[2] <= weights[3] <= weights[4];

% 确保1到40kg的每个重量都能被称量
constraint forall(w in 1..40) (
    sum(weights[i] * status[i, w] for i in 1..4) = w
);

solve satisfy;

output ["砝码组合: \(weights)"];

关键说明 #

• status[i,w]的三个取值对应砝码的三种使用方式：-1代表和物品放在同一侧，0代表不使用，1代表放在配重侧。
• 求解后会得到经典的[1, 3, 9, 27]组合，这是利用三进制数的特性——每个1到40的整数都能通过3的幂次加减组合得到。

内容的提问来源于stack exchange，提问作者Desiderius Severus