# Effective Auxiliary Variables via Structured Reencoding

arXiv: https://arxiv.org/abs/2307.01904 · HTML: https://mlsanity.com/paper/2307.01904/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 4 Jul 2023.

## Built on by (most cited first, 7 of 7)

- [Global Benchmark Database](https://mlsanity.com/paper/2405.10045/) (2024)
- [Automated Explanation Selection for Scientific Discovery](https://mlsanity.com/paper/2407.17454/) (2024)
- [A Reinforcement Learning based Reset Policy for CDCL SAT Solvers](https://mlsanity.com/paper/2404.03753/) (2024)
- [Solving Cyclic Antibandwidth Problem by SAT](https://mlsanity.com/paper/2601.04239/) (2026)
- [Asymptotically Smaller Encodings for Graph Problems and Scheduling](https://mlsanity.com/paper/2506.14042/) (2025)
- [Learning to Solve Weighted Maximum Satisfiability with a Co-Training Architecture](https://mlsanity.com/paper/2511.19544/) (2025)
- [Solving Minimum Span Antibandwidth and Cyclic Antibandwidth Labeling Problems](https://mlsanity.com/paper/2609.20091/) (2026)

## Abstract (arXiv)

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.