一个简单的小问题要花很多时间才能证明是不令人满意的

Question

我的代码在飞行中生成minizinc问题，最近我遇到了以下问题：

var int: a;
var int: b;
constraint a < b;
constraint a > b;
solve satisfy;

它花费了大量的时间(在我的机器上大约2分钟(来证明不令人满意。

我尝试了不同的求解器和搜索策略，但未能加快求解速度。

不幸的是，由于我所在区域的具体情况，我无法绑定边界和/或使用MIP。例如，我可以有其他约束，如a * b < 100或a == arbitrary number。

有什么想法吗？我将非常感谢你的任何建议。

最佳，

Answer 1

正如您所提到的，问题是变量没有边界，这对CP求解器来说不是很好。难道没有办法在这个问题上给出一个大的域吗？例如

var -100000..100000: a;
var -100000..100000: b;        

则Gecode需要0.5s才能产生UNSAT。

对于您最初的问题(使用var int(，我测试了一些基于SAT/非CP的解算器，它们可以很快检测到UNSAT：

• geas:5.282s

• picatSAT:0.115s

• optimathSAT:0.519s

• 错误：0.177s

• oscar_cbls:1.376s

我还使用SAT混合解算器或工具和Chuffed进行了测试，但它们在这个特定问题上的速度相当慢。

然而，这只是问题的一半，因为求解器在非UNSAT实例上也应该很快，对吧？那么SAT解算器可能不是最快的。

一个想法是使用组合求解器，如SunnyCP，它有一个不同的FlatZinc求解器池，试图并行解决问题。(不幸的是，我的SunnyCP安装现在不工作，所以我无法测试它。(