Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

The strength of the dominance rule

Leszek Aleksander Kołodziejczyk, Neil Thapen

TL;DR

It is shown that symmetry-breaking for a single symmetry can be handled inside ER, and evidence is given that the system of [Bogaerts et al. 2023] is plausibly strictly stronger than ER and DRAT.

Abstract

It has become standard that, when a SAT solver decides that a CNF $Γ$ is unsatisfiable, it produces a certificate of unsatisfiability in the form of a refutation of $Γ$ 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.

The strength of the dominance rule

TL;DR

It is shown that symmetry-breaking for a single symmetry can be handled inside ER, and evidence is given that the system of [Bogaerts et al. 2023] is plausibly strictly stronger than ER and DRAT.

Abstract

It has become standard that, when a SAT solver decides that a CNF is unsatisfiable, it produces a certificate of unsatisfiability in the form of a refutation of 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 , 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.
Paper Structure (40 sections, 19 theorems, 27 equations)

This paper contains 40 sections, 19 theorems, 27 equations.

Table of Contents

  1. Introduction
  2. Traditional proof systems
  3. Quantified Boolean formulas and $G_1$
  4. Pseudo-Boolean constraints and cutting planes
  5. Extended resolution as a derivational system
  6. The dominance rule
  7. The dominance proof system
  8. Implicational derivation rule.
  9. (Objective bound update rule
  10. Redundance-based strengthening rule.
  11. Deletion rule.
  12. Transfer rule.
  13. Dominance-based strengthening rule.
  14. Order change rule.
  15. The linear dominance proof system
  16. ...and 25 more sections

Key Result

Proposition 2

If $\omega$ is a symmetry of $\Gamma$, then $\Gamma$ and $\Gamma \cup [\vec{z} \le_{\mathrm{lex}} \vec{z}_{ \upharpoonright \omega}]$ are equisatisfiable.

Theorems & Definitions (41)

  • Definition 1
  • Proposition 2
  • proof
  • Proposition 3: informal
  • proof : Proof (sketch)
  • Theorem 4
  • Theorem 5
  • Definition 6
  • Definition 7
  • Definition 8
  • ...and 31 more