visualization - MiniZinc 中的灰色方块代表什么?
问题描述
在 Minizinc 中可视化执行树(通过配置文件搜索创建)时,我获得了一个包含灰色方块的树。
它们代表什么?
解决方案
灰色方块是后跳。它们是求解器能够证明不存在解决方案的树的一部分。
在一般约束规划求解器中,求解器执行树搜索。每当您发现一个分支不包含任何解决方案时,您就会转到另一个分支。传统上,每个搜索决策都有两个分支。例如,赋值及其否定。但也可以为变量可以采用的每个可能值创建一个分支。
在惰性子句生成求解器中,搜索的工作方式略有不同。每当您发现搜索失败时,您就让 SAT 后端生成一个原因,通常称为“不合格”。这个不好解释了为什么这个分支不包含任何解决方案,并且可以从那时起作为一个新的约束来强制执行。如果你只是重新审视你的上一个决定,那么这个新的约束可能仍然会被违反。取而代之的是,这些 LCG 求解器使用后跳机制跳到最后一个尚未违反不合格的决策。
推荐阅读
- data-structures - 数据结构:什么是 T 表?
- react-native - React Native 月份和年份选择器
- java - 在 Java 中使用 HttpURLConnection POST
- c++ - 如何使用 OpenCV 将 RBG 图像转换为 HSV 并将 H、S 和 V 值保存到 C++ 中的 3 个单独的图像中?
- android - TouchableOpacity onLongPress 拦截 FlatList 滚动
- gspread - 更新 gspread 以获取 duplicate_sheet
- java - 连接未与托管连接关联
- robotframework - 如何从机器人框架代码之间的全局变量中获取值
- c++ - OpenCV EqualizeHist() 从彩色图像创建黑白图像
- javascript - 使用 DOM 结合 For 循环创建表;用数组填充表?- JavaScript