# The strength of the dominance rule

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 19 Jun 2024.

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

- [Faster Certified Symmetry Breaking Using Orders With Auxiliary Variables](https://mlsanity.com/paper/2511.16637/) (2025)

## Abstract (arXiv)

It has become standard that, when a SAT solver decides that a CNF Gamma is unsatisfiable, it produces a certificate of unsatisfiability in the form of a refutation of Gamma in some proof system. The system typically used is DRAT, which is equivalent to extended resolution (ER) -- for example, until this year DRAT refutations were required in the annual SAT competition. Recently [Bogaerts et al.~2023] introduced a new proof system, associated with the tool VeriPB, which is at least as strong as DRAT and is further able to handle certain symmetry-breaking techniques. We show that this system simulates the proof system G1, which allows limited reasoning with QBFs and forms the first level above ER in a natural hierarchy of proof systems. This hierarchy is not known to be strict, but nevertheless this is evidence that the system of [Bogaerts et al. 2023] is plausibly strictly stronger than ER and DRAT. In the other direction, we show that symmetry-breaking for a single symmetry can be handled inside ER.