对称变量对BDD顺序影响：最优解的探索与误区

对称变量在BDD（二元决策图）中的顺序性对最终结果有显著影响，特别是在表示布尔函数时。BDD的大小对变量排列非常敏感，特别是当使用基于筛选的重新排序算法时，这些算法会考虑对称性并尝试将对称变量分组，如在对称筛选法中。这种方法在许多情况下能够产生满意的结果，但并非总是最优。 研究者们注意到，某些文献如[PS94]和[PS95]提出的启发式策略，如将对称变量聚集在一起进行排序，虽然在一般情况下表现出色，但在特定情况下，比如在[PS95]中提到的函数f(x;y;z) = xy + yz0 + y0zw的例子中，可能存在误解。原作者认为没有一个对称的顺序是最佳的，但后来发现函数f实际上有两个对称的最优阶数：xyz和xzy。这个误解揭示了对称变量的顺序优化问题的复杂性，即并非所有看起来不理想或不对称的排列都是最差的。 在本论文中，作者首先证明了部分对称函数的一些关键性质，以深化对这一现象的理解。他们随后开发了一个更快的程序，专门针对那些可以用nn-等价类划分的布尔函数，以搜索可能的最优变量顺序。研究者们还探讨了反例的结构，提出了利用现有反例生成新反例的方法，这对于评估和优化变量排序策略至关重要。 进一步的研究发现，布尔函数的对称性使得不同的变量排列组合可能导致极大的多样性。这意味着，即使在最坏的情况下，对称变量的顺序仍然可能落在从最优顺序的一段范围内。因此，优化BDD中的变量顺序是一个既挑战性又复杂的任务，需要深入理解对称性在其中的作用以及如何更有效地处理它。 本论文通过理论分析和实践探索，揭示了对称变量在BDD中排序的重要性，并提供了一种更全面的方法来处理这一问题，以期望在未来优化BDD表示的布尔函数的性能。对于BDD使用者和开发者来说，理解并合理利用对称性对提升算法效率和解决问题的质量具有实际价值。