CNF Encodings of Parity

2022/03/02 by Emdin, Gregory, Kulikov, Alexander S., Mihajlin, Ivan +1 · 1 citation
#Computational Complexity (cs.CC) #FOS: Computer and information sciences

paper · doi:10.48550/arxiv.2203.01082

Abstract

The minimum number of clauses in a CNF representation of the parity function x₁ ⊕ x₂ ⊕ \dotsb ⊕ x_n is 2^n-1. One can obtain a more compact CNF encoding by using non-deterministic variables (also known as guess or auxiliary variables). In this paper, we prove the following lower bounds, that almost match known upper bounds, on the number m of clauses and the maximum width k of clauses: 1) if there are at most s auxiliary variables, then m ≥ Ω(2^n/(s+1)/n) and k ≥ n/(s+1); 2) the minimum number of clauses is at least 3n. We derive the first two bounds from the Satisfiability Coding Lemma due to Paturi, Pudlak, and Zane.

Cited by

• Asymptotically Smaller Encodings for Graph Problems and Scheduling

Related

• Hardness Results for Approximate Pure Horn CNF Formulae Minimization
• An Improved Upper Bound for SAT
• Unsatisfiable Linear CNF Formulas Are Large and Complex
• On the CNF encoding of cardinality constraints and beyond
• Small unsatisfiable k-CNFs with bounded literal occurrence