部分回溯搜索的通用算法答案

【问题标题】：General algorithm for partial backtracking search部分回溯搜索的通用算法
【发布时间】：2020-09-06 19:29:58
【问题描述】：

回溯搜索是一种众所周知的问题解决技术，它通过所有可能的变量分配组合来寻找有效的解决方案。通用算法被抽象成简洁的高阶函数：https://en.wikipedia.org/wiki/Backtracking

有些问题需要部分回溯，也就是说，它们混合了不知道的非确定性（有一个选择，这很重要，如果你弄错了，你必须回溯）和不关心非确定性（可以做出选择，这并不重要，也许重要的是你需要多长时间才能找到解决方案，而不是正确性其中，您不必回溯）。

考虑例如可以用the DPLL algorithm 解决的布尔可满足性问题。如果你试图用一般的回溯算法来表示它，结果不仅会通过所有 2^N 变量赋值（遗憾的是在一般情况下是必要的），而且所有 N！尝试变量的顺序（完全没有必要，而且效率极低）。

是否有用于部分回溯的通用算法？一个简洁的高阶函数，它为 don't-know 和 don't-care 选择提供函数参数？

【问题讨论】：

DPLL 真的会遍历变量的所有排列吗？我的印象是它在每一步都使用启发式方法选择了一些单个变量，然后尝试了两个分支以查看公式是否可以满足。如果两个分支都失败了，那么给定点的公式肯定不能满足，没有理由尝试不同的变量。
@templatetypedef 确实，DPLL 算法本身在这方面很好。但是，如果您从 DPLL 中去掉回溯部分，转而使用通用回溯算法（只为特定领域的部分提供参数）呢？一般的回溯算法不会表现得那么好；它将遍历变量的所有排列。（从某种意义上说，它不会知道变序的选择是不需要回溯的那种选择。）
我不喜欢 Wikipedia 伪代码如何模拟具有两个不同函数的迭代器/惰性列表 - 与返回惰性搜索列表的函数相比，它更难实现有趣的分支启发式树子按顺序打开（即便如此，树探索策略的选择也会产生很大的不同，将深度优先搜索与深度优先的最佳回溯进行比较）。
我常用的概括最好的启发式方法是，最受约束的优先。特别是对于使用 DPLL 解决 SAT 问题，将子句减少为单元子句是一个巨大的胜利，因为它可以让你进行单元传播，所以我会启发式地关注最短的子句。这应该更快地给你单元子句。
但是，有许多免费的、高度优化的 SAT 求解器。除非这是一个学习练习，否则请考虑使用其中之一。

标签： algorithm search backtracking recursive-backtracking

【解决方案1】：

如果我理解正确，您是在询问树搜索中的对称性破坏。在您给出的具体示例中，变量赋值列表的所有排列都是等价的。

对称将是特定领域的。修剪搜索树的更通用技术也是如此，即通过短路和热切回溯。我使用了一些打破对称性的技术来概括。

一种是以规范的顺序搜索问题空间。如果设置变量 10 的分支只尝试变量 11、12 及以上变量，而不尝试变量 9、8 或 7，则它不会搜索相同解的任何排列。它只会测试排列唯一的解决方案。（在 SAT 求解的特定情况下，这可能会排除最佳搜索顺序——尽管您可以任意重新排序变量。）

另一种方法是进行测试，任何等价类只有一个不同的解决方案可以通过，理想情况下可以在搜索树顶部附近检查。典型的例子是，在 8-queens 问题中，检查你首先看的那行的皇后是在棋盘的左边还是右边。她在右侧的任何解决方案都是她在左侧的另一个解决方案的镜像，因此您可以将搜索空间减半。（实际上你可以在这个问题上做得比这更好。）如果你只需要测试可满足性，你可以使用一个过滤器来保证，如果存在任何解决方案，至少一个解决方案将通过。

如果你有足够的内存，你还可以存储一组已经搜索过的分支，然后检查你正在考虑是否要搜索的分支是否与集合中已经存在的分支等价。对于具有大量对称性的搜索空间，这将比具有大量对称唯一解的搜索空间更实用。

【讨论】：