Extended resolution shows that auxiliary variables are very powerful in theory. However, attempts to exploit this potential in practice have had limited success. One reasonably effective method in this regard is bounded variable addition (BVA), which automatically reencodes formulas by introducing new variables and eliminating clauses, often significantly reducing formula size. We find motivating examples suggesting that the performance improvement caused by BVA stems not only from this size reduction but also from the introduction of effective auxiliary variables. Analyzing specific packing-coloring instances, we discover that BVA is fragile with respect to formula randomization, relying on variable order to break ties. With this understanding, we augment BVA with a heuristic for breaking ties in a structured way. We evaluate our new preprocessing technique, Structured BVA (SBVA), on more than 29,000 formulas from previous SAT competitions and show that it is robust to randomization. In a simulated competition setting, our implementation outperforms BVA on both randomized and original formulas, and appears to be well-suited for certain families of formulas.

翻译：扩展归结理论表明，辅助变量在理论上具有强大功能。然而在实践中利用这一潜力的尝试成效有限。目前较为有效的方法之一是边界变量添加（BVA），它通过引入新变量并消除子句来自动重编码公式，通常能显著减小公式规模。我们发现的激励性示例表明，BVA带来的性能提升不仅源于规模缩减，更在于引入了高效的辅助变量。通过分析特定的填充着色实例，我们发现BVA对公式随机化非常敏感，其依赖变量顺序打破平局。基于此认识，我们对BVA进行了增强，引入了一种结构化打破平局的启发式方法。我们在来自此前SAT竞赛的超过29000个公式上评估了新型预处理技术——结构化BVA（SBVA），证明其对随机化具有鲁棒性。在模拟竞赛环境中，我们的实现在随机化公式和原始公式上均优于BVA，并展现出对特定公式族的良好适应性。