CNF Encodings of Parity

The minimum number of clauses in a CNF representation of the parity function \(x_1 \oplus x_2 \oplus \dotsb \oplus 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...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2022-05
Main Authors: Emdin, Gregory, Kulikov, Alexander S, Mihajlin, Ivan, Slezkin, Nikita
Format: Article
Language:English
Subjects:
Lower bounds
Parity
Upper bounds
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:The minimum number of clauses in a CNF representation of the parity function \(x_1 \oplus x_2 \oplus \dotsb \oplus 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 \ge \Omega\left(2^{n/(s+1)}/n\right)\) and \(k \ge 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.
ISSN:2331-8422