Research map / Learning theory and algorithms / Combinatorial and search optimization

Hardness of Random Reordered Encodings of Parity for Resolution and CDCL

AAAI 2024 · Learning theory and algorithms › Combinatorial and search optimization · approach: SAT and model counting solvers · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Shows that random reordered XOR/parity encodings (rPar and rAddPar) are Tseitin formulas with linear treewidth w.h.p., hence exponentially hard for resolution, while admitting short DRAT^- proofs, and confirms experimentally that CDCL runtime grows exponentially with treewidth.

Problem

CDCL solvers struggle on simple contradictory parity constraints encoded with different variable orders; no resolution lower bound was known for these formulas, and the role of Gaussian-elimination-style addition steps was unexplained.

Approach

Recognizes that the reordered parity formulas are Tseitin formulas whose graphs have linear treewidth with high probability under random variable orders (via random 4-regular graph results), so known treewidth-based resolution lower bounds apply; extends the argument to a random parity-addition family and gives short DRAT^- and extended resolution refutations.

Key results

• Random permutation rPar(n,sigma) formulas have resolution refutations of length at least 2^{alpha n} w.h.p., since their Tseitin graphs have linear treewidth.
• CaDiCaL running time grows exponentially with the best treewidth upper bound on both rPar and rAddPar benchmarks.
• rAddPar(a,b) and rPar(n,sigma) admit DRAT^- refutations with O(n log n) lines.

Measured effects reported in the paper

Surprising findings

• CryptoMiniSat, which uses Gaussian elimination, solved all reordered parity instances within a few seconds while CaDiCaL timed out on high-treewidth ones.

Limitations

• Treewidth gray area between logarithmic and linear is not resolved.
• Experimental benchmarks are not uniformly sampled, unlike the theoretical random model.
• Treewidth of 100-vertex graphs could only be bounded, not always computed exactly.

Experimental setup

Datasets: rPar(n,sigma) benchmark formulas (n=50) rAddPar(a,b) benchmark formulas (95 instances)

Benchmarks: rPar(n,sigma) formulas n=50 rAddPar(a,b) formulas

Metrics: solving time treewidth upper and lower bounds

Baselines: CaDiCaL CryptoMiniSat

Builds on: Tseitin formulas Ben-Sasson and Wigderson width-length relations Galesi et al. treewidth lower bounds Chew and Heule DRAT sorting proofs

Closest papers by meaning

• A Cardinal Improvement to Pseudo-Boolean Solving (AAAI 2020 · similarity 0.88)
• Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs (AAAI 2021 · similarity 0.88)
• MaxSAT Resolution With the Dual Rail Encoding (AAAI 2018 · similarity 0.86)
• The Impact of Literal Sorting on Cardinality Constraint Encodings (AAAI 2025 · similarity 0.86)
• Runtime vs. Extracted Proof Size: An Exponential Gap for CDCL on QBFs (AAAI 2024 · similarity 0.86)
• Parameterization of (Partial) Maximum Satisfiability above Matching in a Variable-Clause Graph (AAAI 2024 · similarity 0.85)