Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Hardness of Random Reordered Encodings of Parity for Resolution and CDCL

Leroy Chew, Alexis de Colnet, Friedrich Slivovsky, Stefan Szeider

TL;DR

Parity reasoning is notoriously hard for CDCL and resolution when encoded with random variable orders. The authors prove that the formulas $\mathsf{rPar}(n,\sigma)$ and a related family $\mathsf{rAddPar}(a,b)$ are Tseitin formulas whose Tseitin graphs have $tw = \Omega(n)$ with high probability, implying exponential resolution refutations. They also show that DRAT$^-$ and Extended Resolution proofs exist with $O(n\log n)$ lines, while Gaussian-elimination-inspired reasoning captures practical upper bounds. Experiments corroborate the link between treewidth and CDCL solving time, with running time growing exponentially in $tw$, whereas XOR-aware solvers can handle many instances quickly.

Abstract

Parity reasoning is challenging for Conflict-Driven Clause Learning (CDCL) SAT solvers. This has been observed even for simple formulas encoding two contradictory parity constraints with different variable orders (Chew and Heule 2020). We provide an analytical explanation for their hardness by showing that they require exponential resolution refutations with high probability when the variable order is chosen at random. We obtain this result by proving that these formulas, which are known to be Tseitin formulas, have Tseitin graphs of linear treewidth with high probability. Since such Tseitin formulas require exponential resolution proofs, our result follows. We generalize this argument to a new class of formulas that capture a basic form of parity reasoning involving a sum of two random parity constraints with random orders. Even when the variable order for the sum is chosen favorably, these formulas remain hard for resolution. In contrast, we prove that they have short DRAT refutations. We show experimentally that the running time of CDCL SAT solvers on both classes of formulas grows exponentially with their treewidth.

Hardness of Random Reordered Encodings of Parity for Resolution and CDCL

TL;DR

Parity reasoning is notoriously hard for CDCL and resolution when encoded with random variable orders. The authors prove that the formulas and a related family are Tseitin formulas whose Tseitin graphs have with high probability, implying exponential resolution refutations. They also show that DRAT and Extended Resolution proofs exist with lines, while Gaussian-elimination-inspired reasoning captures practical upper bounds. Experiments corroborate the link between treewidth and CDCL solving time, with running time growing exponentially in , whereas XOR-aware solvers can handle many instances quickly.

Abstract

Parity reasoning is challenging for Conflict-Driven Clause Learning (CDCL) SAT solvers. This has been observed even for simple formulas encoding two contradictory parity constraints with different variable orders (Chew and Heule 2020). We provide an analytical explanation for their hardness by showing that they require exponential resolution refutations with high probability when the variable order is chosen at random. We obtain this result by proving that these formulas, which are known to be Tseitin formulas, have Tseitin graphs of linear treewidth with high probability. Since such Tseitin formulas require exponential resolution proofs, our result follows. We generalize this argument to a new class of formulas that capture a basic form of parity reasoning involving a sum of two random parity constraints with random orders. Even when the variable order for the sum is chosen favorably, these formulas remain hard for resolution. In contrast, we prove that they have short DRAT refutations. We show experimentally that the running time of CDCL SAT solvers on both classes of formulas grows exponentially with their treewidth.
Paper Structure (22 sections, 20 theorems, 59 equations, 4 figures)

This paper contains 22 sections, 20 theorems, 59 equations, 4 figures.

Table of Contents

  1. Introduction
  2. Problem 1: Reordered Parity
  3. Problem 2: Random Parity Addition
  4. Preliminaries
  5. Proofs and Refutations
  6. Resolution.
  7. Extended Resolution.
  8. DRAT.
  9. Treewidth
  10. Tseitin Formulas
  11. Parity Problems
  12. Problem 1: Reordered Parity
  13. Problem 2: Random Parity Addition
  14. The Graph Model and Lower Bounds
  15. Lower Bounds for Reordered Parity
  16. ...and 7 more sections

Key Result

Theorem 1

There is a constant $\alpha>0$ such that, with probability tending to $1$ as $n$ increases, the length of a smallest resolution refutation of the unsatisfiable formula $\mathsf{rPar}(n, \sigma)$, where $\sigma$ is chosen uniformly at random, is at least $2^{\alpha n}$.

Figures (4)

  • Figure 1: Construction of $m(H)$
  • Figure 2: DRAT steps required for Lemma \ref{['switching']}, d denotes a deletion step.
  • Figure 3: Treewidth (x-axis) vs. solving time (y-axis) for reordered parity (left) and random parity addition (right).
  • Figure 4: Lower and upper bounds for the treewidth (y-axis) of reordered parity formulas (x-axis).

Theorems & Definitions (42)

  • Theorem 1
  • Theorem 2
  • Theorem 3
  • Theorem 4
  • Example 1
  • Definition 1
  • Definition 2: JHB12
  • Definition 3: JHB12
  • Example 2
  • Theorem 5
  • ...and 32 more