New Algorithms for Parity-SAT and Its Bounded-Occurrence Versions

TL;DR

This paper introduces new algorithms for Parity-SAT and its bounded-occurrence variants, breaking classical exponential barriers by exploiting structural restrictions and parity properties.

Contribution

The paper presents the first randomized algorithm breaking the $2^m$ barrier for fixed variable occurrence bounds and sharper algorithms for the case $d=2$, advancing parity problem solving.

Findings

Breaks the $2^m$ barrier for fixed $d$ in Parity-$d$-occ-SAT

Develops a sharper $O^*(1.1193^n)$ algorithm for $d=2$

Provides an $O^*(1.1052^L)$ algorithm for general Parity-SAT

Abstract

Parity-SAT is the problem of determining whether a given CNF formula has an odd number of satisfying assignments. As a canonical $\oplus$P-complete problem, it represents a fundamental variant of the exact model counting problem (#SAT). Under the Strong Exponential Time Hypothesis (SETH), Parity-SAT admits no $O^*((2-\varepsilon)^n)$-time or $O^*((2-\varepsilon)^m)$-time algorithm for any constant $\varepsilon>0$, where $n$ and $m$ denote the numbers of variables and clauses, respectively. Thus, breaking the $2^n$ or $2^m$ barrier appears impossible in full generality. In this work, we revisit this barrier through structural restrictions and a refined exploitation of parity. We study Parity-$d$-occ-SAT, where each variable appears in at most $d$ clauses, and obtain three main results. First, we design a randomized $O^*(2^{m(1-1/O(d))})$-time algorithm, thereby breaking the $2^m$ barrier for every fixed $d$. Second, for the special case $d=2$, we develop a significantly sharper branching algorithm running in $O^*(1.1193^n)$ time or $O^*(1.3248^m)$ time. Third, leveraging the structural insights underlying the $d=2$ case, we obtain an $O^*(1.1052^L)$-time algorithm for general Parity-SAT, where $L$ denotes the formula length. All algorithms use only polynomial space. Notably, our running-time bounds are better than the best known bounds for the corresponding exact counting counterparts, highlighting a genuine algorithmic advantage of parity over counting. Conceptually, our results demonstrate that parity admits finer structural reductions and more efficient branching than exact model counting, and that bounded occurrence can be systematically leveraged to circumvent classical exponential barriers.