仅当 IntVars 之间的某些关系为真时才对 CpModel 施加约束

Question

tl;dr：我在 Java 中使用 Google OR-Tools。我想根据涉及 IntVar 变量的子句是否为真，向 CpModel 添加条件约束。基本上，像

CpModel model = new CpModel;
List<Literal> workers = getActiveWorkers();
IntVar startTimeVar = model.newIntVar(0, 100, "start");
int currentTime = getCurrentTime(); //guaranteed to be < 100, say.
IntVar currentTimeVar = model.newConstant(currentTime);
// What I'd want to write but can't
model.addExactlyOne(workers).onlyEnforceIf(currentTimeVar >= startTimeVar);

要替换 "currentTime >= startTime"，我可能想要类似 model.addGreaterOrEqual(currentTimeVar, startTimeVar) 的东西，但是这个 returns（并添加到模型中）是 Constraint，而不是 Literal。（我知道onlyEnforceIf的参数类型是Literal[]）。我可以做什么？

更多上下文： 我试图概括 OR 工具站点上的 Employee Schedule and Job Shop Scheduling 示例。我有 J 个工作，每个工作的持续时间称为 j.duration，要分配给 W 工作人员。主要有两个限制：

每个工作必须有一个唯一的工人，并且；
工人一次最多只能从事一份工作。

我想最小化完工时间，其上限为 T =（所有工作持续时间的总和）。我的问题是，要强制执行约束 (1)，我需要为每个工作 j 强制执行该约束，分配给一名工人仅次t 满足 j.start <= t < j.end.

我的代码与我 link编辑的两个示例非常相似。与员工时间表示例一样，我跟踪布尔文字的赋值数组 assignment[w][j][t]，表示 if worker w 在工作 j，时间 t。

public static void main(String[] args) {
        class Job {
            int duration;
            String name;
        }
        class JobVariable {
            IntVar start, end;
            IntervalVar duration;
        }
        Loader.loadNativeLibraries();
        List<Job> jobs = getJobData();

        final int numJobs = jobs.size();
        final int numWorkers = 3;
        final int timeUpperBound = items.stream().mapToInt(j -> j.duration).sum();

        CpModel model = new CpModel();

        //Initialize assignments array.
        Literal[][][] assignments = new Literal[numWorkers][numJobs][timeUpperBound];
        for(int w = 0; w < numWorkers; w++){
            for(int j = 0; j < numJobs; j++){
                for(int t = 0; t < timeUpperBound; t++){
                    assignments[w][j][t] = model.newBoolVar("Worker"+w+"Job"+j+"Time"+t);
                }
            }
        }

        //Initialize IntVars and IntervalVar for each job
        Map<Job, JobVariable> jobToVariable = new HashMap<>();
        for(Job job : jobs){
            JobVariable jobVar = new JobVariable();
            jobVar.start = model.newIntVar(0, timeUpperBound, "start:" + job.name);
            jobVar.end = model.newIntVar(0, timeUpperBound, "end:" + job.name);
            jobVar.duration = model.newIntervalVar(jobVar.start, 
            LinearExpr.constant(job.duration), jobVar.end, "interval:" + job.name);
            jobToVariable.put(job, jobVar);
        }
        eachWorkerHasAtMostOneTaskAtATime(assignments, numWorkers, numJobs, timeUpperBound, model);

        eachTaskHasUniqueWorker(assignments, numWorkers, numJobs, timeUpperBound, model, jobToVariable);

        //Solve model...
        CpSolver solver = new CpSolver();
        CpSolverStatus status = solver.solve(model);
    }

方法 eachWorkerHasAtMostOneTaskAtATime 看起来就像示例代码，对每个工作和时间的工人进行“求和”，并且与 Employee Scheduling link 中的片段相同。另一种方法是我的问题出现的地方 - 我需要确保（a）每个工作在活动时都有一个工人，并且（b）同一个工人在活动时处理工作。这些的数学约束在下面代码片段的注释中：

public static void eachJobHasUniqueWorker(Literal[][][] assignments,
                                             int numWorkers,
                                             int numJobs,
                                             int timeUpperBound,
                                             CpModel model,
                                             Map<Job, JobVariable> jobToVariable,
                                             List<Job> jobs){
        // Constraint (a): 
        // for all jobs j,
        //  and for all time t where j.start <= t < j.end,
        //   ensure that exactly one worker is assigned to job j.

        for(int j = 0; j < numJobs; j++){
            JobVariable jobVariable = jobToVariable.get(jobs.get(j));
            for(int t = 0; t < timeUpperBound; t++){
                Literal timeInJobInterval = model.newBoolVar("time_"+t+"job_"+j);
                
                //tie the value of timeInJobInterval
                //to something reflecting j.start <= t < j.end
                model.AddBoolAnd(timeInJobInterval, SOMETHING GOES HERE?)

                List<Literal> workers = new ArrayList<>();
                for(int w = 0; w < numWorkers; w++){
                    workers.add(assignments[w][j][t]);
                }
 
                model.addExactlyOne(workers).onlyEnforceIf(timeInJobInterval);
            }
        }

        // Constraint (b):
        // for all jobs j,
        //  if assignment[w][j][t] == 1 and t < j.end - 1,
        //   then assignment[w][j][t+1] == 1
        for(int j = 0; j < numJobs; j++){
            for(int t = 0; t < timeUpperBound; t++){
                for(int w = 0; w < numWorkers; w++){
                    Literal timeStrictlyBeforeStepEnd = model.newBoolVar("time"+t+"job"+j);
                    // again, tie the above value to
                    // the condition t < j.end - 1
                    model.addBoolAnd(timeStrictlyBeforeStepEnd, SOMETHING HERE);
                    model.addImplication(assignments[w][j][t], assignments[w][j][t+1]).onlyEnforceIf(timeStrictlyBeforeStepEnd);
                }
            }
        }
    }

如前所述，我希望 timeInJobInterval 字面量反映索引 t 是否在作业的范围内 - 如果是，那么我已设置，但我不知道如何确保这一点。 tl;dr 中概述的方法也不起作用。

如有任何帮助，我们将不胜感激。另外，如果您发现比我概述的方法更简洁的方法，请告诉我。

Answer 1

假设您在两个整数变量和结果约束 ct 之间有一个条件 cond，并且您想要强制执行 cond implies ct.

最好的方法是创建一个布尔变量 cond_is_true，然后 link 它同时赋给 ct 和 cond。

    Literal condIsTrue = model.newBoolVar("condIsTrue");
    model.add(cond).onlyEnforceIf(condIsTrue);
    model.add(negation_of_cond).onlyEnforceIf(condIsTrue.not());
    model.add(ct).onlyEnforceIf(condIsTrue);

参见 this channeling documentation page。

仅当 IntVars 之间的某些关系为真时才对 CpModel 施加约束

Impose Constraint on CpModel only when some relation between IntVars is true

java

or-tools

constraint-programming