如何检查假定的解决方案会违反哪些约束？答案

【问题标题】：how to check which constraints would be violated by a presumed solution?如何检查假定的解决方案会违反哪些约束？
【发布时间】：2021-03-23 09:39:24
【问题描述】：

在某些情况下，求解器无法为我的模型找到解决方案，我认为它就在那里。所以我想填充一个解决方案，然后检查违反了哪个约束。如何用 choco-solver 做到这一点？

使用 choco-solver 4.10.6。

【问题讨论】：

标签： choco

【解决方案1】：

强制解决

我最终添加了约束以强制变量为我假定的解决方案的值：例如

    // constraints to force given solution 
    vehicle2FirstStop[0].eq(model.intVar(4)).post();
    vehicle2FirstStop[1].eq(model.intVar(3)).post();
    nextStop[1].eq(model.intVar(0)).post();
    nextStop[2].eq(model.intVar(1)).post();
    ...

然后

 model.getSolver().showContradiction();
 if (model.getSolver().solve()) { ....

显示假定解的第一个矛盾，例如

/!\ CONTRADICTION (PropXplusYeqZ(sum_exp_49, mul_exp_51, ...

所以下一步是找出诸如 sum_exp_49 之类的术语的来源。

用代码匹配矛盾项

这是一个简单的约束修复方法，希望能提供足够的信息。我们可以覆盖模型的 post() 和 associates() 方法，以便在发布约束/创建变量时转储 java 源文件名和行号。

   Model model = new Model("Vrp1RpV") {
    /**
     * retrieve the filename and line number of first caller outside of choco-solver from stacktrace
     */
    String getSource() {
        String source = null;
        StackTraceElement[] stackTraceElements = Thread.currentThread().getStackTrace();            
        // starts from 3: thread.getStackTrace() + this.getSource() + caller (post() or associates())
        for (int i = 3; i < stackTraceElements.length; i++) {                
                // keep rewinding until we get out of choco-solver packages
                if (!stackTraceElements[i].getClassName().toString().startsWith("org.chocosolver")) {
                    source = stackTraceElements[i].getFileName() + ":" + stackTraceElements[i].getLineNumber();
                    break;
                }                
        }
        return source;
    }
    @Override
    public void post(Constraint... cs) throws SolverException {
        String source=getSource();
        // dump each constraint along source location
        for (Constraint c : cs) {
            System.err.println(source + " post: " + c);
        }
        super.post(cs);
    }
    
    @Override
    public void associates(Variable variable) {
        System.err.println(getSource() + " associates: " + variable.getName());
        super.associates(variable);
    }
};

这将转储以下内容：

Vrp1RpV2.java:182 post: ARITHM ([prop(EQ_exp_47.EQ.mul_exp_48)])
Vrp1RpV2.java:182 associates: sum_exp_49
Vrp1RpV2.java:182 post: ARITHM ([prop(mul_exp_48.EQ.sum_exp_49)])
Vrp1RpV2.java:182 associates: EQ_exp_50
Vrp1RpV2.java:182 post: BASIC_REIF ([(stop2vehicle[2] = 1) <=> EQ_exp_50])
...

从那里可以看到 sum_exp_49 的来源。

编辑：感谢@cprudhom 对https://gitter.im/chocoteam/choco-solver 的建议，添加了 associates()

【讨论】：