The strength of the dominance rule

TL;DR

This paper compares proof systems for SAT unsatisfiability certificates, showing that a new system can simulate a higher-level proof system and discussing the handling of symmetry-breaking within existing systems.

Contribution

It demonstrates that the new proof system introduced by Bogaerts et al. can simulate the proof system G_1, indicating it is at least as strong as extended resolution and possibly stronger.

Findings

The new proof system simulates the G_1 proof system.

It is plausibly strictly stronger than ER and DRAT.

Symmetry-breaking for a single symmetry can be handled within ER.

Abstract

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.