The strength of the dominance rule
<|reference_start|>The strength of the dominance rule: 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 $G_1$, 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.<|reference_end|>
@article{kołodziejczyk2024the,
    title={The strength of the dominance rule},
    author={Leszek Aleksander Ko{l}odziejczyk and Neil Thapen},
    journal={arXiv preprint arXiv:2406.13657},
    year={2024},
    archivePrefix={arXiv},
    eprint={2406.13657},
    primaryClass={cs.LO math.LO}
}